ID0000027: **This issue was created automatically from Mantis Issue 27. Further discussion may take place here.** --- | **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** | | --- | --- | --- | --- | --- | --- | | ID0000027 | Frama-C | Plug-in > jessie | public | 2009-04-07 | 2009-12-03 | | | | | | | | | --- | --- | --- | --- | --- | --- | | **Reporter** | virgile | **Assigned To** | cmarche | **Resolution** | fixed | | **Priority** | normal | **Severity** | minor | **Reproducibility** | always | | **Platform** | - | **OS** | - | **OS Version** | - | | **Product Version** | Frama-C Lithium-20081201 | **Target Version** | - | **Fixed in Version** | - | ### Description : [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. Regards, Nicolas. ### Additional Information : Depends upon coq 8.2?