From 226b857933a67b2066ff674425c823f6431289c5 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers
Date: Wed, 5 Feb 2020 17:43:41 +0100
Subject: [PATCH] Add proof mode documentation for the `-# pat` intro pattern.
---
docs/proof_mode.md | 4 ++++
1 file changed, 4 insertions(+)
diff --git a/docs/proof_mode.md b/docs/proof_mode.md
index 1767f1a8..019ed731 100644
--- a/docs/proof_mode.md
+++ b/docs/proof_mode.md
@@ -240,6 +240,10 @@ _introduction patterns_:
hypothesis is already in the intuitionistic context, the tactic will still
strip intuitionistic and persistence modalities (it is a no-op if the
hypothesis does not contain such modalities).
+- `-# ipat` : move the hypothesis from the intuitionistic context into the
+ spatial context. If the hypothesis is already in the spatial context, the
+ tactic is a no-op. If the hypothesis is not affine, an `` modality is
+ added to the hypothesis.
- `> ipat` : eliminate a modality (if the goal permits).
Apart from this, there are the following introduction patterns that can only
--
GitLab