From 27e86bd0d3d1dce8d609f8e793f5be1827d31099 Mon Sep 17 00:00:00 2001
From: mohring
Date: Tue, 28 Aug 2001 09:01:29 +0000
Subject: Remplace numarg -> pure_numarg dans Double Induction

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1900 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 b1f68d0701..98e3d6ead8 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -254,7 +254,7 @@ GEXTEND Gram
       | IDENT "Induction"; n = pure_numarg -> <:ast< (Induction $n) >>
       | IDENT "NewInduction"; c=ident_or_constrarg -> <:ast<(NewInduction $c)>>
       | IDENT "NewInduction"; n = pure_numarg -> <:ast< (NewInduction $n) >>
-      | IDENT "Double"; IDENT "Induction"; i = numarg; j = numarg ->
+      | IDENT "Double"; IDENT "Induction"; i = pure_numarg; j = pure_numarg ->
           <:ast< (DoubleInd $i $j) >>
       | IDENT "Trivial" -> <:ast<(Trivial)>>
       | IDENT "Trivial"; "with"; lid = ne_identarg_list -> 
-- 
cgit v1.2.3