Hi, an error occurred during building the whole library with the following messages:
...... coqc metric2/Metric -R . CoRN -R math-classes/src MathClasses File "/home/gslee/c-corn/corn/metric2/Metric.v", line 48, characters 33-36: Error: In environment is_MetricSpace : forall X : RSetoid, (Qpos -> relation X) -> Prop X : RSetoid B : Qpos -> relation X e : Qpos The term "B e" has type "relation X" while it is expected to have type "CProp". scons: *** [metric2/Metric.vo] Error 1 scons: building terminated because of errors. .... That is, there is a type mismatch in the metric2/Metric.v library. I am using Ubuntu 14.04 with Coq 8.4pl4 and scons 1.2.0 First question: Does this error just mean that some updates of the library are not compatible? Second question: Does the version of scons does not matter when it is >= 1.2? I tested both versions (1.2.0 and the latest). During building, the latest version shows hardly a warning, but the 1.2.0 version shows a lot. (It's my first time to use scons.) But the errors occur at the same point. Gyesik
_______________________________________________ C-CoRN mailing list [email protected] http://mailman.science.ru.nl/mailman/listinfo/c-corn
