Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Marianna Rapoport
iris-coq
Commits
e1764691
Commit
e1764691
authored
Jul 12, 2017
by
Robbert Krebbers
Browse files
Fix typo.
parent
0abc7f0f
Changes
1
Hide whitespace changes
Inline
Side-by-side
theories/proofmode/class_instances.v
View file @
e1764691
...
...
@@ -392,7 +392,7 @@ Proof. intros. by rewrite /FromAnd big_opL_app always_and_sep_l. Qed.
(* TODO: Worst case there could be a lot of backtracking on these instances,
try to refactor. *)
Global
Instance
is_op_pair
{
A
B
:
cmraT
}
(
a
b1
b2
:
A
)
(
a'
b1'
b2'
:
B
)
:
IsOp
'
a
b1
b2
→
IsOp
a'
b1'
b2'
→
IsOp'
(
a
,
a'
)
(
b1
,
b1'
)
(
b2
,
b2'
).
IsOp
a
b1
b2
→
IsOp
a'
b1'
b2'
→
IsOp'
(
a
,
a'
)
(
b1
,
b1'
)
(
b2
,
b2'
).
Proof
.
by
constructor
.
Qed
.
Global
Instance
is_op_pair_persistent_l
{
A
B
:
cmraT
}
(
a
:
A
)
(
a'
b1'
b2'
:
B
)
:
Persistent
a
→
IsOp
a'
b1'
b2'
→
IsOp'
(
a
,
a'
)
(
a
,
b1'
)
(
a
,
b2'
).
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a 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