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
Iris
Iris
Commits
1560d168
Commit
1560d168
authored
Feb 15, 2018
by
Jacques-Henri Jourdan
Browse files
Do not call [eval hnf] in iIntoValid.
parent
96ab3ac7
Pipeline
#6790
passed with stage
in 14 minutes and 40 seconds
Changes
1
Pipelines
1
Hide whitespace changes
Inline
Side-by-side
theories/proofmode/tactics.v
View file @
1560d168
...
...
@@ -620,7 +620,7 @@ a goal [P] for non-dependent arguments [x_i : P]. *)
Tactic
Notation
"iIntoValid"
open_constr
(
t
)
:
=
let
rec
go
t
:
=
let
tT
:
=
type
of
t
in
lazymatch
eval
hnf
in
tT
with
lazymatch
tT
with
|
?P
→
?Q
=>
let
H
:
=
fresh
in
assert
P
as
H
;
[|
go
uconstr
:
(
t
H
)
;
clear
H
]
|
∀
_
:
?T
,
_
=>
(* Put [T] inside an [id] to avoid TC inference from being invoked. *)
...
...
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