Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
What's new
10
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Open sidebar
Iris
stdpp
Commits
046dfe31
Commit
046dfe31
authored
Mar 01, 2017
by
Ralf Jung
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
speed up f_equiv by doing reflexivity less often
parent
10db208c
Pipeline
#3975
passed with stage
in 5 minutes and 9 seconds
Changes
2
Pipelines
1
Hide whitespace changes
Inline
Side-by-side
Showing
2 changed files
with
1 addition
and
2 deletions
+1
-2
theories/list.v
theories/list.v
+1
-1
theories/tactics.v
theories/tactics.v
+0
-1
No files found.
theories/list.v
View file @
046dfe31
...
...
@@ -3113,7 +3113,7 @@ Section mapM.
(∀ x y, f y = Some x → y = g x) → mapM f k = Some l → k = g <$> l.
Proof.
intros Hgf. revert l; induction k as [|??]; intros [|??] ?;
simplify_option_eq; f_equiv; eauto.
simplify_option_eq;
try
f_equiv; eauto.
Qed.
End mapM.
...
...
theories/tactics.v
View file @
046dfe31
...
...
@@ -272,7 +272,6 @@ when having [Proper (equiv ==> dist) f] and [Proper (dist ==> dist) f], it will
favor the second because the relation (dist) stays the same. *)
Ltac
f_equiv
:
=
match
goal
with
|
_
=>
reflexivity
|
|-
pointwise_relation
_
_
_
_
=>
intros
?
(* We support matches on both sides, *if* they concern the same variable, or
variables in some relation. *)
...
...
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