Skip to content
GitLab
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Iris
Iris
Commits
b2426163
Commit
b2426163
authored
Feb 13, 2018
by
Jacques-Henri Jourdan
Browse files
Fix doc.
parent
58a49c2a
Pipeline
#6711
passed with stages
in 3 minutes and 47 seconds
Changes
1
Pipelines
1
Hide whitespace changes
Inline
Side-by-side
theories/proofmode/classes.v
View file @
b2426163
...
...
@@ -43,15 +43,15 @@ 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 "[%]"]
(** [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.
use [true] for specialization patterns and [false] for the
[iPureIntro]
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
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment