Commit 58a49c2a by Jacques-Henri Jourdan

Wrong kind of comment.

parent 411142ee
 ... ... @@ -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. ... ...
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!