Commit d7fd78fd authored by Robbert Krebbers's avatar Robbert Krebbers

Fix compilation with Coq master and bump Iris.

parent 090c2bd0
Pipeline #16826 passed with stage
in 15 minutes and 2 seconds
...@@ -9,5 +9,5 @@ build: [make "-j%{jobs}%"] ...@@ -9,5 +9,5 @@ build: [make "-j%{jobs}%"]
install: [make "install"] install: [make "install"]
remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/iris-c" ] remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/iris-c" ]
depends: [ depends: [
"coq-iris" { (= "dev.2019-05-01.1.c7164230") | (= "dev") } "coq-iris" { (= "dev.2019-05-20.1.eb3117bd") | (= "dev") }
] ]
...@@ -87,4 +87,4 @@ Section U. ...@@ -87,4 +87,4 @@ Section U.
Proof. by rewrite /FromModal. Qed. Proof. by rewrite /FromModal. Qed.
End U. End U.
Hint Extern 1 (environments.envs_entails _ (U _)) => iModIntro. Hint Extern 1 (environments.envs_entails _ (U _)) => iModIntro : core.
...@@ -494,7 +494,7 @@ Section flock. ...@@ -494,7 +494,7 @@ Section flock.
Lemma big_sepM_own_frag {A B : Type} {C} `{EqDecision A, Countable A} Lemma big_sepM_own_frag {A B : Type} {C} `{EqDecision A, Countable A}
`{inG Σ (authR (gmapUR A C))} (f : B C) (m : gmap A B) (γ : gname) : `{inG Σ (authR (gmapUR A C))} (f : B C) (m : gmap A B) (γ : gname) :
own γ ( ) - own γ ( ) -
own γ ( (f <$> m)) - [ map] ix m, own γ ( {[ i := f x ]}). own γ ( (f <$> m : gmap A C)) - [ map] ix m, own γ ( {[ i := f x ]}).
Proof. Proof.
simple refine (map_ind (λ m, _)%I _ _ m); simpl. simple refine (map_ind (λ m, _)%I _ _ m); simpl.
- iIntros "He". rewrite fmap_empty big_sepM_empty. iSplit; eauto. - iIntros "He". rewrite fmap_empty big_sepM_empty. iSplit; eauto.
......
...@@ -745,8 +745,8 @@ Section proofmode. ...@@ -745,8 +745,8 @@ Section proofmode.
Global Instance into_pure_mapsto_nil cl q : IntoPure (cl C{q} []) True. Global Instance into_pure_mapsto_nil cl q : IntoPure (cl C{q} []) True.
Proof. done. Qed. Proof. done. Qed.
Global Instance from_pure_mapsto_nil a cl q : FromPure a (cl C{q} []) True | 100. Global Instance from_pure_mapsto_nil cl q : FromPure false (cl C{q} []) True | 100.
Proof. by rewrite /FromPure bi.affinely_if_elim. Qed. Proof. done. Qed.
Global Instance into_sep_mapsto_list_cons cl q vs v vs' : Global Instance into_sep_mapsto_list_cons cl q vs v vs' :
IsCons vs v vs' IsCons vs v vs'
......
...@@ -216,8 +216,8 @@ Arguments wand_denv_interp {_ _} _ !_ _%I /. ...@@ -216,8 +216,8 @@ Arguments wand_denv_interp {_ _} _ !_ _%I /.
Section denv. Section denv.
Context `{cmonadG Σ}. Context `{cmonadG Σ}.
Local Arguments Q_to_Qp : simpl never. Local Arguments Q_to_Qp : simpl never.
Hint Resolve Q_plus_nonneg. Hint Resolve Q_plus_nonneg : core.
Hint Resolve Q_div_nonneg. Hint Resolve Q_div_nonneg : core.
(* Well-formedness stuff *) (* Well-formedness stuff *)
Ltac simplify := Ltac simplify :=
......
...@@ -83,21 +83,21 @@ End forward. ...@@ -83,21 +83,21 @@ End forward.
Section forward_spec. Section forward_spec.
Context `{cmonadG Σ}. Context `{cmonadG Σ}.
Hint Extern 2 (_ `prefix_of` _) => etrans; [eassumption|]. Hint Extern 2 (_ `prefix_of` _) => etrans; [eassumption|] : core.
Hint Extern 0 (0 < 1)%Q => reflexivity. Hint Extern 0 (0 < 1)%Q => reflexivity : core.
Hint Resolve dknown_bool_of_dval_correct. Hint Resolve dknown_bool_of_dval_correct : core.
Hint Resolve dloc_var_of_dval_wf dloc_var_of_dval_correct. Hint Resolve dloc_var_of_dval_wf dloc_var_of_dval_correct : core.
Hint Resolve denv_wf_1_stack_pop denv_wf_2_stack_pop. Hint Resolve denv_wf_1_stack_pop denv_wf_2_stack_pop : core.
Hint Resolve dun_op_eval_Some_wf dun_op_eval_correct. Hint Resolve dun_op_eval_Some_wf dun_op_eval_correct : core.
Hint Resolve dcbin_op_eval_Some_wf dcbin_op_eval_correct. Hint Resolve dcbin_op_eval_Some_wf dcbin_op_eval_correct : core.
Hint Resolve dce_subst_wf'. Hint Resolve dce_subst_wf' : core.
Hint Resolve denv_wf_dval_wf_lookup. Hint Resolve denv_wf_dval_wf_lookup : core.
Hint Resolve denv_wf_insert denv_wf_merge denv_wf_unlock. Hint Resolve denv_wf_insert denv_wf_merge denv_wf_unlock : core.
Hint Resolve denv_wf_delete_full denv_wf_dval_wf_delete_full. Hint Resolve denv_wf_delete_full denv_wf_dval_wf_delete_full : core.
Hint Resolve denv_wf_1_delete_frac_2 denv_wf_2_delete_frac_2. Hint Resolve denv_wf_1_delete_frac_2 denv_wf_2_delete_frac_2 : core.
Hint Resolve denv_wf_frac_wf_delete_frac_2 denv_wf_dval_wf_delete_frac_2. Hint Resolve denv_wf_frac_wf_delete_frac_2 denv_wf_dval_wf_delete_frac_2 : core.
Hint Resolve denv_wf_1_delete_full_2 denv_wf_2_delete_full_2. Hint Resolve denv_wf_1_delete_full_2 denv_wf_2_delete_full_2 : core.
Hint Resolve denv_wf_dval_wf_delete_full_2. Hint Resolve denv_wf_dval_wf_delete_full_2 : core.
Lemma dexpr_eval_wf E de dv : Lemma dexpr_eval_wf E de dv :
dexpr_eval de = Some dv dexpr_wf E de dval_wf E dv. dexpr_eval de = Some dv dexpr_wf E de dval_wf E dv.
...@@ -107,7 +107,7 @@ Section forward_spec. ...@@ -107,7 +107,7 @@ Section forward_spec.
| H : _, _ |- _ => efeed specialize H; [done..|] | H : _, _ |- _ => efeed specialize H; [done..|]
end; naive_solver. end; naive_solver.
Qed. Qed.
Hint Resolve dexpr_eval_wf. Hint Resolve dexpr_eval_wf : core.
Lemma forward_aux_length E de ms ms' mNew dv n : Lemma forward_aux_length E de ms ms' mNew dv n :
forward_aux E n ms de = Some (ms', mNew, dv) length ms = length ms'. forward_aux E n ms de = Some (ms', mNew, dv) length ms = length ms'.
...@@ -147,7 +147,7 @@ Section forward_spec. ...@@ -147,7 +147,7 @@ Section forward_spec.
forward_aux E n ms de = Some (ms', mNew, dv) forward_aux E n ms de = Some (ms', mNew, dv)
Forall (denv_wf E) ms dcexpr_wf E de dval_wf E dv. Forall (denv_wf E) ms dcexpr_wf E de dval_wf E dv.
Proof. intros; eapply denv_wf_all_wf_forward_aux; eauto. Qed. Proof. intros; eapply denv_wf_all_wf_forward_aux; eauto. Qed.
Hint Resolve denv_wf_1_forward_aux denv_wf_2_forward_aux denv_wf_dval_wf_forward_aux. Hint Resolve denv_wf_1_forward_aux denv_wf_2_forward_aux denv_wf_dval_wf_forward_aux : core.
Lemma denv_wf_1_forward E de m m' mNew dv n : Lemma denv_wf_1_forward E de m m' mNew dv n :
forward E n m de = Some (m', mNew, dv) forward E n m de = Some (m', mNew, dv)
...@@ -167,7 +167,7 @@ Section forward_spec. ...@@ -167,7 +167,7 @@ Section forward_spec.
Proof. Proof.
rewrite /forward. intros; repeat (case_match || simplify_option_eq); eauto. rewrite /forward. intros; repeat (case_match || simplify_option_eq); eauto.
Qed. Qed.
Hint Resolve denv_wf_1_forward denv_wf_2_forward denv_wf_dval_wf_forward. Hint Resolve denv_wf_1_forward denv_wf_2_forward denv_wf_dval_wf_forward : core.
Lemma dexpr_eval_correct E de dv : Lemma dexpr_eval_correct E de dv :
dexpr_eval de = Some dv dexpr_eval de = Some dv
......
...@@ -21,8 +21,8 @@ Arguments PropIntoDEnv {_ _} _ _ _%I _%I _. ...@@ -21,8 +21,8 @@ Arguments PropIntoDEnv {_ _} _ _ _%I _%I _.
Section tactics. Section tactics.
Context `{cmonadG Σ}. Context `{cmonadG Σ}.
Implicit Types P Q : iProp Σ. Implicit Types P Q : iProp Σ.
Hint Extern 0 (0 < _)%Q => apply Qp_prf. Hint Extern 0 (0 < _)%Q => apply Qp_prf : core.
Hint Extern 2 (_ `prefix_of` _) => etrans; [eassumption|]. Hint Extern 2 (_ `prefix_of` _) => etrans; [eassumption|] : core.
Global Instance prop_into_denv_default E P m : PropIntoDEnv E E P P m m | 100. Global Instance prop_into_denv_default E P m : PropIntoDEnv E E P P m m | 100.
Proof. by split. Qed. Proof. by split. Qed.
......
...@@ -265,23 +265,23 @@ End vcg. ...@@ -265,23 +265,23 @@ End vcg.
Section vcg_spec. Section vcg_spec.
Context `{cmonadG Σ}. Context `{cmonadG Σ}.
Hint Extern 2 (_ `prefix_of` _) => etrans; [eassumption|]. Hint Extern 2 (_ `prefix_of` _) => etrans; [eassumption|] : core.
Hint Extern 0 (0 < 1)%Q => reflexivity. Hint Extern 0 (0 < 1)%Q => reflexivity : core.
Hint Resolve dknown_bool_of_dval_correct. Hint Resolve dknown_bool_of_dval_correct : core.
Hint Resolve dloc_var_of_dval_wf dloc_var_of_dval_correct. Hint Resolve dloc_var_of_dval_wf dloc_var_of_dval_correct : core.
Hint Resolve denv_wf_1_stack_pop denv_wf_2_stack_pop. Hint Resolve denv_wf_1_stack_pop denv_wf_2_stack_pop : core.
Hint Resolve dun_op_eval_Some_wf dun_op_eval_correct. Hint Resolve dun_op_eval_Some_wf dun_op_eval_correct : core.
Hint Resolve dcbin_op_eval_Some_wf dcbin_op_eval_correct. Hint Resolve dcbin_op_eval_Some_wf dcbin_op_eval_correct : core.
Hint Resolve dce_subst_wf'. Hint Resolve dce_subst_wf' : core.
Hint Resolve denv_wf_dval_wf_lookup. Hint Resolve denv_wf_dval_wf_lookup : core.
Hint Resolve denv_wf_insert denv_wf_merge denv_wf_unlock. Hint Resolve denv_wf_insert denv_wf_merge denv_wf_unlock : core.
Hint Resolve denv_wf_delete_full denv_wf_dval_wf_delete_full. Hint Resolve denv_wf_delete_full denv_wf_dval_wf_delete_full : core.
Hint Resolve denv_wf_1_delete_frac_2 denv_wf_2_delete_frac_2. Hint Resolve denv_wf_1_delete_frac_2 denv_wf_2_delete_frac_2 : core.
Hint Resolve denv_wf_frac_wf_delete_frac_2 denv_wf_dval_wf_delete_frac_2. Hint Resolve denv_wf_frac_wf_delete_frac_2 denv_wf_dval_wf_delete_frac_2 : core.
Hint Resolve denv_wf_1_delete_full_2 denv_wf_2_delete_full_2. Hint Resolve denv_wf_1_delete_full_2 denv_wf_2_delete_full_2 : core.
Hint Resolve denv_wf_dval_wf_delete_full_2. Hint Resolve denv_wf_dval_wf_delete_full_2 : core.
Hint Resolve dexpr_eval_wf. Hint Resolve dexpr_eval_wf : core.
Hint Resolve denv_wf_1_forward denv_wf_2_forward denv_wf_dval_wf_forward. Hint Resolve denv_wf_1_forward denv_wf_2_forward denv_wf_dval_wf_forward : core.
Lemma vcg_continuation_correct Φ E m dv : Lemma vcg_continuation_correct Φ E m dv :
denv_wf E m dval_wf E dv denv_wf E m dval_wf E dv
......
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