Suppression définitive de lmatch et or_metanum dans tacinterp

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

8 files changed, 43 insertions, 63 deletions

diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4
index fb3850c900..57f47ca150 100644
--- a/parsing/g_ltac.ml4
+++ b/parsing/g_ltac.ml4
@@ -31,7 +31,7 @@ open Q
 type let_clause_kind =
   | LETTOPCLAUSE of Names.identifier * constr_expr
   | LETCLAUSE of
-      (Names.identifier Util.located * (constr_expr, Libnames.reference Genarg.or_metanum) may_eval option * raw_tactic_arg)
+      (Names.identifier Util.located * (constr_expr, Libnames.reference) may_eval option * raw_tactic_arg)
 
 ifdef Quotify then
 module Prelude = struct
diff --git a/parsing/g_ltacnew.ml4 b/parsing/g_ltacnew.ml4
index 834e978e48..2000765572 100644
--- a/parsing/g_ltacnew.ml4
+++ b/parsing/g_ltacnew.ml4
@@ -31,7 +31,7 @@ open Q
 type let_clause_kind =
   | LETTOPCLAUSE of Names.identifier * constr_expr
   | LETCLAUSE of
-      (Names.identifier Util.located * (constr_expr, Libnames.reference Genarg.or_metanum) may_eval option * raw_tactic_arg)
+      (Names.identifier Util.located * (constr_expr, Libnames.reference) may_eval option * raw_tactic_arg)
 
 ifdef Quotify then
 module Prelude = struct
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 62f2300a7b..225aa4728d 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -84,13 +84,13 @@ GEXTEND Gram
   ;
   (* Either an hypothesis or a ltac ref (variable or pattern patvar) *)
   id_or_ltac_ref:
-    [ [ id = base_ident -> Genarg.AN id
-      | "?"; n = natural -> Genarg.MetaNum (loc,Pattern.patvar_of_int n) ] ]
+    [ [ id = base_ident -> AI (loc,id)
+      | "?"; n = natural -> AI (loc,Pattern.patvar_of_int n) ] ]
   ;
   (* Either a global ref or a ltac ref (variable or pattern patvar) *)
   global_or_ltac_ref:
-    [ [ qid = global -> AN qid
-      | "?"; n = natural -> MetaNum (loc,Pattern.patvar_of_int n) ] ]
+    [ [ qid = global -> qid
+      | "?"; n = natural -> Libnames.Ident (loc,Pattern.patvar_of_int n) ] ]
   ;
   (* An identifier or a quotation meta-variable *)
   id_or_meta:
@@ -320,10 +320,10 @@ GEXTEND Gram
       (* Context management *)
       | IDENT "Clear"; l = LIST1 id_or_ltac_ref -> TacClear l
       | IDENT "ClearBody"; l = LIST1 id_or_ltac_ref -> TacClearBody l
-      | IDENT "Move"; id1 = identref; IDENT "after"; id2 = identref -> 
-	  TacMove (true,id1,id2)
-      | IDENT "Rename"; id1 = identref; IDENT "into"; id2 = identref -> 
-	  TacRename (id1,id2)
+      | IDENT "Move"; id1 = id_or_ltac_ref; IDENT "after"; 
+	  id2 = id_or_ltac_ref -> TacMove (true,id1,id2)
+      | IDENT "Rename"; id1 = id_or_ltac_ref; IDENT "into"; 
+	  id2 = id_or_ltac_ref -> TacRename (id1,id2)
 
       (* Constructors *)
       | IDENT "Left"; bl = with_binding_list -> TacLeft bl
diff --git a/parsing/g_tacticnew.ml4 b/parsing/g_tacticnew.ml4
index b299a33680..40a292ca19 100644
--- a/parsing/g_tacticnew.ml4
+++ b/parsing/g_tacticnew.ml4
@@ -95,16 +95,6 @@ GEXTEND Gram
   [ [ a0 = autoarg_depth; l = autoarg_adding; 
       a2 = autoarg_destructing; a3 = autoarg_usingTDB -> (a0,l,a2,a3) ] ]
   ;
