The file compiles on my linux machine with 8.4pl4.
On Mon, May 19, 2014 at 2:58 PM, Bas Spitters <[email protected]> wrote: > 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
