From f774d316a0c3f62f1bfc908126aab900e7d5cb08 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 27 Sep 2016 11:33:42 +0200
Subject: [PATCH] Extend iClear to handle clearing of Coq-level variables.
---
ProofMode.md | 5 +++--
proofmode/tactics.v | 2 ++
2 files changed, 5 insertions(+), 2 deletions(-)
diff --git a/ProofMode.md b/ProofMode.md
index de5340bf9..74e0b0d1d 100644
--- a/ProofMode.md
+++ b/ProofMode.md
@@ -23,8 +23,9 @@ Context management
- `iIntros (x1 ... xn) "ipat1 ... ipatn"` : introduce universal quantifiers
using Coq introduction patterns `x1 ... xn` and implications/wands using proof
mode introduction patterns `ipat1 ... ipatn`.
-- `iClear "H1 ... Hn"` : clear the hypothesis `H1 ... Hn`. The symbol `★` can
- be used to clear entire spatial context.
+- `iClear (x1 ... xn) "H1 ... Hn"` : clear the hypothesis `H1 ... Hn` as well as
+ the Coq level hypotheses/variables `x1 ... xn`. The symbol `★` can be used to
+ clear entire spatial context.
- `iRevert (x1 ... xn) "H1 ... Hn"` : revert the proof mode hypotheses
`H1 ... Hn` into wands, as well as the Coq level hypotheses/variables
`x1 ... xn` into universal quantifiers. The symbol `★` can be used to revert
diff --git a/proofmode/tactics.v b/proofmode/tactics.v
index 1fabcf66a..7ee2bb6eb 100644
--- a/proofmode/tactics.v
+++ b/proofmode/tactics.v
@@ -66,6 +66,8 @@ Tactic Notation "iClear" constr(Hs) :=
[env_cbv; reflexivity || fail "iClear:" H "not found"|go Hs]
end in
let Hs := words Hs in go Hs.
+Tactic Notation "iClear" "(" ident_list(xs) ")" constr(Hs) :=
+ iClear Hs; clear xs.
(** * Assumptions *)
Tactic Notation "iExact" constr(H) :=
--
GitLab