From f511129c372080b2ed6edb4fdbc07e31dcb68cb4 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 11 Jul 2016 15:31:03 +0200
Subject: [PATCH] ProofMode.md: typos
---
ProofMode.md | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/ProofMode.md b/ProofMode.md
index 8ffaa46bc..6ab598f0d 100644
--- a/ProofMode.md
+++ b/ProofMode.md
@@ -114,7 +114,7 @@ introduction patterns:
- `# ipat` : move the hypothesis to the persistent context.
- `%` : move the hypothesis to the pure Coq context (anonymously).
- `[ipat ipat]` : (separating) conjunction elimination.
-- `|ipat|ipat]` : disjunction elimination.
+- `[ipat|ipat]` : disjunction elimination.
- `[]` : false elimination.
Apart from this, there are the following introduction patterns that can only
@@ -186,7 +186,7 @@ Many of the proof mode tactics (such as `iDestruct`, `iApply`, `iRewrite`) can
take both hypotheses and lemmas, and allow one to instantiate universal
quantifiers and implications/wands of these hypotheses/lemmas on the fly.
-The syntax for the arguments, called _proof mode terms_ of these tactics is:
+The syntax for the arguments, called _proof mode terms_, of these tactics is:
(H $! t1 ... tn with "spat1 .. spatn")
--
GitLab