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
Rice Wine
Iris
Commits
c6c87884
Commit
c6c87884
authored
Feb 15, 2018
by
Jacques-Henri Jourdan
Browse files
Also remove the [cbv zeta].
parent
1560d168
Changes
1
Hide whitespace changes
Inline
Side-by-side
theories/proofmode/tactics.v
View file @
c6c87884
...
...
@@ -628,7 +628,7 @@ Tactic Notation "iIntoValid" open_constr(t) :=
let
e
:
=
fresh
in
evar
(
e
:
id
T
)
;
let
e'
:
=
eval
unfold
e
in
e
in
clear
e
;
go
(
t
e'
)
|
_
=>
let
tT'
:
=
eval
cbv
zeta
in
tT
in
eapply
(
as_valid_1
tT
'
)
;
eapply
(
as_valid_1
tT
)
;
(* Doing [apply _] here fails because that will try to solve all evars
whose type is a typeclass, in dependency order (according to Matthieu).
If one fails, it aborts. However, we rely on progress on the main goal
...
...
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