Commit f774d316 authored by Robbert Krebbers's avatar Robbert Krebbers

Extend iClear to handle clearing of Coq-level variables.

parent 06fad70e
Pipeline #2728 passed with stage
in 9 minutes and 27 seconds
......@@ -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
......
......@@ -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) :=
......
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