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
Jonas Kastberg
iris
Commits
394075cc
Commit
394075cc
authored
Nov 20, 2018
by
Robbert Krebbers
Browse files
Do not manually apply TC instances using `refine`.
After Coq PR #7825 this will create unwanted evars.
parent
0aa8c098
Changes
1
Hide whitespace changes
Inline
Side-by-side
theories/proofmode/ltac_tactics.v
View file @
394075cc
...
...
@@ -601,7 +601,7 @@ Ltac iSpecializePat_go H1 pats :=
fail
"iSpecialize:"
H1
"not found"
|
solve_to_wand
H1
|
lazymatch
m
with
|
GSpatial
=>
notypeclasses
refine
(
add_modal_id
_
_
)
|
GSpatial
=>
class_apply
add_modal_id
|
GModal
=>
iSolveTC
||
fail
"iSpecialize: goal not a modality"
end
|
pm_reflexivity
||
...
...
Write
Preview
Supports
Markdown
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