From 461c88d6f1284483f94e973812c132fa76af011c Mon Sep 17 00:00:00 2001
From: Robbert Krebbers
Date: Tue, 18 Feb 2020 22:13:35 +0100
Subject: [PATCH] And more useless new lines.

docs/proof_mode.md  7 +
1 file changed, 1 insertion(+), 6 deletions()
diff git a/docs/proof_mode.md b/docs/proof_mode.md
index 00dd50b06..a80b31ff3 100644
 a/docs/proof_mode.md
+++ b/docs/proof_mode.md
@@ 108,17 +108,13 @@ Separation logicspecific tactics
 `iFrame (t1 .. tn) "selpat"` : cancel the Coq terms (or Coq hypotheses)
`t1 ... tn` and Iris hypotheses given by `selpat` in the goal. The constructs
of the selection pattern have the following meaning:

+ `%` : repeatedly frame hypotheses from the Coq context.
+ `#` : repeatedly frame hypotheses from the intuitionistic context.
+ `∗` : frame as much of the spatial context as possible. (N.B: this
is the unicode symbol `∗`, not the regular asterisk `*`.)

Notice that framing spatial hypotheses makes them disappear, but framing Coq
or intuitionistic hypotheses does not make them disappear.

 This tactic solves the goal if everything in the conclusion has been
 framed.
+ This tactic solves the goal if everything in the conclusion has been framed.
 `iCombine "H1" "H2" as "pat"` : combines `H1 : P1` and `H2 : P2` into
`H: P1 ∗ P2`, then calls `iDestruct H as pat` on the combined hypothesis.
 `iAccu` : solves a goal that is an evar by instantiating it with a all
@@ 176,7 +172,6 @@ Rewriting / simplification
goal / hypotheses given by the selection pattern `selpat`. This is a
shorthand for `iEval (simpl)`.

Iris


GitLab