From 418f57db9e5d063e995b98b2e3e85fb93fa76d93 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Tue, 13 Feb 2018 12:40:34 +0100
Subject: [PATCH] More doc about FromPure.

---
 theories/proofmode/classes.v | 13 +++++++++++++
 1 file changed, 13 insertions(+)

diff --git a/theories/proofmode/classes.v b/theories/proofmode/classes.v
index 25e01bcbf..381025699 100644
--- a/theories/proofmode/classes.v
+++ b/theories/proofmode/classes.v
@@ -43,6 +43,19 @@ Proof. by exists φ. Qed.
 Hint Extern 0 (IntoPureT _ _) =>
   notypeclasses refine (into_pureT_hint _ _ _) : typeclass_instances.
 
+(* [FromPure] is used when introducing a pure assertion. It is used by
+   iPure, the "[%]" specialization pattern, and the [with "[%]"]
+   pattern when using [iAssert].
+
+   The [a] Boolean asserts whether we introduce the pure assertion in
+   an affine way or in an absorbing way. When [FromPure true P φ] is
+   derived, then [FromPure false P φ] can always be derived too. We
+   use [true] for specialization patterns and [false] for the [iPure]
+   tactic.
+
+   This Boolean is not needed for [IntoPure], because in the case of
+   [IntoPure], we can have the same behavior by asking that [P] be
+   [Affine]. *)
 Class FromPure {PROP : bi} (a : bool) (P : PROP) (φ : Prop) :=
   from_pure : bi_affinely_if a ⌜φ⌝ ⊢ P.
 Arguments FromPure {_} _ _%I _%type_scope : simpl never.
-- 
GitLab