From 93950e2298f78a94a1864b1b998cf04432699016 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Lennard=20G=C3=A4her?= <gaeher@mpi-sws.org>
Date: Sat, 26 Nov 2022 11:06:27 +0100
Subject: [PATCH] bump iris
---
semantics.opam | 2 +-
theories/program_logics/heap_lang/proofmode.v | 14 +++++++-------
theories/program_logics/reloc/proofmode.v | 14 +++++++-------
3 files changed, 15 insertions(+), 15 deletions(-)
diff --git a/semantics.opam b/semantics.opam
index 28595fc..6324efb 100644
--- a/semantics.opam
+++ b/semantics.opam
@@ -10,7 +10,7 @@ version: "dev"
depends: [
"coq" { (>= "8.13" & < "8.17~") | (= "dev") }
- "coq-iris-heap-lang" { (= "dev.2022-09-29.0.b335afaf") | (= "dev") }
+ "coq-iris-heap-lang" { (= "dev.2022-11-24.2.5b5d3f4d") | (= "dev") }
"coq-equations" { (= "1.2.4+8.13") | (= "1.3+8.14") | (= "1.3+8.15") | (= "1.3+8.16") }
"coq-autosubst" { (= "1.7") | (= "dev") }
]
diff --git a/theories/program_logics/heap_lang/proofmode.v b/theories/program_logics/heap_lang/proofmode.v
index 77631c1..46da3d4 100644
--- a/theories/program_logics/heap_lang/proofmode.v
+++ b/theories/program_logics/heap_lang/proofmode.v
@@ -75,10 +75,10 @@ Tactic Notation "wp_pure" open_constr(efoc) :=
reshape_expr e ltac:(fun K e' =>
unify e' efoc;
eapply (tac_wp_pure _ _ _ _ _ K e');
- [iSolveTC (* PureExec *)
+ [tc_solve (* PureExec *)
|try solve_vals_compare_safe (* The pure condition for PureExec --
handles trivial goals, including [vals_compare_safe] *)
- |iSolveTC (* IntoLaters *)
+ |tc_solve (* IntoLaters *)
|wp_finish (* new goal *)
])
|| fail "wp_pure: cannot find" efoc "in" e "or" efoc "is not a redex"
@@ -322,14 +322,14 @@ Tactic Notation "wp_alloc" ident(l) "as" constr(H) :=
first
[reshape_expr e ltac:(fun K e' => eapply (tac_wp_alloc _ _ _ _ _ Htmp K))
|fail 1 "wp_alloc: cannot find 'Alloc' in" e];
- [iSolveTC
+ [tc_solve
|finish ()]
in
let process_array _ :=
first
[reshape_expr e ltac:(fun K e' => eapply (tac_wp_allocN _ _ _ _ _ Htmp K))
|fail 1 "wp_alloc: cannot find 'Alloc' in" e];
- [idtac|iSolveTC
+ [idtac|tc_solve
|finish ()]
in (process_single ()) || (process_array ())
| _ => fail "wp_alloc: not a 'wp'"
@@ -348,7 +348,7 @@ Tactic Notation "wp_free" :=
first
[reshape_expr e ltac:(fun K e' => eapply (tac_wp_free _ _ _ _ _ _ K))
|fail 1 "wp_free: cannot find 'Free' in" e];
- [iSolveTC
+ [tc_solve
|solve_mapsto ()
|pm_reduce; wp_finish]
| _ => fail "wp_free: not a 'wp'"
@@ -364,7 +364,7 @@ Tactic Notation "wp_load" :=
first
[reshape_expr e ltac:(fun K e' => eapply (tac_wp_load _ _ _ _ _ _ K))
|fail 1 "wp_load: cannot find 'Load' in" e];
- [iSolveTC
+ [tc_solve
|solve_mapsto ()
|wp_finish]
| _ => fail "wp_load: not a 'wp'"
@@ -380,7 +380,7 @@ Tactic Notation "wp_store" :=
first
[reshape_expr e ltac:(fun K e' => eapply (tac_wp_store _ _ _ _ _ _ K))
|fail 1 "wp_store: cannot find 'Store' in" e];
- [iSolveTC
+ [tc_solve
|solve_mapsto ()
|pm_reduce; first [wp_seq|wp_finish]]
| _ => fail "wp_store: not a 'wp'"
diff --git a/theories/program_logics/reloc/proofmode.v b/theories/program_logics/reloc/proofmode.v
index 2bfc11f..f9e051d 100644
--- a/theories/program_logics/reloc/proofmode.v
+++ b/theories/program_logics/reloc/proofmode.v
@@ -113,9 +113,9 @@ Tactic Notation "src_pure" open_constr(ef) :=
reshape_expr e ltac:(fun K e' =>
unify e' ef;
eapply (tac_src_pure (fill K' e) (K++K') e');
- [by rewrite ?fill_app | iSolveTC | ..])
+ [by rewrite ?fill_app | tc_solve | ..])
end;
- [iSolveTC || fail "src_pure: cannot eliminate modality in the goal"
+ [tc_solve || fail "src_pure: cannot eliminate modality in the goal"
|solve_ndisj || fail "src_pure: cannot prove 'nclose specN ⊆ ?'"
|iAssumptionCore || fail "src_pure: cannot find the RHS"
|try (exact I || reflexivity) (* ψ *)
@@ -191,11 +191,11 @@ Qed.
Tactic Notation "src_store" :=
iStartProof;
eapply (tac_src_store);
- [iSolveTC || fail "src_store: cannot eliminate modality in the goal"
+ [tc_solve || fail "src_store: cannot eliminate modality in the goal"
|solve_ndisj || fail "src_store: cannot prove 'nclose specN ⊆ ?'"
|iAssumptionCore || fail "src_store: cannot find RHS"
|src_bind_helper
- |iSolveTC || fail "src_store: cannot convert the argument to a value"
+ |tc_solve || fail "src_store: cannot convert the argument to a value"
|simpl; reflexivity || fail "src_store: this should not happen"
|iAssumptionCore || fail "src_store: cannot find '? ↦ₛ ?'"
|pm_reduce (* new goal *)].
@@ -243,7 +243,7 @@ Qed.
Tactic Notation "src_load" :=
iStartProof;
eapply (tac_src_load);
- [iSolveTC || fail "src_load: cannot eliminate modality in the goal"
+ [tc_solve || fail "src_load: cannot eliminate modality in the goal"
|solve_ndisj || fail "src_load: cannot prove 'nclose specN ⊆ ?'"
|iAssumptionCore || fail "src_load: cannot find the RHS"
|src_bind_helper
@@ -298,11 +298,11 @@ Tactic Notation "src_alloc" ident(l) "as" constr(H) :=
| (iIntros H; src_normalise) || fail 1 "src_alloc:" H "not correct intro pattern" ] in
iStartProof;
eapply (tac_src_alloc);
- [iSolveTC || fail "src_alloc: cannot eliminate modality in the goal"
+ [tc_solve || fail "src_alloc: cannot eliminate modality in the goal"
|solve_ndisj || fail "src_alloc: cannot prove 'nclose specN ⊆ ?'"
|iAssumptionCore || fail "src_alloc: cannot find the RHS"
|src_bind_helper
- |iSolveTC || fail "src_alloc: expressions is not a value"
+ |tc_solve || fail "src_alloc: expressions is not a value"
|finish ()
(* new goal *)].
--
GitLab