Commit f028cdeb authored by Ralf Jung's avatar Ralf Jung

bump iris

parent d185a08c
Pipeline #5286 failed with stage
in 5 minutes and 3 seconds
......@@ -11,5 +11,5 @@ build: [make "-j%{jobs}%"]
install: [make "install"]
remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/lrust'" ]
depends: [
"coq-iris" { (= "dev.2017-11-04.0") | (= "dev") }
"coq-iris" { (= "dev.2017-11-07.2") | (= "dev") }
]
......@@ -638,7 +638,7 @@ Proof.
apply: (irreducible_fill (K:=ectx_language.fill K)); first done.
apply prim_head_irreducible; unfold stuck_term.
- inversion 1.
- apply ectxi_language_sub_values.
- apply ectxi_language_sub_redexes_are_values.
intros [] ??; simplify_eq/=; eauto; discriminate_list.
Qed.
......
......@@ -76,7 +76,7 @@ Lemma next_access_head_reductible_ctx e σ σ' a l K :
Proof.
intros Hhead Hred. apply prim_head_reducible.
- eapply (reducible_fill (K:=ectx_language.fill K)), Hred. destruct Hhead; eauto.
- apply ectxi_language_sub_values. intros [] ? ->; inversion Hhead; eauto.
- apply ectxi_language_sub_redexes_are_values. intros [] ? ->; inversion Hhead; eauto.
Qed.
Definition head_reduce_not_to_stuck (e : expr) (σ : state) :=
......
......@@ -160,7 +160,7 @@ Proof.
destruct e; simpl; try done; repeat (case_match; try done);
inversion 1; try (apply val_irreducible; rewrite ?language.to_of_val; naive_solver eauto); [].
rewrite -[stuck_term](fill_empty). apply stuck_irreducible.
- apply ectxi_language_sub_values=> /= Ki e' Hfill.
- apply ectxi_language_sub_redexes_are_values=> /= Ki e' Hfill.
revert He. destruct e; simpl; try done; repeat (case_match; try done);
rewrite ?bool_decide_spec;
destruct Ki; inversion Hfill; subst; clear Hfill;
......
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