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

Typos.

parent 584f9f96
Pipeline #6216 passed with stages
in 3 minutes and 27 seconds
......@@ -900,9 +900,9 @@ Tactic Notation "iNext" open_constr(n) :=
let P := match goal with |- envs_entails _ ?P => P end in
try lazymatch n with 0 => fail 1 "iNext: cannot strip 0 laters" end;
(* apply is sometimes confused wrt. canonical structures search.
refine should us the other unification algorithm, which should
refine should use the other unification algorithm, which should
not have this issue. *)
notypeclasses refine (coq_tactics.tac_next _ _ n _ _ _ _ _);
notypeclasses refine (tac_next _ _ n _ _ _ _ _);
[apply _ || fail "iNext:" P "does not contain" n "laters"
|lazymatch goal with
| |- IntoLaterNEnvs 0 _ _ => fail "iNext:" P "does not contain laters"
......@@ -1562,7 +1562,7 @@ Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH)
Tactic Notation "iLöbCore" "as" constr (IH) :=
iStartProof;
(* apply is sometimes confused wrt. canonical structures search.
refine should us the other unification algorithm, which should
refine should use the other unification algorithm, which should
not have this issue. *)
notypeclasses refine (tac_löb _ _ IH _ _ _ _);
[reflexivity || fail "iLöb: spatial context not empty, this should not happen"
......
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