Commit 614533e1 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan

Bump Iris, fix compatibility with Iris/Coq.

parent ac32c3e2
......@@ -10,6 +10,6 @@ build: [make "-j%{jobs}%"]
install: [make "install"]
remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/iris_time" ]
depends: [
"coq-iris" { (= "dev.2019-09-20.0.b958d569") | (= "dev") }
"coq-iris" { (= "dev.2019-11-07.0.c3e6385b") | (= "dev") }
"coq-tlc" { (= "20181116") | (= "dev") }
]
......@@ -677,7 +677,7 @@ Section Safety.
specialize (Hsafe _ _ _ eq_refl Hsteps (elem_of_list_here _ _)). clear Hsteps.
destruct Hsafe as [ Hval | Hred ].
+ left. by eapply fill_val.
+ destruct (to_val e') eqn:Hnotval ; first by eauto. right.
+ destruct (to_val e') eqn:Hnotval; [by left; eauto|]. right.
destruct Hred as (κ & _ & σ'' & efs & [ K2 e'2 e''2 Efill _ Hstep ]) ; simpl in *.
eapply step_by_val in Efill as Efill' ; try eassumption ; destruct Efill' as [K' ->].
rewrite fill_app in Efill ; apply fill_inj in Efill as ->.
......
......@@ -186,8 +186,6 @@ Proof. destruct e=>//=. by intros [= <-]. Qed.
Global Instance of_val_inj : Inj (=) (=) of_val.
Proof. intros ??. congruence. Qed.
Global Instance mach_int_eq_dec : EqDecision base_lit.
Global Instance base_lit_eq_dec : EqDecision base_lit.
Proof. solve_decision. Defined.
Global Instance un_op_eq_dec : EqDecision un_op.
......
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