Commit ddd48268 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan
Browse files

Fix typo.

parent 75c98fae
Pipeline #6862 passed with stage
in 10 minutes and 41 seconds
...@@ -630,8 +630,8 @@ Tactic Notation "iIntoValid" open_constr(t) := ...@@ -630,8 +630,8 @@ Tactic Notation "iIntoValid" open_constr(t) :=
in order to make sure we do not unfold [bi_valid]. *) in order to make sure we do not unfold [bi_valid]. *)
let tT := type of t in let tT := type of t in
first first
[ let tT' := eval hnf in tT in go_specilize t tT' [ let tT' := eval hnf in tT in go_specialize t tT'
| let tT' := eval cbv zeta in tT in go_specilize t tT' | let tT' := eval cbv zeta in tT in go_specialize t tT'
| let tT' := eval cbv zeta in tT in | 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 (* Doing [apply _] here fails because that will try to solve all evars
...@@ -641,7 +641,7 @@ Tactic Notation "iIntoValid" open_constr(t) := ...@@ -641,7 +641,7 @@ Tactic Notation "iIntoValid" open_constr(t) :=
elsewhere. With [typeclasses eauto], that seems to work better. *) elsewhere. With [typeclasses eauto], that seems to work better. *)
[solve [ typeclasses eauto with typeclass_instances ] || [solve [ typeclasses eauto with typeclass_instances ] ||
fail "iPoseProof: not a BI assertion"|exact t]] fail "iPoseProof: not a BI assertion"|exact t]]
with go_specilize t tT := with go_specialize t tT :=
lazymatch tT with (* We do not use hnf of tT, because, if lazymatch tT with (* We do not use hnf of tT, because, if
entailment is not opaque, then it would entailment is not opaque, then it would
unfold it. *) unfold it. *)
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment