From 4afebcb8dd39c8420707019e36ce6cb60f59e5a0 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Tue, 16 Jan 2018 08:36:15 +0100
Subject: [PATCH] Typos.
---
theories/proofmode/tactics.v | 6 +++---
1 file changed, 3 insertions(+), 3 deletions(-)
diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index 904d30642..e283e18de 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -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"
--
GitLab