Compilation problem with Coq 8.4pl5
vzaliva opened this issue · 0 comments
vzaliva commented
After upgrading to Coq 8.4pl5 I am getting a compilation error:
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"