From 100120634953b594169931409122c580fa12e5b1 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 14 Jun 2002 10:06:54 +0000
Subject: *** empty log message ***

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2785 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 test-suite/success/ltac.v | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/test-suite/success/ltac.v b/test-suite/success/ltac.v
index 04d7c87c5b..bac62f16eb 100644
--- a/test-suite/success/ltac.v
+++ b/test-suite/success/ltac.v
@@ -9,6 +9,11 @@ f plus.
 Reflexivity.
 Qed.
 
+(* Submitted by Pierre Crégut *)
+(* Check syntactic correctness *)
+Recursive Tactic Definition F x := Idtac; (G x)
+And G y := Idtac; (F y).
+
 (* Check that Match Context keeps a closure *)
 Tactic Definition U := Let a = 'I In Match Context With [ |- ? ] -> Apply a.
 
-- 
cgit v1.2.3