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
Jonas Kastberg
iris
Commits
df4beedf
Commit
df4beedf
authored
Jun 25, 2018
by
Ralf Jung
Browse files
always use notypeclasses refine
parent
38ba379f
Changes
1
Hide whitespace changes
Inline
Side-by-side
theories/proofmode/ltac_tactics.v
View file @
df4beedf
...
...
@@ -680,7 +680,7 @@ Tactic Notation "iSpecializeCore" open_constr(H)
fail
"iSpecialize:"
H
"not found"
|
iSpecializePat
H
pat
;
[..
|
refine
(
tac_specialize_persistent_helper_done
_
H
_
_
_
)
;
|
notypeclasses
refine
(
tac_specialize_persistent_helper_done
_
H
_
_
_
)
;
pm_reflexivity
]
|
iSolveTC
||
let
Q
:
=
match
goal
with
|-
IntoPersistent
_
?Q
_
=>
Q
end
in
...
...
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