-  (* Either an hypothesis or a ltac ref (variable or pattern patvar) *)
-  id_or_ltac_ref:
-    [ [ id = base_ident -> AN id
-(*      | "?"; n = natural -> MetaNum (loc,Pattern.patvar_of_int n) *) ] ]
-  ;
-  (* Either a global ref or a ltac ref (variable or pattern patvar) *)
-  global_or_ltac_ref:
-    [ [ qid = global -> AN qid
-(*      | "?"; n = natural -> MetaNum (loc,Pattern.patvar_of_int n) *) ] ]
-  ;
   (* An identifier or a quotation meta-variable *)
   id_or_meta:
     [ [ id = identref -> AI id 
@@ -186,15 +176,15 @@ GEXTEND Gram
     [ [ "with"; bl = binding_list -> bl | -> NoBindings ] ]
   ;
   unfold_occ:
-    [ [ nl = LIST0 integer; c = global_or_ltac_ref -> (nl,c) ] ]
+    [ [ nl = LIST0 integer; c = global -> (nl,c) ] ]
   ;
   red_flag:
     [ [ IDENT "beta" -> FBeta
       | IDENT "delta" -> FDeltaBut []
       | IDENT "iota" -> FIota
       | IDENT "zeta" -> FZeta
-      | IDENT "delta"; "["; idl = LIST1 global_or_ltac_ref; "]" -> FConst idl
-      | IDENT "delta"; "-"; "["; idl = LIST1 global_or_ltac_ref; "]" -> FDeltaBut idl
+      | IDENT "delta"; "["; idl = LIST1 global; "]" -> FConst idl
+      | IDENT "delta"; "-"; "["; idl = LIST1 global; "]" -> FDeltaBut idl
     ] ]
   ;
   red_tactic:
@@ -310,7 +300,7 @@ GEXTEND Gram
           ids = with_names -> TacNewDestruct (c,el,ids)
       | IDENT "decompose"; IDENT "record" ; c = lconstr -> TacDecomposeAnd c
       | IDENT "decompose"; IDENT "sum"; c = lconstr -> TacDecomposeOr c
-      | IDENT "decompose"; "["; l = LIST1 global_or_ltac_ref; "]"; c = lconstr
+      | IDENT "decompose"; "["; l = LIST1 global; "]"; c = lconstr
         -> TacDecompose (l,c)
 
       (* Automation tactic *)
@@ -326,11 +316,11 @@ GEXTEND Gram
 	  TacDAuto (n, p)
 
       (* Context management *)
-      | IDENT "clear"; l = LIST1 id_or_ltac_ref -> TacClear l
-      | IDENT "clearbody"; l = LIST1 id_or_ltac_ref -> TacClearBody l
-      | IDENT "move"; id1 = identref; IDENT "after"; id2 = identref -> 
+      | IDENT "clear"; l = LIST1 id_or_meta -> TacClear l
+      | IDENT "clearbody"; l = LIST1 id_or_meta -> TacClearBody l
+      | IDENT "move"; id1 = id_or_meta; IDENT "after"; id2 = id_or_meta -> 
 	  TacMove (true,id1,id2)
-      | IDENT "rename"; id1 = identref; IDENT "into"; id2 = identref -> 
+      | IDENT "rename"; id1 = id_or_meta; IDENT "into"; id2 = id_or_meta -> 
 	  TacRename (id1,id2)
 
       (* Constructors *)
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 8558c2d2f3..7bf1d837d2 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -151,7 +151,7 @@ module Tactic :
     open Rawterm
     val castedopenconstr : constr_expr Gram.Entry.e
     val constr_with_bindings : constr_expr with_bindings Gram.Entry.e
-    val constrarg : (constr_expr,reference or_metanum) may_eval Gram.Entry.e
+    val constrarg : (constr_expr,reference) may_eval Gram.Entry.e
     val quantified_hypothesis : quantified_hypothesis Gram.Entry.e
     val int_or_var : int or_var Gram.Entry.e
     val red_expr : raw_red_expr Gram.Entry.e
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index 0f26e390b8..3022fcbb19 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -83,10 +83,6 @@ let pi3 (_,_,a) = a
 
 let pr_arg pr x = spc () ++ pr x
 
-let pr_or_metanum pr = function
-  | AN x -> pr x
-  | MetaNum (_,n) -> str "?" ++ pr_patvar n
-
 let pr_or_var pr = function
   | ArgArg x -> pr x
   | ArgVar (_,s) -> pr_id s
@@ -249,13 +245,13 @@ let rec pr_raw_generic prc prlc prtac x =
   | SortArgType -> pr_arg pr_sort (out_gen rawwit_sort x)
   | ConstrArgType -> pr_arg prc (out_gen rawwit_constr x)
   | ConstrMayEvalArgType ->
-      pr_arg (pr_may_eval prc (pr_or_metanum pr_reference))
+      pr_arg (pr_may_eval prc pr_reference)
         (out_gen rawwit_constr_may_eval x)
   | QuantHypArgType ->
       pr_arg pr_quantified_hypothesis (out_gen rawwit_quant_hyp x)
   | RedExprArgType ->
       pr_arg (pr_red_expr 
-        (prc,pr_or_metanum pr_reference)) (out_gen rawwit_red_expr x)
+        (prc,pr_reference)) (out_gen rawwit_red_expr x)
   | TacticArgType -> pr_arg prtac (out_gen rawwit_tactic x)
   | CastedOpenConstrArgType ->
       pr_arg prc (out_gen rawwit_casted_open_constr x)
@@ -292,12 +288,12 @@ let rec pr_glob_generic prc prlc prtac x =
   | ConstrArgType -> pr_arg prc (out_gen globwit_constr x)
   | ConstrMayEvalArgType ->
       pr_arg (pr_may_eval prc
-        (pr_or_metanum (pr_or_var (pr_and_short_name pr_evaluable_reference)))) (out_gen globwit_constr_may_eval x)
+        (pr_or_var (pr_and_short_name pr_evaluable_reference))) (out_gen globwit_constr_may_eval x)
   | QuantHypArgType ->
       pr_arg pr_quantified_hypothesis (out_gen globwit_quant_hyp x)
   | RedExprArgType ->
       pr_arg (pr_red_expr 
-        (prc,pr_or_metanum (pr_or_var (pr_and_short_name pr_evaluable_reference)))) (out_gen globwit_red_expr x)
+        (prc,pr_or_var (pr_and_short_name pr_evaluable_reference))) (out_gen globwit_red_expr x)
   | TacticArgType -> pr_arg prtac (out_gen globwit_tactic x)
   | CastedOpenConstrArgType ->
       pr_arg prc (out_gen globwit_casted_open_constr x)
