From 5c942d318e31bd045c59fc098d476817372eca0b Mon Sep 17 00:00:00 2001
From: Dan Frumin <dfrumin@cs.ru.nl>
Date: Wed, 29 Apr 2020 20:55:08 +0200
Subject: [PATCH] better handling of rel_pure_l/r
---
theories/logic/proofmode/tactics.v | 14 ++++++++------
1 file changed, 8 insertions(+), 6 deletions(-)
diff --git a/theories/logic/proofmode/tactics.v b/theories/logic/proofmode/tactics.v
index 511e379..28cd751 100644
--- a/theories/logic/proofmode/tactics.v
+++ b/theories/logic/proofmode/tactics.v
@@ -172,14 +172,15 @@ Tactic Notation "rel_pure_l" open_constr(ef) :=
rel_reshape_cont_l ltac:(fun K e' =>
unify e' ef;
eapply (tac_rel_pure_l K e');
- [reflexivity (** e = fill K e1 *)
- |iSolveTC (** PureClosed Ï• e1 e2 *)
- |try heap_lang.proofmode.solve_vals_compare_safe (** φ *)
+ [reflexivity (** e = fill K e' *)
+ |iSolveTC (** PureClosed Ï• e' e2 *)
+ | .. ]);
+ [try heap_lang.proofmode.solve_vals_compare_safe (** φ *)
|first [left; split; reflexivity (** Here we decide if the mask E is ⊤ *)
| right; reflexivity] (** (m = n ∧ E = ⊤) ∨ (m = 0) *)
|iSolveTC (** IntoLaters *)
|simpl; reflexivity (** eres = fill K e2 *)
- |rel_finish (** new goal *)])
+ |rel_finish (** new goal *)]
|| fail "rel_pure_l: cannot find the reduct".
Tactic Notation "rel_pure_l" := rel_pure_l _.
@@ -191,10 +192,11 @@ Tactic Notation "rel_pure_r" open_constr(ef) :=
eapply (tac_rel_pure_r K e');
[reflexivity (** e = fill K e1 *)
|iSolveTC (** PureClosed Ï• e1 e2 *)
- |try heap_lang.proofmode.solve_vals_compare_safe (** φ *)
+ |..]);
+ [try heap_lang.proofmode.solve_vals_compare_safe (** φ *)
|solve_ndisj || fail 1 "rel_pure_r: cannot solve ↑specN ⊆ ?"
|simpl; reflexivity (** eres = fill K e2 *)
- |rel_finish (** new goal *)])
+ |rel_finish (** new goal *)]
|| fail "rel_pure_r: cannot find the reduct".
Tactic Notation "rel_pure_r" := rel_pure_r _.
--
GitLab