Imported Upstream version 8.5~beta1+dfsg

1 files changed, 4 insertions, 8 deletions

diff --git a/test-suite/success/ltac.v b/test-suite/success/ltac.v
index c2eb8bd7..badce063 100644
--- a/test-suite/success/ltac.v
+++ b/test-suite/success/ltac.v
@@ -1,6 +1,6 @@
 (* The tactic language *)
 
-(* Submitted by Pierre Crégut *)
+(* Submitted by Pierre Crégut *)
 (* Checks substitution of x *)
 Ltac f x := unfold x; idtac.
 
@@ -9,7 +9,7 @@ f plus.
 reflexivity.
 Qed.
 
-(* Submitted by Pierre Crégut *)
+(* Submitted by Pierre Crégut *)
 (* Check syntactic correctness *)
 Ltac F x := idtac; G x
  with G y := idtac; F y.
@@ -143,7 +143,7 @@ Qed.
 
 Ltac check_binding y := cut ((fun y => y) = S).
 Goal True.
-check_binding true.
+check_binding ipattern:H.
 Abort.
 
 (* Check that variables explicitly parsed as ltac variables are not
@@ -211,7 +211,7 @@ is.
 exact I.
 Abort.
 
-(* Interférence entre espaces des noms *)
+(* Interférence entre espaces des noms *)
 
 Ltac O := intro.
 Ltac Z1 t := set (x:=t).
@@ -298,7 +298,3 @@ evar(foo:nat).
 let evval := eval compute in foo in not_eq evval 1.
 let evval := eval compute in foo in not_eq 1 evval.
 Abort.
-
-(* Check that this returns an error and not an anomaly (see r13667) *)
-
-Fail Local Tactic Notation "myintro" := intro.