@@ -481,7 +477,7 @@ and pr_atom1 = function
       hov 1 (str "Decompose Sum" ++ pr_arg pr_constr c)
   | TacDecompose (l,c) ->
       hov 1 (str "Decompose" ++ spc () ++
-        hov 0 (str "[" ++ prlist_with_sep spc (pr_or_metanum pr_ind) l
+        hov 0 (str "[" ++ prlist_with_sep spc pr_ind l
 	  ++ str "]"))
   | TacSpecialize (n,c) ->
       hov 1 (str "Specialize" ++ pr_opt int n ++ pr_with_bindings c)
@@ -506,19 +502,19 @@ and pr_atom1 = function
 
   (* Context management *)
   | TacClear l ->
-      hov 1 (str "Clear" ++ spc () ++ prlist_with_sep spc (pr_or_metanum pr_id) l)
+      hov 1 (str "Clear" ++ spc () ++ prlist_with_sep spc pr_ident l)
   | TacClearBody l ->
-      hov 1 (str "Clear" ++ spc () ++ prlist_with_sep spc (pr_or_metanum pr_id) l)
-  | TacMove (b,(_,id1),(_,id2)) ->
+      hov 1 (str "Clear" ++ spc () ++ prlist_with_sep spc pr_ident l)
+  | TacMove (b,id1,id2) ->
       (* Rem: only b = true is available for users *)
       assert b;
       hov 1
-        (str "Move" ++ brk (1,1) ++ pr_id id1 ++ spc () ++ 
-	 str "after" ++ brk (1,1) ++ pr_id id2)
-  | TacRename ((_,id1),(_,id2)) ->
+        (str "Move" ++ brk (1,1) ++ pr_ident id1 ++ spc () ++ 
+	 str "after" ++ brk (1,1) ++ pr_ident id2)
+  | TacRename (id1,id2) ->
       hov 1
-        (str "Rename" ++ brk (1,1) ++ pr_id id1 ++ spc () ++ 
-	 str "into" ++ brk (1,1) ++ pr_id id2)
+        (str "Rename" ++ brk (1,1) ++ pr_ident id1 ++ spc () ++ 
+	 str "into" ++ brk (1,1) ++ pr_ident id2)
 
   (* Constructors *)
   | TacLeft l -> hov 1 (str "Left" ++ pr_bindings l)
@@ -679,7 +675,7 @@ let rec glob_printers =
      pr_glob_tactic0,
      pr_and_constr_expr Ppconstr.pr_rawconstr,
      Printer.pr_pattern,
-     pr_or_metanum (pr_or_var (pr_and_short_name pr_evaluable_reference)),
+     pr_or_var (pr_and_short_name pr_evaluable_reference),
      pr_or_var pr_inductive,
      pr_or_var (pr_located pr_ltac_constant),
      pr_located pr_id,
diff --git a/parsing/pptactic.mli b/parsing/pptactic.mli
index 728c8f8cd3..bd06d5e1e2 100644
--- a/parsing/pptactic.mli
+++ b/parsing/pptactic.mli
@@ -17,7 +17,6 @@ open Topconstr
 open Rawterm
 
 val pr_or_var : ('a -> std_ppcmds) -> 'a or_var -> std_ppcmds
-val pr_or_metanum : ('a -> std_ppcmds) -> 'a or_metanum -> std_ppcmds
 val pr_or_metaid : ('a -> std_ppcmds) -> 'a or_metaid -> std_ppcmds
 val pr_and_short_name : ('a -> std_ppcmds) -> 'a and_short_name -> std_ppcmds
 val pr_located : ('a -> std_ppcmds) -> 'a Util.located -> std_ppcmds
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index bb0164962c..a424655727 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -144,11 +144,6 @@ let mlexpr_of_intro_pattern = function
 
 let mlexpr_of_ident_option = mlexpr_of_option (mlexpr_of_ident)
 
-let mlexpr_of_or_metanum f = function
-  | Genarg.AN a -> <:expr< Genarg.AN $f a$ >>
-  | Genarg.MetaNum (_,n) ->
-      <:expr< Genarg.MetaNum $dloc$ $mlexpr_of_ident n$ >>
-
 let mlexpr_of_or_metaid f = function
   | Tacexpr.AI a -> <:expr< Tacexpr.AI $f a$ >>
   | Tacexpr.MetaId (_,id) -> <:expr< Tacexpr.AI $anti loc id$ >>
@@ -161,11 +156,11 @@ let mlexpr_of_located f (loc,x) = <:expr< ($dloc$, $f x$) >>
 
 let mlexpr_of_loc loc = <:expr< $dloc$ >>
 
+let mlexpr_of_hyp = mlexpr_of_or_metaid (mlexpr_of_located mlexpr_of_ident)
+
 let mlexpr_of_hyp_location = function
-  | Tacexpr.InHyp id ->
-      <:expr< Tacexpr.InHyp $mlexpr_of_or_metaid (mlexpr_of_located mlexpr_of_ident) id$ >>
-  | Tacexpr.InHypType id ->
-      <:expr< Tacexpr.InHypType $mlexpr_of_or_metaid (mlexpr_of_located mlexpr_of_ident) id$ >>
+  | Tacexpr.InHyp id -> <:expr< Tacexpr.InHyp $mlexpr_of_hyp id$ >>
+  | Tacexpr.InHypType id -> <:expr< Tacexpr.InHypType $mlexpr_of_hyp id$ >>
 
 (*
 let mlexpr_of_red_mode = function
@@ -185,7 +180,7 @@ let mlexpr_of_red_flags {
   Rawterm.rIota = $mlexpr_of_bool bi$;
   Rawterm.rZeta = $mlexpr_of_bool bz$;
   Rawterm.rDelta = $mlexpr_of_bool bd$;
-  Rawterm.rConst = $mlexpr_of_list (mlexpr_of_or_metanum mlexpr_of_reference) l$
+  Rawterm.rConst = $mlexpr_of_list mlexpr_of_reference l$
 } >>
 
 let rec mlexpr_of_constr = function
@@ -221,7 +216,7 @@ let mlexpr_of_red_expr = function
       <:expr< Rawterm.Lazy $mlexpr_of_red_flags f$ >>
   | Rawterm.Unfold l ->
       let f1 = mlexpr_of_list mlexpr_of_int in
-      let f2 = mlexpr_of_or_metanum mlexpr_of_reference in
+      let f2 = mlexpr_of_reference in
       let f = mlexpr_of_list (mlexpr_of_pair f1 f2) in
       <:expr< Rawterm.Unfold $f l$ >>
   | Rawterm.Fold l ->
@@ -392,15 +387,15 @@ let rec mlexpr_of_atomic_tactic = function
 
   (* Context management *)
   | Tacexpr.TacClear l ->
-      let l = mlexpr_of_list (mlexpr_of_or_metanum mlexpr_of_ident) l in
+      let l = mlexpr_of_list (mlexpr_of_hyp) l in
       <:expr< Tacexpr.TacClear $l$ >>
   | Tacexpr.TacClearBody l ->
-      let l = mlexpr_of_list (mlexpr_of_or_metanum mlexpr_of_ident) l in
+      let l = mlexpr_of_list (mlexpr_of_hyp) l in
       <:expr< Tacexpr.TacClearBody $l$ >>
   | Tacexpr.TacMove (dep,id1,id2) ->
       <:expr< Tacexpr.TacMove $mlexpr_of_bool dep$
-              $mlexpr_of_located mlexpr_of_ident id1$
-              $mlexpr_of_located mlexpr_of_ident id2$ >>
+              $mlexpr_of_hyp id1$
+              $mlexpr_of_hyp id2$ >>
 
   (* Constructors *)
   | Tacexpr.TacLeft l ->