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
George Pirlea
Iris
Commits
3e1c355f
Commit
3e1c355f
authored
Mar 05, 2016
by
Ralf Jung
Browse files
try to speed up set_solver a little
parent
c82719b9
Changes
1
Hide whitespace changes
Inline
Side-by-side
prelude/collections.v
View file @
3e1c355f
...
...
@@ -265,7 +265,7 @@ Ltac set_unfold :=
[set_solver] already. We use the [naive_solver] tactic as a substitute.
This tactic either fails or proves the goal. *)
Tactic
Notation
"set_solver"
"by"
tactic3
(
tac
)
:
=
try
d
on
e
;
try
(
reflexivity
||
eassumpti
on
)
;
intros
;
setoid_subst
;
set_unfold
;
intros
;
setoid_subst
;
...
...
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