Prise en compte noms longs dans SuperAuto

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1391 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 30 insertions, 39 deletions

diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index f4b0e01e58..4595c81b8f 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -14,6 +14,31 @@ open Util
 (* Auxiliary grammar rules *)
 
 GEXTEND Gram
+  GLOBAL: autoargs;
+
+  autoarg_depth:
+  [ [ n = pure_numarg -> <:ast< $n>>
+     | -> Coqast.Str(loc,"NoAutoArg") ] ]
+  ;
+  autoarg_adding:
+  [ [ IDENT "Adding" ; "["; l = ne_qualidarg_list; "]" -> l
+      | -> [] ] ]
+  ;
+  autoarg_destructing:
+  [ [ IDENT "Destructing" -> Coqast.Str(loc,"Destructing")
+      | -> Coqast.Str(loc,"NoAutoArg") ] ]
+  ;
+  autoarg_usingTDB:
+  [ [ "Using"; "TDB"  ->  Coqast.Str(loc,"UsingTDB")
+      | -> Coqast.Str(loc,"NoAutoArg")  ] ]
+  ;
+  autoargs:
+  [ [ a0 = autoarg_depth; l = autoarg_adding; 
+      a2 = autoarg_destructing; a3 = autoarg_usingTDB -> a0::a2::a3::l ] ]
+  ;
+  END
+
+GEXTEND Gram
 
   identarg:
     [ [ id = Constr.ident -> id ] ]
@@ -63,9 +88,6 @@ GEXTEND Gram
   ne_qualidconstarg_list:
     [ [ l = LIST1 qualidconstarg -> l ] ]
   ;
-  ne_num_list:
-    [ [ n = numarg; l = ne_num_list -> n :: l | n = numarg -> [n] ] ]
-  ;
   pattern_occ:
     [ [ nl = LIST1 pure_numarg; c = constrarg ->
          <:ast< (PATTERN $c ($LIST $nl)) >>
@@ -175,23 +197,6 @@ GEXTEND Gram
     [ [ "in"; idl = ne_identarg_list -> <:ast< (CLAUSE ($LIST idl)) >>
       | -> <:ast< (CLAUSE) >> ] ]
   ;
-  autoarg_depth:
-  [ [ n = pure_numarg -> <:ast< $n>>
-     | -> Coqast.Str(loc,"NoAutoArg") ] ]
-  ;
-  autoarg_adding:
-  [ [ IDENT "Adding" ; "["; l = ne_identarg_list; "]" -> 
-        <:ast< (CLAUSE ($LIST $l))>>
-      | -> <:ast< (CLAUSE) >> ] ]
-  ;
-  autoarg_destructing:
-  [ [ IDENT "Destructing" -> Coqast.Str(loc,"Destructing")
-      | -> Coqast.Str(loc,"NoAutoArg") ] ]
-  ;
-  autoarg_usingTDB:
-  [ [ "Using"; "TDB"  ->  Coqast.Str(loc,"UsingTDB")
-      | -> Coqast.Str(loc,"NoAutoArg")  ] ]
-  ;
   fixdecl:
     [ [ id = identarg; n = pure_numarg; ":"; c = constrarg; fd = fixdecl ->
           <:ast< (FIXEXP $id $n $c) >> :: fd
@@ -362,12 +367,8 @@ GEXTEND Gram
       | IDENT "DHyp";  id=identarg  -> <:ast< (DHyp  $id)>>
       | IDENT "CDHyp"; id=identarg -> <:ast<  (CDHyp $id)>>
       | IDENT "DConcl"  -> <:ast< (DConcl)>>
-      | IDENT "SuperAuto"; 
-                       a0 = autoarg_depth;
-                       a1 = autoarg_adding; 
-                       a2 = autoarg_destructing; 
-                       a3 = autoarg_usingTDB -> 
-                   <:ast< (SuperAuto $a0 $a1 $a2 $a3) >>
+      | IDENT "SuperAuto"; l = autoargs ->
+                   <:ast< (SuperAuto ($LIST $l)) >>
       | IDENT "Auto"; n = pure_numarg; IDENT "Decomp" -> <:ast< (DAuto $n) >>
       | IDENT "Auto"; IDENT "Decomp" -> <:ast< (DAuto) >>
       | IDENT "Auto"; n = pure_numarg; IDENT "Decomp"; p = pure_numarg ->
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index 5776cb811a..2d451839fb 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -272,7 +272,8 @@ module Tactic =
     let gec_list s =
       let e = Gram.Entry.create ("Tactic." ^ s) in
       Hashtbl.add utactic s (ListAst e); e
-    
+
+    let autoargs = gec_list "autoargs"    
     let binding_list = gec "binding_list"
     let castedopenconstrarg = gec "castedopenconstrarg"
     let castedconstrarg = gec "castedconstrarg"
@@ -300,7 +301,6 @@ module Tactic =
     let ne_identarg_list = gec_list "ne_identarg_list"
     let ne_qualidarg_list = gec_list "ne_qualidarg_list"
     let ne_qualidconstarg_list = gec_list "ne_qualidconstarg_list"
-    let ne_num_list = gec_list "ne_num_list"
     let ne_pattern_list = gec_list "ne_pattern_list"
     let clause_pattern = gec "clause_pattern"
     let one_intropattern = gec "one_intropattern"
@@ -311,11 +311,6 @@ module Tactic =
     let rec_clause = gec "rec_clause"
     let red_tactic = gec "red_tactic"
     let red_flag = gec "red_flag"
-    let autoarg_depth = gec "autoarg_depth"
-    let autoarg_excluding = gec "autoarg_excluding"
-    let autoarg_adding = gec "autoarg_adding"
-    let autoarg_destructing = gec "autoarg_destructing"
-    let autoarg_usingTDB = gec "autoarg_usingTDB"
     let numarg = gec "numarg"
     let pattern_occ = gec "pattern_occ"
     let pattern_occ_hyp = gec "pattern_occ_hyp"
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 1999733f0e..79d33a98bc 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -96,11 +96,7 @@ module Constr :
 
 module Tactic :
   sig
-    val autoarg_adding : Coqast.t Gram.Entry.e
-    val autoarg_depth : Coqast.t Gram.Entry.e
-    val autoarg_destructing : Coqast.t Gram.Entry.e
-    val autoarg_excluding : Coqast.t Gram.Entry.e
-    val autoarg_usingTDB : Coqast.t Gram.Entry.e
+    val autoargs : Coqast.t list Gram.Entry.e
     val binding_list : Coqast.t Gram.Entry.e
     val castedopenconstrarg : Coqast.t Gram.Entry.e
     val castedconstrarg : Coqast.t Gram.Entry.e
@@ -131,7 +127,6 @@ module Tactic :
     val ne_qualidarg_list : Coqast.t list Gram.Entry.e
     val ne_qualidconstarg_list : Coqast.t list Gram.Entry.e
     val ne_intropattern : Coqast.t Gram.Entry.e
-    val ne_num_list : Coqast.t list Gram.Entry.e
     val ne_pattern_list : Coqast.t list Gram.Entry.e
     val clause_pattern : Coqast.t Gram.Entry.e
     val ne_unfold_occ_list : Coqast.t list Gram.Entry.e