1 files changed, 7 insertions, 7 deletions
diff --git a/test-suite/success/Mod_ltac.v b/test-suite/success/Mod_ltac.v
index 1a9f6fc5..44bb3a55 100644
--- a/test-suite/success/Mod_ltac.v
+++ b/test-suite/success/Mod_ltac.v
@@ -1,20 +1,20 @@
 (* Submitted by Houda Anoun *)
 
 Module toto.
-Tactic Definition titi:=Auto.
+Ltac titi := auto.
 End toto.
 
 Module ti.
 Import toto.
-Tactic Definition equal:=
-Match Context With
-[ |- ?1=?1]-> titi
-| [ |- ?]-> Idtac.
+Ltac equal := match goal with
+              |  |- (?X1 = ?X1) => titi
+              |  |- _ => idtac
+              end.
 
 End ti.
 
 Import ti.
-Definition simple:(a:nat) a=a.
-Intro.
+Definition simple : forall a : nat, a = a.
+intro.
 equal.
 Qed.