Thank you. It works. Gyesik 2014. 5. 22. 오전 6:46에 "Bas Spitters" <[email protected]>님이 작성:
> > 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
