Commit 010efcf2 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan

Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coq

parents 5657f5ca 272535e4
......@@ -188,8 +188,13 @@ _introduction patterns_:
- `?` : create an anonymous hypothesis.
- `_` : remove the hypothesis.
- `$` : frame the hypothesis in the goal.
- `[ipat ipat]` : (separating) conjunction elimination.
- `[ipat|ipat]` : disjunction elimination.
- `[ipat1 ipat2]` : (separating) conjunction elimination. In order to eliminate
conjunctions `P ∧ Q` in the spatial context, one of the following conditions
should hold:
+ Either the proposition `P` or `Q` should be persistent.
+ Either `ipat1` or `ipat2` should be `_`, which results in one of the
conjuncts to be thrown away.
- `[ipat1|ipat2]` : disjunction elimination.
- `[]` : false elimination.
- `%` : move the hypothesis to the pure Coq context (anonymously).
- `# ipat` : move the hypothesis to the persistent context.
......
......@@ -778,7 +778,8 @@ Local Tactic Notation "iExistDestruct" constr(H)
(** * Always *)
Tactic Notation "iAlways":=
iStartProof;
apply tac_always_intro; env_cbv.
apply tac_always_intro; env_cbv
|| fail "iAlways: the goal is not an always modality".
(** * Later *)
Tactic Notation "iNext" open_constr(n) :=
......
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