From 5b6ab906fb6281ef7550c4e710c9b348fb83382b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Arma=C3=ABl=20Gu=C3=A9neau?= <armael.gueneau@ens-lyon.org>
Date: Fri, 1 Oct 2021 14:32:24 +0200
Subject: [PATCH] Implement a more conservative ident_for_pat_default, which
simplifies the iAndDestruct case
---
iris/proofmode/ltac_tactics.v | 28 +++++++++++-----------------
1 file changed, 11 insertions(+), 17 deletions(-)
diff --git a/iris/proofmode/ltac_tactics.v b/iris/proofmode/ltac_tactics.v
index 41453a3a7..7d76d952d 100644
--- a/iris/proofmode/ltac_tactics.v
+++ b/iris/proofmode/ltac_tactics.v
@@ -1476,7 +1476,8 @@ Tactic Notation "iModCore" constr(H) "as" constr(H') :=
to the intro-pattern [pat], when trying to avoid extra renamings. These
mainly look whether the pattern is a name, and use that name in that case.
Otherwise, [ident_for_pat] generates a fresh name (a safe option), and
- [ident_for_pat_default] uses the [default] name that it was provided.
+ [ident_for_pat_default] uses the [default] name that it was provided if
+ it is an anonymous name.
*)
Local Ltac ident_for_pat pat :=
lazymatch pat with
@@ -1487,7 +1488,11 @@ Local Ltac ident_for_pat pat :=
Local Ltac ident_for_pat_default pat default :=
lazymatch pat with
| IIdent ?x => x
- | _ => default
+ | _ =>
+ lazymatch default with
+ | IAnon _ => default
+ | _ => let x := iFresh in x
+ end
end.
(** [pat0] is the unparsed pattern, and is only used in error messages *)
@@ -1526,22 +1531,11 @@ Local Ltac iDestructHypGo Hz pat0 pat :=
rename_by_string x s;
iDestructHypGo y pat0 pat2
| IList [[?pat1; ?pat2]] =>
- (* We have to take care of not using the same name for the two hypotheses.
- Furthermore, we can only reuse the name [Hz] for the first hypothesis,
- on which we recurse first.
-
- One tricky case is iDestruct "H" as "[? H]": here, we cannot reuse the
- name "H" for the first hypothesis, as it would clash with the chosen
- name for the second one. Hence, we need to compute the second name
- first, and check it against [Hz] to know if it can be reused.
- *)
+ (* We have to take care of not using the same name for the two hypotheses:
+ [ident_for_pat_default] will thus only reuse [Hz] (which could in principle
+ clash with a name from [pat2]) if it is an anonymous name. *)
+ let x1 := ident_for_pat_default pat1 Hz in
let x2 := ident_for_pat pat2 in
- let x1 :=
- lazymatch x2 with
- | Hz => ident_for_pat pat1
- | _ => ident_for_pat_default pat1 Hz
- end
- in
iAndDestruct Hz as x1 x2;
iDestructHypGo x1 pat0 pat1; iDestructHypGo x2 pat0 pat2
| IList [_ :: _ :: _] => fail "iDestruct:" pat0 "has too many conjuncts"
--
GitLab