From ebf2a25f97c3ffc3376967d2841fbd681e6d69c2 Mon Sep 17 00:00:00 2001
From: delahaye
Date: Tue, 24 Apr 2001 19:48:47 +0000
Subject: Les clauses de Rec doivent prendre des tactic_atom's

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1701 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 parsing/g_tactic.ml4 | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index e32a649f05..bab0c5afa0 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -243,7 +243,7 @@ GEXTEND Gram
 	| _ -> errorlabstrm "Gram.let_clause" [<'sTR "Not a COMMAND">]) ] ]
   ;
   rec_clause:
-    [ [ name = identarg; it = LIST1 input_fun; "->"; body = tactic_expr ->
+    [ [ name = identarg; it = LIST1 input_fun; "->"; body = tactic_atom ->
           <:ast< (RECCLAUSE $name (FUNVAR ($LIST $it)) $body) >> ] ]
   ;
   match_pattern:
-- 
cgit v1.2.3