Commit 0a94e6be authored by Armaël Guéneau's avatar Armaël Guéneau

Merge branch 'coq-fixes' into 'master'

Make CFML work with coq 8.6.1 and newer

See merge request !4
parents e7e1c856 fd3a3137
...@@ -19,18 +19,15 @@ CFML consists of two parts: ...@@ -19,18 +19,15 @@ CFML consists of two parts:
Installation Installation
============ ============
The current version of CFML requires Coq 8.6 (*not* 8.6.1). The current version of CFML requires Coq 8.6 or newer.
The simplest way of installing the *latest released version* of CFML is via `opam`. The simplest way of installing the *latest released version* of CFML is via `opam`.
It is recommended to create a new switch, whose name you can choose;
in the following, we use `cfml86`.
```sh ```sh
opam switch cfml86 -A 4.05.0 # This only needs to be done once, to add the opam repository with coq packages
eval `opam config env` opam repo add coq-released https://coq.inria.fr/opam/released
opam install -j4 coq.8.6
opam install -j4 coq-cfml opam install coq-cfml
``` ```
If instead you wish to use *the development version* of CFML, If instead you wish to use *the development version* of CFML,
......
...@@ -1923,16 +1923,16 @@ Ltac hsimpl_try_same tt := ...@@ -1923,16 +1923,16 @@ Ltac hsimpl_try_same tt :=
Ltac hsimpl_find_same H HL := Ltac hsimpl_find_same H HL :=
match HL with match HL with
| H \* _ => apply hsimpl_cancel_1 | ?H' \* _ => unify H H'; apply hsimpl_cancel_1
| _ \* H \* _ => apply hsimpl_cancel_2 | _ \* ?H' \* _ => unify H H'; apply hsimpl_cancel_2
| _ \* _ \* H \* _ => apply hsimpl_cancel_3 | _ \* _ \* ?H' \* _ => unify H H'; apply hsimpl_cancel_3
| _ \* _ \* _ \* H \* _ => apply hsimpl_cancel_4 | _ \* _ \* _ \* ?H' \* _ => unify H H'; apply hsimpl_cancel_4
| _ \* _ \* _ \* _ \* H \* _ => apply hsimpl_cancel_5 | _ \* _ \* _ \* _ \* ?H' \* _ => unify H H'; apply hsimpl_cancel_5
| _ \* _ \* _ \* _ \* _ \* H \* _ => apply hsimpl_cancel_6 | _ \* _ \* _ \* _ \* _ \* ?H' \* _ => unify H H'; apply hsimpl_cancel_6
| _ \* _ \* _ \* _ \* _ \* _ \* H \* _ => apply hsimpl_cancel_7 | _ \* _ \* _ \* _ \* _ \* _ \* ?H' \* _ => unify H H'; apply hsimpl_cancel_7
| _ \* _ \* _ \* _ \* _ \* _ \* _ \* H \* _ => apply hsimpl_cancel_8 | _ \* _ \* _ \* _ \* _ \* _ \* _ \* ?H' \* _ => unify H H'; apply hsimpl_cancel_8
| _ \* _ \* _ \* _ \* _ \* _ \* _ \* _ \* H \* _ => apply hsimpl_cancel_9 | _ \* _ \* _ \* _ \* _ \* _ \* _ \* _ \* ?H' \* _ => unify H H'; apply hsimpl_cancel_9
| _ \* _ \* _ \* _ \* _ \* _ \* _ \* _ \* _ \* H \* _ => apply hsimpl_cancel_10 | _ \* _ \* _ \* _ \* _ \* _ \* _ \* _ \* _ \* ?H' \* _ => unify H H'; apply hsimpl_cancel_10
end. end.
Ltac hsimpl_find_data l HL cont := Ltac hsimpl_find_data l HL cont :=
...@@ -2421,7 +2421,7 @@ Lemma Group_add : forall a (x:a) A `{Inhab A} (M:map a A) (G:htype A a) X, ...@@ -2421,7 +2421,7 @@ Lemma Group_add : forall a (x:a) A `{Inhab A} (M:map a A) (G:htype A a) X,
Heapdata G -> Heapdata G ->
Group G M \* (x ~> G X) ==> Group G (M[x:=X]). Group G M \* (x ~> G X) ==> Group G (M[x:=X]).
Proof using. Proof using.
intros. hchange~ Group_add_fresh. hsimpl. hsimpl. intros. hchange~ Group_add_fresh. hsimpl.
Qed. Qed.
(* LATER: prove reciprocal to Group_add (* LATER: prove reciprocal to Group_add
...@@ -2575,7 +2575,7 @@ Proof using. ...@@ -2575,7 +2575,7 @@ Proof using.
rewrite star_assoc. exists~ h1 h2. rewrite star_assoc. exists~ h1 h2.
auto. auto.
intros x. hchange (Qle' x). hchange~ (Qle x). intros x. hchange (Qle' x). hchange~ (Qle x).
set (H' := \GC) at 1 2. hsimpl; subst H'; affine. hchange (@hsimpl_gc (\GC \* \GC)). affine. hsimpl.
apply~ local_erase. apply~ local_erase.
Qed. Qed.
......
...@@ -108,8 +108,8 @@ Lemma iter_spec_rest : forall A (l:list A) (f:func), ...@@ -108,8 +108,8 @@ Lemma iter_spec_rest : forall A (l:list A) (f:func),
Proof using. Proof using.
=>> M. xapp~ (fun k => Hexists r, \[l = k ++ r] \* I r). =>> M. xapp~ (fun k => Hexists r, \[l = k ++ r] \* I r).
{ =>> E. xpull ;=> r' E'. subst l. { =>> E. xpull ;=> r' E'. subst l.
lets: app_cancel_l E'. subst r'. lets: app_cancel_l E'. subst r'.
xapp. xsimpl~. xsimpl~. } xapp. xsimpl~. }
{ xpull ;=>> E. rewrites (>> self_eq_app_l_inv E). xsimpl~. } { xpull ;=>> E. rewrites (>> self_eq_app_l_inv E). xsimpl~. }
Qed. (* TODO: beautify this proof *) Qed. (* TODO: beautify this proof *)
......
...@@ -14,6 +14,6 @@ remove: [make "uninstall"] ...@@ -14,6 +14,6 @@ remove: [make "uninstall"]
depends: [ depends: [
"ocamlbuild" {build} "ocamlbuild" {build}
"pprint" "pprint"
"coq" {= "8.6"} "coq" {>= "8.6"}
"coq-tlc" {>= "20161010"} "coq-tlc" {>= "20161010"}
] ]
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment