coq 8.5: cannot find Memory.v

ID0002208: This issue was created automatically from Mantis Issue 2208. Further discussion may take place here.

---

Id	Project	Category	View	Due Date	Updated
ID0002208	Frama-C	Plug-in > wp	public	2016-02-11	2017-01-03

Reporter	jens	Assigned To	correnson	Resolution	fixed
Priority	normal	Severity	major	Reproducibility	always
Platform	-	OS	-	OS Version	-
Product Version	Frama-C Magnesium	Target Version	-	Fixed in Version	-

Description :

After updating my Frama-C installation through opam to coq.8.5 and why3.0.86.3 I observe the following error. When compiling the attached file with

coqc -R /Users/jens/.opam/system/share/frama-c/wp/coqwp -as "" WP_basics.v

I receive the following error message:

File "./WP_basics.v", line 3, characters 15-21:
Error: Unable to locate library Memory.

With coq.8.4.6 and earlier I did not observe this error.

Additional Information :

The path '/Users/jens/.opam/system/share/frama-c' points to my Frama-C share.

ls -l /Users/jens/.opam/system/share/frama-c/wp/coqwp/Memory.v

produces

-rw-r--r-- 1 jens staff 10160 11 Feb 10:38 /Users/jens/.opam/system/share/frama-c/wp/coqwp/Memory.v

Attachments

• WP_basics.v