The Coq mailing list

[Cedric Auger <sedrikov AT gmail.com>]

Seing the file on the git repository, I guess that changing (φ c d) into (@φ c d) should do the trick. Didn’t tried it though.

2014-12-04 1:01 GMT+01:00 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

--

.../Sedrikov\...