From 58a49c2adce21090c1bf2fddb1236f1477ef9b53 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Tue, 13 Feb 2018 12:48:41 +0100
Subject: [PATCH] Wrong kind of comment.
---
theories/proofmode/classes.v | 26 +++++++++++++-------------
1 file changed, 13 insertions(+), 13 deletions(-)
diff --git a/theories/proofmode/classes.v b/theories/proofmode/classes.v
index 2856dd620..409d92274 100644
--- a/theories/proofmode/classes.v
+++ b/theories/proofmode/classes.v
@@ -43,19 +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]. *)
+(** [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