The Coq mailing list

[Vadim Zaliva <vzaliva AT cmu.edu>]

After upgrading to 8.4pl5 I am no longer able to compile MathClasses.

coqc -R . CoRN -R math-classes/src MathClasses -q 
math-classes/src/theory/adjunctions.v
File "/Volumes/CORN/corn/math-classes/src/theory/adjunctions.v", line 192, 
characters 32-38:
Error: Illegal application (Non-functional construction):
The expression "φ c" of type "?1062 ⟶ G ?1063"
cannot be applied to the term
 "d" : "?1057"

I am not up to the task of fixing it myself. Does somebody have a workaround?
To make things worse, one could no longer used the version compiled with with
previous version:

Error: Compiled library MathClasses.interfaces.abstract_algebra.vo makes
inconsistent assumptions over library Coq.Init.Datatypes

The only course of action I see is to downgrade to 8.4pl4.

Sincerely,
Vadim Zaliva

--
CMU ECE PhD student
Mobile: +1(510)220-1060
Skype: vzaliva