Jessie: the 'R' reference seems to be not present in the current release (Real for coq ?)
ID0000027: This issue was created automatically from Mantis Issue 27. Further discussion may take place here.
|ID0000027||Frama-C||Plug-in > jessie||public||2009-04-07||2009-12-03|
|Product Version||Frama-C Lithium-20081201||Target Version||-||Fixed in Version||-|
[bug 7104 of old BTS, reported by Nicolas Stouls] when calling
cd t.jessie make -f t.makefile coq-goals
after a "frama-c t.c -jessie-anaysis -jessie-gui" The following error is returned :
coqc -I coq coq/t_ctx_why.v Error while reading (...)/t.jessie/coq/t_ctx_why.v : File "(...)/t.jessie/coq/t_ctx_why.v", line 139, characters 46-47 Error: The reference R was not found in the current environment make: *** [coq/t_ctx_why.vo] Erreur 1
Currently, the context file generated by Jessie (t_ctx_why.v) includes some Defintions such as :
(Why logic) Definition add_real : R -> R -> R. Admitted.
but R is not defined.
Additional Information :
Depends upon coq 8.2?