I'll try to have a closer look (at the IHP now). I use scons v2.3.0
On Sun, May 18, 2014 at 5:29 PM, Gyesik Lee <[email protected]> wrote: > 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 > >
_______________________________________________ C-CoRN mailing list [email protected] http://mailman.science.ru.nl/mailman/listinfo/c-corn
