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

27 files changed, 288 insertions, 387 deletions

diff --git a/contrib/interface/pbp.ml b/contrib/interface/pbp.ml
index 4abcb5f96f..74ecdaaa3d 100644
--- a/contrib/interface/pbp.ml
+++ b/contrib/interface/pbp.ml
@@ -177,7 +177,7 @@ let make_pbp_atomic_tactic = function
       TacAtom
 	(zz, TacElim ((make_var hyp_name,ExplicitBindings bind),None))
   | PbpTryClear l -> 
-      TacTry (TacAtom (zz, TacClear (List.map (fun s -> AN s) l)))
+      TacTry (TacAtom (zz, TacClear (List.map (fun s -> AI (zz,s)) l)))
   | PbpSplit -> TacAtom (zz, TacSplit (false,NoBindings));;
 
 let rec make_pbp_tactic = function
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 9fbd1158f5..b83ce2d71e 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -200,16 +200,6 @@ let loc_qualid_to_ct_ID ref =
 let int_of_meta n = int_of_string (string_of_id n)
 let is_int_meta n = try let _ = int_of_meta n in true with _ -> false
 
-let qualid_or_meta_to_ct_ID = function
-  | AN qid -> tac_qualid_to_ct_ID qid
-  | MetaNum (_,n) when is_int_meta n -> CT_metac (CT_int (int_of_meta n))
-  | MetaNum _ -> xlate_error "TODO: ident meta"
-
-let ident_or_meta_to_ct_ID = function
-  | AN id -> xlate_ident id
-  | MetaNum (_,n) when is_int_meta n -> CT_metac (CT_int (int_of_meta n))
-  | MetaNum _ -> xlate_error "TODO: ident meta"
-
 let xlate_qualid_list l = CT_id_list (List.map loc_qualid_to_ct_ID l)
 
 let reference_to_ct_ID = function
@@ -394,6 +384,10 @@ let (xlate_ident_or_metaid:
     AI (_, x) -> xlate_ident x
   | MetaId(_, x) -> CT_metaid x;;
 
+let xlate_hyp = function
+  | AI (_,id) -> xlate_ident id
+  | MetaId _ -> xlate_error "MetaId should occur only in quotations"
+
 let xlate_hyp_location =
  function
   | InHyp (AI (_,id)) -> CT_coerce_ID_to_ID_OR_INTYPE (xlate_ident id)
@@ -495,12 +489,12 @@ let strip_targ_intropatt =
 let get_flag r =
   let conv_flags, red_ids = 
     if r.rDelta then
-      [CT_delta], CT_unfbut (List.map qualid_or_meta_to_ct_ID r.rConst)
+      [CT_delta], CT_unfbut (List.map tac_qualid_to_ct_ID r.rConst)
     else
       (if r.rConst = []
       then (* probably useless: just for compatibility *) []
       else [CT_delta]),
-      CT_unf (List.map qualid_or_meta_to_ct_ID r.rConst) in
+      CT_unf (List.map tac_qualid_to_ct_ID r.rConst) in
   let conv_flags = if r.rBeta then CT_beta::conv_flags else conv_flags in
   let conv_flags = if r.rIota then CT_iota::conv_flags else conv_flags in
   let conv_flags = if r.rZeta then CT_zeta::conv_flags else conv_flags in
@@ -560,7 +554,7 @@ let xlate_using = function
 let xlate_one_unfold_block = function
     (nums,qid) -> 
       CT_unfold_occ (CT_int_list (List.map (fun x -> CT_int x) nums),
-		     qualid_or_meta_to_ct_ID qid);;
+		     tac_qualid_to_ct_ID qid);;
 
 let xlate_lettac_clauses = function
     (opt_l, l') ->
@@ -814,8 +808,8 @@ and xlate_tac =
      CT_intro_after(CT_coerce_ID_to_ID_OPT (xlate_ident id1),xlate_ident id2)
     | TacIntroMove (None, Some (_,id2)) ->
 	CT_intro_after(CT_coerce_NONE_to_ID_OPT CT_none, xlate_ident id2)
-    | TacMove (true, (_,id1), (_,id2)) ->
-	CT_move_after(xlate_ident id1, xlate_ident id2)
+    | TacMove (true, id1, id2) ->
+	CT_move_after(xlate_hyp id1, xlate_hyp id2)
     | TacMove (false, id1, id2) -> xlate_error "Non dep Move is only internal"
     | TacIntroPattern [] -> CT_intros (CT_intro_patt_list [])
     | TacIntroPattern patt_list ->
@@ -961,16 +955,16 @@ and xlate_tac =
     | TacDecompose ([],c) ->
 	xlate_error "Decompose : empty list of identifiers?"
     | TacDecompose (id::l,c) ->
-	let id' = qualid_or_meta_to_ct_ID id in
-	let l' = List.map qualid_or_meta_to_ct_ID l in
+	let id' = tac_qualid_to_ct_ID id in
+	let l' = List.map tac_qualid_to_ct_ID l in
         CT_decompose_list(CT_id_ne_list(id',l'),xlate_formula c)
     | TacDecomposeAnd c -> CT_decompose_record (xlate_formula c)
     | TacDecomposeOr c -> CT_decompose_sum(xlate_formula c)
     | TacClear [] ->
 	xlate_error "Clear expects a non empty list of identifiers"
     | TacClear (id::idl) ->
-       let idl' = List.map ident_or_meta_to_ct_ID idl in
-       CT_clear (CT_id_ne_list (ident_or_meta_to_ct_ID id, idl'))
+       let idl' = List.map xlate_hyp idl in
+       CT_clear (CT_id_ne_list (xlate_hyp id, idl'))
     | (*For translating tactics/Inv.v *)
       TacExtend (_,("SimpleInversion"|"Inversion"|"InversionClear" as s), [id])
       ->
@@ -1002,12 +996,10 @@ and xlate_tac =
      CT_use_inversion (id, xlate_formula c,
        CT_id_list (List.map xlate_ident idlist))
     | TacExtend (_,"Omega", []) -> CT_omega
-    | TacRename ((_,id1), (_,id2)) -> CT_rename(xlate_ident id1, xlate_ident id2)
+    | TacRename (id1, id2) -> CT_rename(xlate_hyp id1, xlate_hyp id2)
     | TacClearBody([]) -> assert false
     | TacClearBody(a::l) -> 
-	CT_clear_body
-	  (CT_id_ne_list
-	     (ident_or_meta_to_ct_ID a, List.map ident_or_meta_to_ct_ID l))
+	CT_clear_body (CT_id_ne_list (xlate_hyp a, List.map xlate_hyp l))
     | TacDAuto (a, b) -> CT_dauto(xlate_int_opt a, xlate_int_opt b)
     | TacNewDestruct(a,b,c) ->
 	CT_new_destruct
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index ce671515f9..cfb0c4fb19 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -471,14 +471,12 @@ let internalise isarity sigma env allow_soapp lvar c =
 		  Array.of_list (List.map (intern false env) cl))
     | CHole loc -> 
 	RHole (loc, QuestionMark)
-    | CPatVar (loc, n) when allow_soapp = None ->
+    | CPatVar (loc, n) when allow_soapp ->
 	RPatVar (loc, n)
-    | CPatVar (loc, n) when Options.do_translate () ->
-	RVar (loc, snd n)
+    | CPatVar (loc, (false,n)) when Options.do_translate () ->
+	RVar (loc, n)
     | CPatVar (loc, (false,n as x)) ->
-        if List.mem n (out_some allow_soapp) or Options.do_translate () then
-	  RPatVar (loc, x)
-        else if List.mem n (fst (let (a,_,_) = lvar in a))
+        if List.mem n (fst (let (a,_,_) = lvar in a))
 	  (* & !Options.v7 : ne pas exiger, Tauto est encore en V7 ! *) then 
 	  RVar (loc, n)
 	else
@@ -589,13 +587,13 @@ let interp_rawconstr_gen isarity sigma env impls allow_soapp ltacvar c =
     allow_soapp (ltacvar,Environ.named_context env, []) c
 
 let interp_rawconstr sigma env c =
-  interp_rawconstr_gen false sigma env [] (Some []) ([],[]) c
+  interp_rawconstr_gen false sigma env [] false ([],[]) c
 
 let interp_rawtype sigma env c =
-  interp_rawconstr_gen true sigma env [] (Some []) ([],[]) c
+  interp_rawconstr_gen true sigma env [] false ([],[]) c
 
 let interp_rawtype_with_implicits sigma env impls c =
-  interp_rawconstr_gen true sigma env impls (Some []) ([],[]) c
+  interp_rawconstr_gen true sigma env impls false ([],[]) c
 
 (*
 (* The same as interp_rawconstr but with a list of variables which must not be
@@ -612,10 +610,10 @@ let interp_constr sigma env c =
   understand sigma env (interp_rawconstr sigma env c)
 
 let interp_openconstr sigma env c =
-  understand_gen_tcc sigma env [] [] None (interp_rawconstr sigma env c)
+  understand_gen_tcc sigma env [] None (interp_rawconstr sigma env c)
 
 let interp_casted_openconstr sigma env c typ =
-  understand_gen_tcc sigma env [] [] (Some typ) (interp_rawconstr sigma env c)
+  understand_gen_tcc sigma env [] (Some typ) (interp_rawconstr sigma env c)
 
 let interp_type sigma env c =
   understand_type sigma env (interp_rawtype sigma env c)
@@ -650,25 +648,25 @@ type ltac_env =
 (* Interprets a constr according to two lists *)
 (* of instantiations (variables and metas)    *)
 (* Note: typ is retyped *)
-let interp_constr_gen sigma env (ltacvar,unbndltacvar) lmeta c exptyp =
-  let c = interp_rawconstr_gen false sigma env [] (Some (List.map fst lmeta))
-    (List.map fst ltacvar,unbndltacvar) c
-  and rtype lst = retype_list sigma env lst in
-  understand_gen sigma env (rtype ltacvar) (rtype lmeta) exptyp c;;
+let interp_constr_gen sigma env (ltacvars,unbndltacvars) c exptyp =
+  let c = interp_rawconstr_gen false sigma env [] false
+    (List.map fst ltacvars,unbndltacvars) c in
+  let typs = retype_list sigma env ltacvars in
+  understand_gen sigma env typs exptyp c
 
 (*Interprets a casted constr according to two lists of instantiations
   (variables and metas)*)
-let interp_openconstr_gen sigma env (ltacvar,unbndltacvar) lmeta c exptyp =
-  let c = interp_rawconstr_gen false sigma env [] (Some (List.map fst lmeta))
-    (List.map fst ltacvar,unbndltacvar) c
-  and rtype lst = retype_list sigma env lst in
-  understand_gen_tcc sigma env (rtype ltacvar) (rtype lmeta) exptyp c;;
+let interp_openconstr_gen sigma env (ltacvars,unbndltacvars) c exptyp =
+  let c = interp_rawconstr_gen false sigma env [] false
+    (List.map fst ltacvars,unbndltacvars) c in
+  let typs = retype_list sigma env ltacvars in
+  understand_gen_tcc sigma env typs exptyp c
 
 let interp_casted_constr sigma env c typ = 
-  understand_gen sigma env [] [] (Some typ) (interp_rawconstr sigma env c)
+  understand_gen sigma env [] (Some typ) (interp_rawconstr sigma env c)
 
 let interp_constrpattern_gen sigma env (ltacvar,unbndltacvar) c =
-  let c = interp_rawconstr_gen false sigma env [] None
+  let c = interp_rawconstr_gen false sigma env [] true
     (List.map fst ltacvar,unbndltacvar) c in
   pattern_of_rawconstr c
 
@@ -680,7 +678,7 @@ let interp_aconstr vars a =
   (* [vl] is intended to remember the scope of the free variables of [a] *)
   let vl = List.map (fun id -> (id,ref None)) vars in
   let c = for_grammar (internalise false Evd.empty (extract_ids env, [], [])
-    (Some []) (([],[]),Environ.named_context env,vl)) a in
+    false (([],[]),Environ.named_context env,vl)) a in
   (* Translate and check that [c] has all its free variables bound in [vars] *)
   let a = aconstr_of_rawconstr vars c in
   (* Returns [a] and the ordered list of variables with their scopes *)
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index c052dadabf..4f0c803bdc 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -44,7 +44,7 @@ type ltac_env =
 (* Interprets global names, including syntactic defs and section variables *)
 val interp_rawconstr     : evar_map -> env -> constr_expr -> rawconstr
 val interp_rawconstr_gen : bool -> evar_map -> env -> implicits_env -> 
-    patvar list option -> ltac_sign -> constr_expr -> rawconstr
+    bool -> ltac_sign -> constr_expr -> rawconstr
 
 (*s Composing the translation with typing *)
 val interp_constr        : evar_map -> env -> constr_expr -> constr
@@ -70,14 +70,13 @@ val type_judgment_of_rawconstr :
 (* Interprets a constr according to two lists of instantiations (variables and
   metas), possibly casting it*)
 val interp_constr_gen     :
-  evar_map -> env -> ltac_env -> patvar_map -> constr_expr -> 
-    constr option -> constr
+  evar_map -> env -> ltac_env -> constr_expr -> constr option -> constr
 
 (* Interprets a constr according to two lists of instantiations (variables and
   metas), possibly casting it, and turning unresolved evar into metas*)
 val interp_openconstr_gen     :
   evar_map -> env -> ltac_env ->
-    patvar_map -> constr_expr -> constr option -> evar_map * constr
+    constr_expr -> constr option -> evar_map * constr
 
 (* Interprets constr patterns according to a list of instantiations
   (variables)*)
diff --git a/interp/genarg.ml b/interp/genarg.ml
index 833da9e78e..8eb8d2a0d6 100644
--- a/interp/genarg.ml
+++ b/interp/genarg.ml
@@ -40,7 +40,6 @@ type argument_type =
   | ExtraArgType of string
 
 type 'a or_var = ArgArg of 'a | ArgVar of identifier located
-type 'a or_metanum = AN of 'a | MetaNum of patvar located
 type 'a and_short_name = 'a * identifier located option
 type rawconstr_and_expr = rawconstr * constr_expr option
 
diff --git a/interp/genarg.mli b/interp/genarg.mli
index 8aa82ecb24..6c4da92c76 100644
--- a/interp/genarg.mli
+++ b/interp/genarg.mli
@@ -17,7 +17,6 @@ open Topconstr
 open Term
 
 type 'a or_var = ArgArg of 'a | ArgVar of identifier located
-type 'a or_metanum = AN of 'a | MetaNum of patvar located
 type 'a and_short_name = 'a * identifier located option
 
 (* In globalize tactics, we need to keep the initial constr_expr to recompute*)
@@ -110,8 +109,8 @@ val rawwit_constr : (constr_expr,constr_expr,'ta) abstract_argument_type
 val globwit_constr : (rawconstr_and_expr,rawconstr_and_expr,'ta) abstract_argument_type
 val wit_constr : (constr,constr,'ta) abstract_argument_type
 
-val rawwit_constr_may_eval : ((constr_expr,reference or_metanum) may_eval,constr_expr,'ta) abstract_argument_type
-val globwit_constr_may_eval : ((rawconstr_and_expr,evaluable_global_reference and_short_name or_var or_metanum) may_eval,rawconstr_and_expr,'ta) abstract_argument_type
+val rawwit_constr_may_eval : ((constr_expr,reference) may_eval,constr_expr,'ta) abstract_argument_type
+val globwit_constr_may_eval : ((rawconstr_and_expr,evaluable_global_reference and_short_name or_var) may_eval,rawconstr_and_expr,'ta) abstract_argument_type
 val wit_constr_may_eval : (constr,constr,'ta) abstract_argument_type
 
 val rawwit_casted_open_constr : (open_constr_expr,constr_expr,'ta) abstract_argument_type
@@ -122,8 +121,8 @@ val rawwit_constr_with_bindings : (constr_expr with_bindings,constr_expr,'ta) ab
 val globwit_constr_with_bindings : (rawconstr_and_expr with_bindings,rawconstr_and_expr,'ta) abstract_argument_type
 val wit_constr_with_bindings : (constr with_bindings,constr,'ta) abstract_argument_type
 
-val rawwit_red_expr : ((constr_expr,reference or_metanum) red_expr_gen,constr_expr,'ta) abstract_argument_type
-val globwit_red_expr : ((rawconstr_and_expr,evaluable_global_reference and_short_name or_var or_metanum) red_expr_gen,rawconstr_and_expr,'ta) abstract_argument_type
+val rawwit_red_expr : ((constr_expr,reference) red_expr_gen,constr_expr,'ta) abstract_argument_type
+val globwit_red_expr : ((rawconstr_and_expr,evaluable_global_reference and_short_name or_var) red_expr_gen,rawconstr_and_expr,'ta) abstract_argument_type
 val wit_red_expr : ((constr,evaluable_global_reference) red_expr_gen,constr,'ta) abstract_argument_type
 
 (* TODO: transformer tactic en extra arg *)
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 ->
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 0e76558f1f..0b665d4b29 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -203,7 +203,7 @@ let pretype_sort = function
 (* [pretype tycon env isevars lvar lmeta cstr] attempts to type [cstr] *)
 (* in environment [env], with existential variables [(evars_of isevars)] and *)
 (* the type constraint tycon *)
-let rec pretype tycon env isevars lvar lmeta = function
+let rec pretype tycon env isevars lvar = function
 
   | RRef (loc,ref) ->
       inh_conv_coerce_to_tycon loc env isevars
@@ -224,17 +224,8 @@ let rec pretype tycon env isevars lvar lmeta = function
       let j = (Retyping.get_judgment_of env (evars_of isevars) c) in
       inh_conv_coerce_to_tycon loc env isevars j tycon
 
-  | RPatVar (loc,(someta,n)) ->
-      assert (not someta);
-      let j =
-	try
-	  List.assoc n (lmeta@lvar)
-	with
-            Not_found ->
-	      user_err_loc
-		(loc,"pretype",
-		 str "Metavariable " ++ pr_patvar n ++ str " is unbound")
-      in inh_conv_coerce_to_tycon loc env isevars j tycon
+  | RPatVar (loc,(someta,n)) -> 
+      anomaly "Found a pattern variable in a rawterm to type"
 	   
   | RHole (loc,k) ->
       if !compter then nbimpl:=!nbimpl+1;
@@ -245,7 +236,7 @@ let rec pretype tycon env isevars lvar lmeta = function
 
   | RRec (loc,fixkind,names,lar,vdef) ->
       let larj =
-        Array.map (pretype_type empty_valcon env isevars lvar lmeta) lar in
+        Array.map (pretype_type empty_valcon env isevars lvar) lar in
       let lara = Array.map (fun a -> a.utj_val) larj in
       let nbfix = Array.length lar in
       let names = Array.map (fun id -> Name id) names in
@@ -255,7 +246,7 @@ let rec pretype tycon env isevars lvar lmeta = function
 	  (fun i def -> (* we lift nbfix times the type in tycon, because of
 			 * the nbfix variables pushed to newenv *)
              pretype (mk_tycon (lift nbfix (larj.(i).utj_val)))
-               newenv isevars lvar lmeta def)
+               newenv isevars lvar def)
           vdef in
       evar_type_fixpoint loc env isevars names lara vdefj;
       let fixj =
@@ -274,7 +265,7 @@ let rec pretype tycon env isevars lvar lmeta = function
       inh_conv_coerce_to_tycon loc env isevars (pretype_sort s) tycon
 
   | RApp (loc,f,args) -> 
-      let fj = pretype empty_tycon env isevars lvar lmeta f in
+      let fj = pretype empty_tycon env isevars lvar f in
       let floc = loc_of_rawconstr f in
       let rec apply_rec env n resj = function
 	| [] -> resj
@@ -285,14 +276,14 @@ let rec pretype tycon env isevars lvar lmeta = function
               whd_betadeltaiota env (evars_of isevars) resj.uj_type in
       	    match kind_of_term resty with
 	      | Prod (na,c1,c2) ->
-		  let hj = pretype (mk_tycon c1) env isevars lvar lmeta c in
+		  let hj = pretype (mk_tycon c1) env isevars lvar c in
 		  let newresj =
       		    { uj_val = applist (j_val resj, [j_val hj]);
 		      uj_type = subst1 hj.uj_val c2 } in
 		  apply_rec env (n+1) newresj rest
 
 	      | _ ->
-		  let hj = pretype empty_tycon env isevars lvar lmeta c in
+		  let hj = pretype empty_tycon env isevars lvar c in
 		  error_cant_apply_not_functional_loc 
 		    (join_loc floc argloc) env (evars_of isevars)
 	      	    resj [hj]
@@ -301,7 +292,7 @@ let rec pretype tycon env isevars lvar lmeta = function
       (*
 	let apply_one_arg (floc,tycon,jl) c =
 	let (dom,rng) = split_tycon floc env isevars tycon in
-	let cj = pretype dom env isevars lvar lmeta c in
+	let cj = pretype dom env isevars lvar c in
 	let rng_tycon = option_app (subst1 cj.uj_val) rng in
 	let argloc = loc_of_rawconstr c in
 	(join_loc floc argloc,rng_tycon,(argloc,cj)::jl)  in
@@ -315,33 +306,33 @@ let rec pretype tycon env isevars lvar lmeta = function
   | RLambda(loc,name,c1,c2)      ->
       let (dom,rng) = split_tycon loc env isevars tycon in
       let dom_valcon = valcon_of_tycon dom in
-      let j = pretype_type dom_valcon env isevars lvar lmeta c1 in
+      let j = pretype_type dom_valcon env isevars lvar c1 in
       let var = (name,None,j.utj_val) in
-      let j' = pretype rng (push_rel var env) isevars lvar lmeta c2 in 
+      let j' = pretype rng (push_rel var env) isevars lvar c2 in 
       judge_of_abstraction env name j j'
 
   | RProd(loc,name,c1,c2)        ->
-      let j = pretype_type empty_valcon env isevars lvar lmeta c1 in
+      let j = pretype_type empty_valcon env isevars lvar c1 in
       let var = (name,j.utj_val) in
       let env' = push_rel_assum var env in
-      let j' = pretype_type empty_valcon env' isevars lvar lmeta c2 in
+      let j' = pretype_type empty_valcon env' isevars lvar c2 in
       let resj =
 	try judge_of_product env name j j'
 	with TypeError _ as e -> Stdpp.raise_with_loc loc e in
       inh_conv_coerce_to_tycon loc env isevars resj tycon
 	
   | RLetIn(loc,name,c1,c2)      ->
-      let j = pretype empty_tycon env isevars lvar lmeta c1 in
+      let j = pretype empty_tycon env isevars lvar c1 in
       let t = Evarutil.refresh_universes j.uj_type in
       let var = (name,Some j.uj_val,t) in
         let tycon = option_app (lift 1) tycon in
-      let j' = pretype tycon (push_rel var env) isevars lvar lmeta c2 in
+      let j' = pretype tycon (push_rel var env) isevars lvar c2 in
       { uj_val = mkLetIn (name, j.uj_val, t, j'.uj_val) ;
 	uj_type = type_app (subst1 j.uj_val) j'.uj_type }
 
   (* Special Case for let constructions to avoid exponential behavior *)      
   | ROrderedCase (loc,st,po,c,[|f|]) when st <> MatchStyle ->
-      let cj = pretype empty_tycon env isevars lvar lmeta c in
+      let cj = pretype empty_tycon env isevars lvar c in
       let (IndType (indf,realargs) as indt) = 
 	try find_rectype env (evars_of isevars) cj.uj_type
 	with Not_found ->
@@ -350,7 +341,7 @@ let rec pretype tycon env isevars lvar lmeta = function
       in
       (match po with
 	 | Some p ->
-             let pj = pretype empty_tycon env isevars lvar lmeta p in
+             let pj = pretype empty_tycon env isevars lvar p in
              let dep = is_dependent_elimination env pj.uj_type indf in
              let ar =
                arity_of_case_predicate env indf dep (Type (new_univ())) in
@@ -366,7 +357,7 @@ let rec pretype tycon env isevars lvar lmeta = function
 		 loc env (evars_of isevars) cj (Array.length bty);
 	     let fj = 
 	       let tyc = bty.(0) in 
-	       pretype (mk_tycon tyc) env isevars lvar lmeta f 
+	       pretype (mk_tycon tyc) env isevars lvar f 
 	     in
 	     let fv = j_val fj in
 	     let ft = fj.uj_type in
@@ -385,7 +376,7 @@ let rec pretype tycon env isevars lvar lmeta = function
 	       error_number_branches_loc loc env (evars_of isevars) 
 		 cj (Array.length expbr);
              let expti = expbr.(0) in
-	     let fj = pretype (mk_tycon expti) env isevars lvar lmeta f in
+	     let fj = pretype (mk_tycon expti) env isevars lvar f in
 	     let use_constraint () =
                (* get type information from constraint *)
                (* warning: if the constraint comes from an evar type, it *)
@@ -425,7 +416,7 @@ let rec pretype tycon env isevars lvar lmeta = function
 	     in
 	     let fj = 
 	       if ok then fj 
-	       else pretype (mk_tycon bty.(0)) env isevars lvar lmeta f 
+	       else pretype (mk_tycon bty.(0)) env isevars lvar f 
 	     in
 	     let fv = fj.uj_val in
 	     let ft = fj.uj_type in
@@ -438,7 +429,7 @@ let rec pretype tycon env isevars lvar lmeta = function
 
   | ROrderedCase (loc,st,po,c,lf) ->
       let isrec = (st = MatchStyle) in
-      let cj = pretype empty_tycon env isevars lvar lmeta c in
+      let cj = pretype empty_tycon env isevars lvar c in
       let (IndType (indf,realargs) as indt) = 
 	try find_rectype env (evars_of isevars) cj.uj_type
 	with Not_found ->
@@ -446,7 +437,7 @@ let rec pretype tycon env isevars lvar lmeta = function
 	  error_case_not_inductive_loc cloc env (evars_of isevars) cj in
       let (dep,pj) = match po with
 	| Some p ->
-            let pj = pretype empty_tycon env isevars lvar lmeta p in
+            let pj = pretype empty_tycon env isevars lvar p in
             let dep = is_dependent_elimination env pj.uj_type indf in
             let ar =
               arity_of_case_predicate env indf dep (Type (new_univ())) in
@@ -472,7 +463,7 @@ let rec pretype tycon env isevars lvar lmeta = function
 		try
 		  let expti = expbr.(i) in
 		  let fj =
-		    pretype (mk_tycon expti) env isevars lvar lmeta lf.(i) in
+		    pretype (mk_tycon expti) env isevars lvar lf.(i) in
 		  let pred = 
 		    Cases.pred_case_ml
                       env (evars_of isevars) isrec indt (i,fj.uj_type) in
@@ -497,7 +488,7 @@ let rec pretype tycon env isevars lvar lmeta = function
       else
 	let lfj =
 	  array_map2
-            (fun tyc f -> pretype (mk_tycon tyc) env isevars lvar lmeta f) bty
+            (fun tyc f -> pretype (mk_tycon tyc) env isevars lvar f) bty
             lf in
 	let lfv = Array.map j_val lfj in
 	let lft = Array.map (fun j -> j.uj_type) lfj in
@@ -517,12 +508,12 @@ let rec pretype tycon env isevars lvar lmeta = function
 
   | RCases (loc,po,tml,eqns) ->
       Cases.compile_cases loc
-	((fun vtyc env -> pretype vtyc env isevars lvar lmeta),isevars)
+	((fun vtyc env -> pretype vtyc env isevars lvar),isevars)
 	tycon env (* loc *) (po,tml,eqns)
 
   | RCast(loc,c,t) ->
-      let tj = pretype_type empty_tycon env isevars lvar lmeta t in
-      let cj = pretype (mk_tycon tj.utj_val) env isevars lvar lmeta c in
+      let tj = pretype_type empty_tycon env isevars lvar t in
+      let cj = pretype (mk_tycon tj.utj_val) env isevars lvar c in
       (* User Casts are for helping pretyping, experimentally not to be kept*)
       (* ... except for Correctness *)
       let v = mkCast (cj.uj_val, tj.utj_val) in
@@ -538,8 +529,8 @@ let rec pretype tycon env isevars lvar lmeta = function
     else
       user_err_loc (loc,"pretype",(str "Not a constr tagged Dynamic"))
 
-(* [pretype_type valcon env isevars lvar lmeta c] coerces [c] into a type *)
-and pretype_type valcon env isevars lvar lmeta = function
+(* [pretype_type valcon env isevars lvar c] coerces [c] into a type *)
+and pretype_type valcon env isevars lvar = function
   | RHole loc ->
       if !compter then nbimpl:=!nbimpl+1;
       (match valcon with
@@ -551,7 +542,7 @@ and pretype_type valcon env isevars lvar lmeta = function
 	     { utj_val = new_isevar isevars env loc (mkSort s);
 	       utj_type = s})
   | c ->
-      let j = pretype empty_tycon env isevars lvar lmeta c in
+      let j = pretype empty_tycon env isevars lvar c in
       let tj = inh_coerce_to_sort env isevars j in
       match valcon with
 	| None -> tj
@@ -562,12 +553,12 @@ and pretype_type valcon env isevars lvar lmeta = function
                 (loc_of_rawconstr c) env (evars_of isevars) tj.utj_val v
 
 
-let unsafe_infer tycon isevars env lvar lmeta constr =
-  let j = pretype tycon env isevars lvar lmeta constr in
+let unsafe_infer tycon isevars env lvar constr =
+  let j = pretype tycon env isevars lvar constr in
   j_nf_evar (evars_of isevars) j
 
-let unsafe_infer_type valcon isevars env lvar lmeta constr =
-  let tj = pretype_type valcon env isevars lvar lmeta constr in
+let unsafe_infer_type valcon isevars env lvar constr =
+  let tj = pretype_type valcon env isevars lvar constr in
   tj_nf_evar (evars_of isevars) tj
 
 (* If fail_evar is false, [process_evars] builds a meta_map with the
@@ -601,54 +592,53 @@ let check_evars fail_evar env initial_sigma isevars c =
 (* constr with holes *)
 type open_constr = evar_map * constr
 
-let ise_resolve_casted_gen fail_evar sigma env lvar lmeta typ c =
+let ise_resolve_casted_gen fail_evar sigma env lvar typ c =
   let isevars = create_evar_defs sigma in
-  let j = unsafe_infer (mk_tycon typ) isevars env lvar lmeta c in
+  let j = unsafe_infer (mk_tycon typ) isevars env lvar c in
   check_evars fail_evar env sigma isevars (mkCast(j.uj_val,j.uj_type));
   (evars_of isevars, j)
 
 let ise_resolve_casted sigma env typ c =
-  ise_resolve_casted_gen true sigma env [] [] typ c
+  ise_resolve_casted_gen true sigma env [] typ c
 
 (* Raw calls to the unsafe inference machine: boolean says if we must fail
    on unresolved evars, or replace them by Metas; the unsafe_judgment list
    allows us to extend env with some bindings *)
-let ise_infer_gen fail_evar sigma env lvar lmeta exptyp c =
+let ise_infer_gen fail_evar sigma env lvar exptyp c =
   let tycon = match exptyp with None -> empty_tycon | Some t -> mk_tycon t in
   let isevars = create_evar_defs sigma in
-  let j = unsafe_infer tycon isevars env lvar lmeta c in
+  let j = unsafe_infer tycon isevars env lvar c in
   check_evars fail_evar env sigma isevars (mkCast(j.uj_val,j.uj_type));
   (evars_of isevars, j)
 
-let ise_infer_type_gen fail_evar sigma env lvar lmeta c =
+let ise_infer_type_gen fail_evar sigma env lvar c =
   let isevars = create_evar_defs sigma in
-  let tj = unsafe_infer_type empty_valcon isevars env lvar lmeta c in
+  let tj = unsafe_infer_type empty_valcon isevars env lvar c in
   check_evars fail_evar env sigma isevars tj.utj_val;
   (evars_of isevars, tj)
 
-type meta_map = (patvar * unsafe_judgment) list
 type var_map = (identifier * unsafe_judgment) list
 
 let understand_judgment sigma env c =
-  snd (ise_infer_gen true sigma env [] [] None c)
+  snd (ise_infer_gen true sigma env [] None c)
 
 let understand_type_judgment sigma env c =
-  snd (ise_infer_type_gen true sigma env [] [] c)
+  snd (ise_infer_type_gen true sigma env [] c)
 
 let understand sigma env c =
-  let _, c = ise_infer_gen true sigma env [] [] None c in
+  let _, c = ise_infer_gen true sigma env [] None c in
   c.uj_val
 
 let understand_type sigma env c =
-  let _,c = ise_infer_type_gen true sigma env [] [] c in
+  let _,c = ise_infer_type_gen true sigma env [] c in
   c.utj_val
 
-let understand_gen sigma env lvar lmeta ~expected_type:exptyp c =
-  let _, c = ise_infer_gen true sigma env lvar lmeta exptyp c in
+let understand_gen sigma env lvar ~expected_type:exptyp c =
+  let _, c = ise_infer_gen true sigma env lvar exptyp c in
   c.uj_val
 
-let understand_gen_tcc sigma env lvar lmeta exptyp c =
-  let metamap, c = ise_infer_gen false sigma env lvar lmeta exptyp c in
+let understand_gen_tcc sigma env lvar exptyp c =
+  let metamap, c = ise_infer_gen false sigma env lvar exptyp c in
   metamap, c.uj_val
 
 let interp_sort = function
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index e6dc58896c..7558de0ff2 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -18,7 +18,6 @@ open Rawterm
 open Evarutil
 (*i*)
 
-type meta_map = (patvar * unsafe_judgment) list
 type var_map = (identifier * unsafe_judgment) list
 
 (* constr with holes *)
@@ -28,7 +27,7 @@ type open_constr = evar_map * constr
 (* Generic call to the interpreter from rawconstr to constr, failing
    unresolved holes in the rawterm cannot be instantiated.
 
-   In [understand_gen sigma env varmap metamap typopt raw],
+   In [understand_gen sigma env varmap typopt raw],
 
    sigma : initial set of existential variables (typically dependent subgoals)
    varmap : partial subtitution of variables (used for the tactic language)
@@ -36,7 +35,7 @@ type open_constr = evar_map * constr
    typopt : is not None, this is the expected type for raw (used to define evars)
 *)
 val understand_gen :
-  evar_map -> env -> var_map -> meta_map 
+  evar_map -> env -> var_map
     -> expected_type:(constr option) -> rawconstr -> constr
 
 
@@ -44,7 +43,7 @@ val understand_gen :
    unresolved holes into metas. Returns also the typing context of
    these metas. Work as [understand_gen] for the rest. *)
 val understand_gen_tcc :
-  evar_map -> env -> var_map -> meta_map 
+  evar_map -> env -> var_map
     -> constr option -> rawconstr -> open_constr
 
 (* Standard call to get a constr from a rawconstr, resolving implicit args *)
@@ -69,11 +68,11 @@ val constr_out : Dyn.t -> constr
  * Unused outside, but useful for debugging
  *)
 val pretype : 
-  type_constraint -> env -> evar_defs -> var_map -> meta_map ->
+  type_constraint -> env -> evar_defs -> var_map ->
     rawconstr -> unsafe_judgment
 
 val pretype_type : 
-  val_constraint -> env -> evar_defs -> var_map -> meta_map ->
+  val_constraint -> env -> evar_defs -> var_map ->
     rawconstr -> unsafe_type_judgment
 (*i*)
 
diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml
index b905c0a26b..c8b4fc3ea1 100644
--- a/proofs/proof_type.ml
+++ b/proofs/proof_type.ml
@@ -71,7 +71,7 @@ and tactic_expr =
   (constr,
    constr_pattern,
    evaluable_global_reference,
-   inductive or_metanum,
+   inductive,
    ltac_constant,
    identifier,
    glob_tactic_expr)
@@ -81,7 +81,7 @@ and atomic_tactic_expr =
   (constr,
    constr_pattern,
    evaluable_global_reference,
-   inductive or_metanum,
+   inductive,
    ltac_constant,
    identifier,
    glob_tactic_expr)
@@ -91,7 +91,7 @@ and tactic_arg =
   (constr,
    constr_pattern,
    evaluable_global_reference,
-   inductive or_metanum,
+   inductive,
    ltac_constant,
    identifier,
    glob_tactic_expr)
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli
index 9337408824..7cbb2355a8 100644
--- a/proofs/proof_type.mli
+++ b/proofs/proof_type.mli
@@ -99,7 +99,7 @@ and tactic_expr =
   (constr,
    constr_pattern,
    evaluable_global_reference,
-   inductive or_metanum,
+   inductive,
    ltac_constant,
    identifier,
    glob_tactic_expr)
@@ -109,7 +109,7 @@ and atomic_tactic_expr =
   (constr,
    constr_pattern,
    evaluable_global_reference,
-   inductive or_metanum,
+   inductive,
    ltac_constant,
    identifier,
    glob_tactic_expr)
@@ -119,7 +119,7 @@ and tactic_arg =
   (constr,
    constr_pattern,
    evaluable_global_reference,
-   inductive or_metanum,
+   inductive,
    ltac_constant,
    identifier,
    glob_tactic_expr)
diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index 2adc93ee50..860a91aff3 100644
--- a/proofs/tacexpr.ml
+++ b/proofs/tacexpr.ml
@@ -25,13 +25,8 @@ type raw_red_flag =
   | FBeta
   | FIota
   | FZeta
-  | FConst of reference or_metanum list
-  | FDeltaBut of reference or_metanum list
-
-type raw_red_expr = (constr_expr, reference or_metanum) red_expr_gen
-
-type glob_red_expr =
-    (rawconstr_and_expr, evaluable_global_reference or_var or_metanum) red_expr_gen
+  | FConst of reference list
+  | FDeltaBut of reference list
 
 let make_red_flag =
   let rec add_flag red = function
@@ -138,10 +133,10 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr =
   | TacDAuto of int option * int option
 
   (* Context management *)
-  | TacClear of identifier or_metanum list
-  | TacClearBody of identifier or_metanum list
-  | TacMove of bool * identifier located * identifier located
-  | TacRename of identifier located * identifier located
+  | TacClear of 'id list
+  | TacClearBody of 'id list
+  | TacMove of bool * 'id * 'id
+  | TacRename of 'id * 'id
 
   (* Constructors *)
   | TacLeft of 'constr bindings
@@ -211,8 +206,8 @@ and ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_arg =
 type raw_tactic_expr =
     (constr_expr,
      pattern_expr,
-     reference or_metanum,
-     reference or_metanum,
+     reference,
+     reference,
      reference,
      identifier located or_metaid,
      raw_tactic_expr) gen_tactic_expr
@@ -220,8 +215,8 @@ type raw_tactic_expr =
 type raw_atomic_tactic_expr =
     (constr_expr,                  (* constr *)
      pattern_expr,                 (* pattern *)
-     reference or_metanum,         (* evaluable reference *)
-     reference or_metanum,         (* inductive *)
+     reference,                    (* evaluable reference *)
+     reference,                    (* inductive *)
      reference,                    (* ltac reference *)
      identifier located or_metaid, (* identifier *)
      raw_tactic_expr) gen_atomic_tactic_expr
@@ -229,8 +224,8 @@ type raw_atomic_tactic_expr =
 type raw_tactic_arg =
     (constr_expr,
      pattern_expr,
-     reference or_metanum,
-     reference or_metanum,
+     reference,
+     reference,
      reference,
      identifier located or_metaid,
      raw_tactic_expr) gen_tactic_arg
@@ -238,12 +233,14 @@ type raw_tactic_arg =
 type raw_generic_argument =
     (constr_expr,raw_tactic_expr) generic_argument
 
+type raw_red_expr = (constr_expr, reference) red_expr_gen
+
 (* Globalized tactics *)
 type glob_tactic_expr =
     (rawconstr_and_expr,
      constr_pattern,
-     evaluable_global_reference and_short_name or_var or_metanum,
-     inductive or_var or_metanum,
+     evaluable_global_reference and_short_name or_var,
+     inductive or_var,
      ltac_constant located or_var,
      identifier located,
      glob_tactic_expr) gen_tactic_expr
@@ -251,8 +248,8 @@ type glob_tactic_expr =
 type glob_atomic_tactic_expr =
     (rawconstr_and_expr,
      constr_pattern,
-     evaluable_global_reference and_short_name or_var or_metanum,
-     inductive or_var or_metanum,
+     evaluable_global_reference and_short_name or_var,
+     inductive or_var,
      ltac_constant located or_var,
      identifier located,
      glob_tactic_expr) gen_atomic_tactic_expr
@@ -260,15 +257,18 @@ type glob_atomic_tactic_expr =
 type glob_tactic_arg =
     (rawconstr_and_expr,
      constr_pattern,
-     evaluable_global_reference and_short_name or_var or_metanum,
-     inductive or_var or_metanum,
-     ltac_constant located or_var,
-     identifier located,
+     evaluable_global_reference and_short_name or_var,
+     inductive or_var,
+     ltac_constant located,
+     identifier located or_var,
      glob_tactic_expr) gen_tactic_arg
 
 type glob_generic_argument =
     (rawconstr_and_expr,glob_tactic_expr) generic_argument
 
+type glob_red_expr =
+    (rawconstr_and_expr, evaluable_global_reference or_var) red_expr_gen
+
 type closed_raw_generic_argument =
     (constr_expr,raw_tactic_expr) generic_argument
 
diff --git a/tactics/elim.ml b/tactics/elim.ml
index 9ced398dda..1dcdec03df 100644
--- a/tactics/elim.ml
+++ b/tactics/elim.ml
@@ -128,10 +128,8 @@ let decompose_or c gls =
     (fun (_,t) -> is_disjunction t)
     c gls
 
-let inj x = Genarg.AN x
 let h_decompose l c =
-  Refiner.abstract_tactic
-    (TacDecompose (List.map inj l,c)) (decompose_these c l)
+  Refiner.abstract_tactic (TacDecompose (l,c)) (decompose_these c l)
 
 let h_decompose_or c =
   Refiner.abstract_tactic (TacDecomposeOr c) (decompose_or c)
diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml
index a502b41100..8e953084da 100644
--- a/tactics/hiddentac.ml
+++ b/tactics/hiddentac.ml
@@ -60,14 +60,12 @@ let h_specialize n d = abstract_tactic (TacSpecialize (n,d)) (new_hyp n d)
 let h_lapply c = abstract_tactic (TacLApply c) (cut_and_apply c)
 
 (* Context management *)
-let inj x = Genarg.AN x
-let h_clear l = abstract_tactic (TacClear (List.map inj l)) (clear l)
-let h_clear_body l =
-  abstract_tactic (TacClearBody (List.map inj l)) (clear_body l)
+let h_clear l = abstract_tactic (TacClear l) (clear l)
+let h_clear_body l = abstract_tactic (TacClearBody l) (clear_body l)
 let h_move dep id1 id2 =
-  abstract_tactic (TacMove (dep,inj_id id1,inj_id id2)) (move_hyp dep id1 id2)
+  abstract_tactic (TacMove (dep,id1,id2)) (move_hyp dep id1 id2)
 let h_rename id1 id2 =
-  abstract_tactic (TacRename (inj_id id1,inj_id id2)) (rename_hyp id1 id2)
+  abstract_tactic (TacRename (id1,id2)) (rename_hyp id1 id2)
 
 (* Constructors *)
 let h_left l          = abstract_tactic (TacLeft l) (left l)
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index b065aac186..02e7e8fb4a 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -91,7 +91,6 @@ let catch_error loc tac g =
 (* Signature for interpretation: val_interp and interpretation functions *)
 type interp_sign =
   { lfun : (identifier * value) list;
-    lmatch : patvar_map;
     debug : debug_info }
 
 let check_is_value = function
@@ -260,8 +259,6 @@ type glob_sign = {
      (* ltac variables and the subset of vars introduced by Intro/Let/... *)
   ltacrecvars : (identifier * ltac_constant) list;
      (* ltac recursive names *)
-  metavars : patvar list;
-     (* metavariables introduced by patterns *)
   gsigma : Evd.evar_map;
   genv : Environ.env }
 
@@ -335,34 +332,21 @@ let get_current_context () =
 let strict_check = ref false
 
 (* Globalize a name which must be bound -- actually just check it is bound *)
-let intern_hyp ist (loc,id) =
+let intern_hyp ist (loc,id as locid) =
   let (_,env) = get_current_context () in
-  if (not !strict_check) or find_ident id ist then id
+  if not !strict_check then
+    locid
+  else if find_ident id ist then
+    (dummy_loc,id)
   else
     Pretype_errors.error_var_not_found_loc loc id
 
-let intern_lochyp ist (_loc,_ as locid) = (loc,intern_hyp ist locid)
-
-let error_unbound_metanum loc n =
-  user_err_loc
-  (loc,"intern_qualid_or_metanum", str "?" ++ pr_patvar n ++ str " is unbound")
-
-let intern_metanum sign loc n =
-  if List.mem n sign.metavars or find_var n sign then n
-  else error_unbound_metanum loc n
-
-let intern_hyp_or_metanum ist = function
-  | AN id -> AN (intern_hyp ist (loc,id))
-  | MetaNum (_loc,n) -> MetaNum (loc,intern_metanum ist loc n)
+let intern_hyp_or_metaid ist id = intern_hyp ist (skip_metaid id)
 
 let intern_inductive ist = function
   | Ident (loc,id) when find_var id ist -> ArgVar (loc,id)
   | r -> ArgArg (Nametab.global_inductive r)
 
-let intern_or_metanum f ist = function
-  | AN x -> AN (f ist x)
-  | MetaNum (_loc,n) -> MetaNum (loc,intern_metanum ist loc n)
-
 let intern_global_reference ist = function
   | Ident (loc,id) as r when find_var id ist -> ArgVar (loc,id)
   | r -> ArgArg (loc,Nametab.global r)
@@ -414,11 +398,11 @@ let intern_quantified_hypothesis ist x =
      statically check the existence of a quantified hyp); thus nothing to do *)
   x
 
-let intern_constr {ltacvars=lfun; metavars=lmatch; gsigma=sigma; genv=env} c =
+let intern_constr {ltacvars=lfun; gsigma=sigma; genv=env} c =
   let warn = if !strict_check then fun x -> x else Constrintern.for_grammar in
   let c' = 
     warn (Constrintern.interp_rawconstr_gen false sigma env []
-           (Some lmatch) (fst lfun,[])) c
+           false (fst lfun,[])) c
   in (c',if !strict_check then None else Some c)
 
 (* Globalize bindings *)
@@ -437,7 +421,7 @@ let intern_clause_pattern ist (l,occl) =
   let rec check = function
     | (hyp,l) :: rest -> 
 	let (_loc,_ as id) = skip_metaid hyp in
-	((loc,intern_hyp ist id),l)::(check rest)
+	(intern_hyp ist id,l)::(check rest)
     | [] -> []
   in (l,check occl)
 
@@ -453,36 +437,32 @@ let intern_induction_arg ist = function
 	ElimOnIdent (loc,id)
 
 (* Globalizes a reduction expression *)
-let intern_evaluable_or_metanum ist = function
-  | AN r ->
-      let e = match r with
-        | Ident (loc,id) as r when find_ltacvar id ist -> ArgVar (loc,id)
-	| Ident (_,id) when
-	    (not !strict_check & find_hyp id ist) or find_ctxvar id ist ->
-	    ArgArg (EvalVarRef id, None)
-	| r ->
-	    let _,qid = qualid_of_reference r in
-	    try
-	      let e = match Nametab.locate qid with
-		| ConstRef c -> EvalConstRef c
-		| VarRef c -> EvalVarRef c
-		| _ -> error_not_evaluable (pr_reference r) in
-              let short_name = match r with
-		| Ident (loc,id) when not !strict_check -> Some (loc,id)
-		| _ -> None in
-              ArgArg (e,short_name)
-	    with Not_found ->
-	      match r with 
-		| Ident (loc,id) when not !strict_check ->
-		    ArgArg (EvalVarRef id, Some (loc,id))
-		| _ -> error_global_not_found_loc loc qid
-      in AN e
-  | MetaNum (_loc,n) -> MetaNum (loc,intern_metanum ist loc n)
-
-let intern_unfold ist (l,qid) = (l,intern_evaluable_or_metanum ist qid)
+let intern_evaluable ist = function
+  | Ident (loc,id) as r when find_ltacvar id ist -> ArgVar (loc,id)
+  | Ident (_,id) when
+      (not !strict_check & find_hyp id ist) or find_ctxvar id ist ->
+      ArgArg (EvalVarRef id, None)
+  | r ->
+      let _,qid = qualid_of_reference r in
+      try
+	let e = match Nametab.locate qid with
+	  | ConstRef c -> EvalConstRef c
+	  | VarRef c -> EvalVarRef c
+	  | _ -> error_not_evaluable (pr_reference r) in
+        let short_name = match r with
+	  | Ident (loc,id) when not !strict_check -> Some (loc,id)
+	  | _ -> None in
+        ArgArg (e,short_name)
+      with Not_found ->
+	match r with 
+	  | Ident (loc,id) when not !strict_check ->
+	      ArgArg (EvalVarRef id, Some (loc,id))
+	  | _ -> error_global_not_found_loc loc qid
+
+let intern_unfold ist (l,qid) = (l,intern_evaluable ist qid)
 
 let intern_flag ist red =
-  { red with rConst = List.map (intern_evaluable_or_metanum ist) red.rConst }
+  { red with rConst = List.map (intern_evaluable ist) red.rConst }
 
 let intern_constr_occurrence ist (l,c) = (l,intern_constr ist c)
 
@@ -500,10 +480,10 @@ let intern_redexp ist = function
 let intern_hyp_location ist = function
   | InHyp id ->
       let (_loc,_ as id) = skip_metaid id in
-      InHyp (loc,intern_hyp ist id)
+      InHyp (intern_hyp ist id)
   | InHypType id -> 
       let (_loc,_ as id) = skip_metaid id in
-      InHypType (loc,intern_hyp ist id)
+      InHypType (intern_hyp ist id)
 
 (* Reads a pattern *)
 let intern_pattern evc env lfun = function
@@ -519,7 +499,7 @@ let intern_pattern evc env lfun = function
 let intern_constr_may_eval ist = function
   | ConstrEval (r,c) -> ConstrEval (intern_redexp ist r,intern_constr ist c)
   | ConstrContext (locid,c) ->
-      ConstrContext ((loc,intern_hyp ist locid),intern_constr ist c)
+      ConstrContext (intern_hyp ist locid,intern_constr ist c)
   | ConstrTypeOf c -> ConstrTypeOf (intern_constr ist c)
   | ConstrTerm c -> ConstrTerm (intern_constr ist c)
 
@@ -564,7 +544,7 @@ let rec intern_atomic lf ist x =
   | TacIntrosUntil hyp -> TacIntrosUntil (intern_quantified_hypothesis ist hyp)
   | TacIntroMove (ido,ido') ->
       TacIntroMove (option_app (intern_ident lf ist) ido,
-          option_app (fun (_loc,_ as x) -> (loc,intern_hyp ist x)) ido')
+          option_app (intern_hyp ist) ido')
   | TacAssumption -> TacAssumption
   | TacExact c -> TacExact (intern_constr ist c)
   | TacApply cb -> TacApply (intern_constr_with_bindings ist cb)
@@ -597,8 +577,7 @@ let rec intern_atomic lf ist x =
   | TacTrivial l -> TacTrivial l
   | TacAuto (n,l) -> TacAuto (n,l)
   | TacAutoTDB n -> TacAutoTDB n
-  | TacDestructHyp (b,(_loc,_ as id)) ->
-      TacDestructHyp(b,(loc,intern_hyp ist id))
+  | TacDestructHyp (b,id) -> TacDestructHyp(b,intern_hyp ist id)
   | TacDestructConcl -> TacDestructConcl
   | TacSuperAuto (n,l,b1,b2) -> TacSuperAuto (n,l,b1,b2)
   | TacDAuto (n,p) -> TacDAuto (n,p)
@@ -620,18 +599,17 @@ let rec intern_atomic lf ist x =
       TacDoubleInduction (h1,h2)
   | TacDecomposeAnd c -> TacDecomposeAnd (intern_constr ist c)
   | TacDecomposeOr c -> TacDecomposeOr (intern_constr ist c)
-  | TacDecompose (l,c) ->
-      let l = List.map (intern_or_metanum intern_inductive ist) l in
+  | TacDecompose (l,c) -> let l = List.map (intern_inductive ist) l in
       TacDecompose (l,intern_constr ist c)
   | TacSpecialize (n,l) -> TacSpecialize (n,intern_constr_with_bindings ist l)
   | TacLApply c -> TacLApply (intern_constr ist c)
 
   (* Context management *)
-  | TacClear l -> TacClear (List.map (intern_hyp_or_metanum ist) l)
-  | TacClearBody l -> TacClearBody (List.map (intern_hyp_or_metanum ist) l)
+  | TacClear l -> TacClear (List.map (intern_hyp_or_metaid ist) l)
+  | TacClearBody l -> TacClearBody (List.map (intern_hyp_or_metaid ist) l)
   | TacMove (dep,id1,id2) ->
-    TacMove (dep,intern_lochyp ist id1,intern_lochyp ist id2)
-  | TacRename (id1,id2) -> TacRename (intern_lochyp ist id1, intern_lochyp ist id2)
+    TacMove (dep,intern_hyp_or_metaid ist id1,intern_hyp_or_metaid ist id2)
+  | TacRename (id1,id2) -> TacRename (intern_hyp_or_metaid ist id1, intern_hyp_or_metaid ist id2)
 
   (* Constructors *)
   | TacLeft bl -> TacLeft (intern_bindings ist bl)
@@ -746,11 +724,11 @@ and intern_match_rule ist = function
   | (All tc)::tl ->
       All (intern_tactic ist tc) :: (intern_match_rule ist tl)
   | (Pat (rl,mp,tc))::tl ->
-      let {ltacvars=(lfun,l2); metavars=lmeta; gsigma=sigma; genv=env} = ist in
+      let {ltacvars=(lfun,l2); gsigma=sigma; genv=env} = ist in
       let lfun',metas1,hyps = intern_match_context_hyps sigma env lfun rl in
       let metas2,pat = intern_pattern sigma env lfun mp in
-      let metas = list_uniquize (metas1@metas2@lmeta) in
-      let ist' = { ist with ltacvars = (metas@lfun',l2); metavars = [] } in
+      let metas = list_uniquize (metas1@metas2) in
+      let ist' = { ist with ltacvars = (metas@lfun',l2) } in
       Pat (hyps,pat,intern_tactic ist' tc) :: (intern_match_rule ist tl)
   | [] -> []
 
@@ -760,7 +738,7 @@ and intern_genarg ist x =
   | IntArgType -> in_gen globwit_int (out_gen rawwit_int x)
   | IntOrVarArgType ->
       let f = function
-	| ArgVar (_loc,id) -> ArgVar (loc,intern_hyp ist (loc,id))
+	| ArgVar (_loc,id) -> ArgVar (intern_hyp ist (loc,id))
 	| ArgArg n as x -> x in
       in_gen globwit_int_or_var (f (out_gen rawwit_int_or_var x))
   | StringArgType ->
@@ -768,7 +746,7 @@ and intern_genarg ist x =
   | PreIdentArgType ->
       in_gen globwit_pre_ident (out_gen rawwit_pre_ident x)
   | IdentArgType ->
-      in_gen globwit_ident (intern_hyp ist (dummy_loc,out_gen rawwit_ident x))
+      in_gen globwit_ident (snd (intern_hyp ist (dummy_loc,out_gen rawwit_ident x)))
   | RefArgType ->
       in_gen globwit_ref (intern_global_reference ist (out_gen rawwit_ref x))
   | SortArgType ->
@@ -1004,10 +982,6 @@ let eval_name ist = function
   | Anonymous -> Anonymous
   | Name id -> Name (eval_ident ist id)
 
-let interp_hyp_or_metanum ist gl = function
-  | AN id -> eval_variable ist gl (dummy_loc,id)
-  | MetaNum (loc,n) -> constr_to_id loc (List.assoc n ist.lfun)
-
 (* To avoid to move to much simple functions in the big recursive block *)
 let forward_vcontext_interp = ref (fun ist v -> failwith "not implemented")
 
@@ -1031,30 +1005,23 @@ let interp_reference ist env = function
 
 let pf_interp_reference ist gl = interp_reference ist (pf_env gl)
 
-let interp_inductive_or_metanum ist = function
-  | MetaNum (loc,n) ->
-      coerce_to_inductive (List.assoc n ist.lfun)
-  | AN r -> match r with
-      | ArgArg r -> r
-      | ArgVar (_,id) -> 
-          coerce_to_inductive (unrec (List.assoc id ist.lfun))
-
-let interp_evaluable_or_metanum ist env = function
-  | MetaNum (loc,n) ->
-      coerce_to_evaluable_ref env (List.assoc n ist.lfun)
-  | AN r -> match r with
-      | ArgArg (r,Some (loc,id)) ->
-          (* Maybe [id] has been introduced by Intro-like tactics *)
-          (try match Environ.lookup_named id env with
-            | (_,Some _,_) -> EvalVarRef id
-            | _ -> error_not_evaluable (pr_id id)
-          with Not_found ->
-	    match r with
-	      | EvalConstRef _ -> r
-	      | _ -> Pretype_errors.error_var_not_found_loc loc id)
-      | ArgArg (r,None) -> r
-      | ArgVar (_,id) -> 
-          coerce_to_evaluable_ref env (unrec (List.assoc id ist.lfun))
+let interp_inductive ist = function
+  | ArgArg r -> r
+  | ArgVar (_,id) -> coerce_to_inductive (unrec (List.assoc id ist.lfun))
+
+let interp_evaluable ist env = function
+  | ArgArg (r,Some (loc,id)) ->
+      (* Maybe [id] has been introduced by Intro-like tactics *)
+      (try match Environ.lookup_named id env with
+        | (_,Some _,_) -> EvalVarRef id
+        | _ -> error_not_evaluable (pr_id id)
+      with Not_found ->
+	match r with
+	  | EvalConstRef _ -> r
+	  | _ -> Pretype_errors.error_var_not_found_loc loc id)
+  | ArgArg (r,None) -> r
+  | ArgVar (_,id) -> 
+      coerce_to_evaluable_ref env (unrec (List.assoc id ist.lfun))
 
 (* Interprets an hypothesis name *)
 let interp_hyp_location ist gl = function
@@ -1083,15 +1050,15 @@ let retype_list sigma env lst =
 
 let interp_casted_constr ocl ist sigma env (c,ce) =
   let (l1,l2) = constr_list ist env in
-  let rtype lst = retype_list sigma env lst in
+  let tl1 = retype_list sigma env l1 in
   let csr = 
     match ce with
     | None ->
-	Pretyping.understand_gen sigma env (rtype l1) (rtype ist.lmatch) ocl c
+	Pretyping.understand_gen sigma env tl1 ocl c
       (* If at toplevel (ce<>None), the error can be due to an incorrect
          context at globalization time: we retype with the now known
          intros/lettac/inversion hypothesis names *)
-    | Some c -> interp_constr_gen sigma env (l1,l2) ist.lmatch c ocl
+    | Some c -> interp_constr_gen sigma env (l1,l2) c ocl
   in
   db_constr ist.debug env csr;
   csr
@@ -1103,17 +1070,16 @@ let interp_constr ist sigma env c =
 let pf_interp_casted_openconstr ist gl (c,ce) =
   let sigma = project gl in
   let env = pf_env gl in
-  let (ltacvar,l) = constr_list ist env in
-  let rtype lst = retype_list sigma env lst in
+  let (ltacvars,l) = constr_list ist env in
+  let typs = retype_list sigma env ltacvars in
   let ocl = Some (pf_concl gl) in
   match ce with
   | None ->
-      Pretyping.understand_gen_tcc sigma env (rtype ltacvar) (rtype ist.lmatch)
-      ocl c
+      Pretyping.understand_gen_tcc sigma env typs ocl c
     (* If at toplevel (ce<>None), the error can be due to an incorrect
        context at globalization time: we retype with the now known
        intros/lettac/inversion hypothesis names *)
-  | Some c -> interp_openconstr_gen sigma env (ltacvar,l) ist.lmatch c ocl
+  | Some c -> interp_openconstr_gen sigma env (ltacvars,l) c ocl
 
 (* Interprets a constr expression *)
 let pf_interp_constr ist gl =
@@ -1125,11 +1091,10 @@ let pf_interp_casted_constr ist gl c =
 
 (* Interprets a reduction expression *)
 let interp_unfold ist env (l,qid) =
-  (l,interp_evaluable_or_metanum ist env qid)
+  (l,interp_evaluable ist env qid)
 
 let interp_flag ist env red =
-  { red
-    with rConst = List.map (interp_evaluable_or_metanum ist env) red.rConst }
+  { red with rConst = List.map (interp_evaluable ist env) red.rConst }
 
 let interp_pattern ist sigma env (l,c) = (l,interp_constr ist sigma env c)
 
@@ -1257,7 +1222,7 @@ and eval_tactic ist = function
 and interp_ltac_reference isapplied ist gl = function
   | ArgVar (loc,id) -> unrec (List.assoc id ist.lfun)
   | ArgArg (loc,r) ->
-      let v = val_interp {lfun=[];lmatch=[];debug=ist.debug} gl (lookup r) in
+      let v = val_interp {lfun=[];debug=ist.debug} gl (lookup r) in
       if isapplied then v else locate_tactic_call loc v
 
 and interp_tacarg ist gl = function
@@ -1280,7 +1245,6 @@ and interp_tacarg ist gl = function
         val_interp ist gl
           (intern_tactic {
             ltacvars = (List.map fst ist.lfun,[]); ltacrecvars = [];
-            metavars = List.map fst ist.lmatch;
             gsigma = project gl; genv = pf_env gl }
             (f ist))
       else if tg = "value" then
@@ -1403,8 +1367,7 @@ and match_context_interp ist g lr lmr =
       let lctxt = give_context ctxt id in
       if mhyps = [] then
 	let lgoal = List.map (fun (id,c) -> (id,VConstr c)) lgoal in
-        eval_with_fail {ist with lfun=lgoal@lctxt@ist.lfun; lmatch=ist.lmatch}
-          mt goal
+        eval_with_fail { ist with lfun=lgoal@lctxt@ist.lfun } mt goal
       else
         apply_hyps_context ist env goal mt lgoal mhyps hyps
     with
@@ -1488,8 +1451,7 @@ and apply_hyps_context ist env goal mt (lgmatch:(Rawterm.patvar * Term.constr) l
     | [] ->
 	let lmatch = List.map (fun (id,c) -> (id,VConstr c)) lmatch in
         db_mc_pattern_success ist.debug;
-        eval_with_fail {ist with lfun=lmatch@lfun@ist.lfun;
-          lmatch=ist.lmatch} mt goal
+        eval_with_fail {ist with lfun=lmatch@lfun@ist.lfun} mt goal
   in
   apply_hyps_context_rec [] lgmatch hyps (hyps,0) mhyps
 
@@ -1545,7 +1507,7 @@ and match_interp ist g constr lmr =
       let (lm,ctxt) = sub_match nocc c csr in
       let lctxt = give_context ctxt id in
       let lm = List.map (fun (id,c) -> (id,VConstr c)) lm in
-      val_interp {ist with lfun=lm@lctxt@ist.lfun; lmatch=ist.lmatch} g mt
+      val_interp {ist with lfun=lm@lctxt@ist.lfun} g mt
     with | NextOccurrence _ -> raise No_match
   in
   let rec apply_match ist csr = function
@@ -1646,15 +1608,15 @@ and interp_atomic ist gl = function
   | TacDecomposeAnd c -> Elim.h_decompose_and (pf_interp_constr ist gl c)
   | TacDecomposeOr c -> Elim.h_decompose_or (pf_interp_constr ist gl c)
   | TacDecompose (l,c) ->
-      let l = List.map (interp_inductive_or_metanum ist) l in
+      let l = List.map (interp_inductive ist) l in
       Elim.h_decompose l (pf_interp_constr ist gl c)
   | TacSpecialize (n,l) ->
       h_specialize n (interp_constr_with_bindings ist gl l)
   | TacLApply c -> h_lapply (pf_interp_constr ist gl c)
 
   (* Context management *)
-  | TacClear l -> h_clear (List.map (interp_hyp_or_metanum ist gl) l)
-  | TacClearBody l -> h_clear_body (List.map (interp_hyp_or_metanum ist gl) l)
+  | TacClear l -> h_clear (List.map (interp_hyp ist gl) l)
+  | TacClearBody l -> h_clear_body (List.map (interp_hyp ist gl) l)
   | TacMove (dep,id1,id2) ->
       h_move dep (interp_hyp ist gl id1) (interp_hyp ist gl id2)
   | TacRename (id1,id2) ->
@@ -1707,20 +1669,19 @@ and interp_atomic ist gl = function
     in tactic_of_value v gl
 
 (* Initial call for interpretation *)
-let interp_tac_gen lfun lmatch debug t gl = 
-  interp_tactic { lfun=lfun; lmatch=lmatch; debug=debug } 
+let interp_tac_gen lfun debug t gl = 
+  interp_tactic { lfun=lfun; debug=debug } 
     (intern_tactic {
       ltacvars = (List.map fst lfun, []); ltacrecvars = [];
-      metavars = List.map fst lmatch;
       gsigma = project gl; genv = pf_env gl } t) gl
 
-let eval_tactic t = interp_tactic { lfun=[]; lmatch=[]; debug=get_debug() } t
+let eval_tactic t = interp_tactic { lfun=[]; debug=get_debug() } t
 
-let interp t = interp_tac_gen [] [] (get_debug()) t
+let interp t = interp_tac_gen [] (get_debug()) t
 
 (* Hides interpretation for pretty-print *)
 let hide_interp t ot gl =
-  let ist = { ltacvars = ([],[]); ltacrecvars = []; metavars = [];
+  let ist = { ltacvars = ([],[]); ltacrecvars = []; 
             gsigma = project gl; genv = pf_env gl } in
   let te = intern_tactic ist t in
   let t = eval_tactic te in
@@ -1763,10 +1724,6 @@ let subst_and_short_name f (c,n) =
   assert (n=None); (* since tacdef are strictly globalized *)
   (f c,None)
 
-let subst_or_metanum f =  function
-  | AN x -> AN (f x)
-  | MetaNum (_loc,n) -> MetaNum (loc,n)
-
 let subst_or_var f =  function
   | ArgVar _ as x -> x
   | ArgArg (x) -> ArgArg (f x)
@@ -1779,8 +1736,7 @@ let subst_global_reference subst =
   subst_or_var (subst_located (subst_global subst))
 
 let subst_evaluable subst =
-  subst_or_metanum (subst_or_var
-    (subst_and_short_name (subst_evaluable_reference subst)))
+  subst_or_var (subst_and_short_name (subst_evaluable_reference subst))
 
 let subst_unfold subst (l,e) = 
   (l,subst_evaluable subst e)
@@ -1864,8 +1820,7 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
   | TacDecomposeAnd c -> TacDecomposeAnd (subst_rawconstr subst c)
   | TacDecomposeOr c -> TacDecomposeOr (subst_rawconstr subst c)
   | TacDecompose (l,c) ->
-      let l = 
-        List.map (subst_or_metanum (subst_or_var (subst_inductive subst))) l in
+      let l = List.map (subst_or_var (subst_inductive subst)) l in
       TacDecompose (l,subst_rawconstr subst c)
   | TacSpecialize (n,l) -> TacSpecialize (n,subst_raw_with_bindings subst l)
   | TacLApply c -> TacLApply (subst_rawconstr subst c)
@@ -2038,8 +1993,8 @@ let make_absolute_name (loc,id) =
   sp
 
 let make_empty_glob_sign () =
-  { ltacvars = ([],[]); ltacrecvars = [];
-    metavars = []; gsigma = Evd.empty; genv = Global.env() }
+  { ltacvars = ([],[]); ltacrecvars = []; 
+    gsigma = Evd.empty; genv = Global.env() }
 
 let add_tacdef isrec tacl =
   let isrec = if !Options.p1 then isrec else true in
@@ -2062,7 +2017,7 @@ let add_tacdef isrec tacl =
 let glob_tactic x = intern_tactic (make_empty_glob_sign ()) x
 
 let interp_redexp env evc r = 
-  let ist = { lfun=[]; lmatch=[]; debug=get_debug () } in
+  let ist = { lfun=[]; debug=get_debug () } in
   let gist = {(make_empty_glob_sign ()) with genv = env; gsigma = evc } in
   redexp_interp ist evc env (intern_redexp gist r)
 
@@ -2072,9 +2027,9 @@ let interp_redexp env evc r =
 let _ = Auto.set_extern_interp
   (fun l -> 
     let l = List.map (fun (id,c) -> (id,VConstr c)) l in
-    interp_tactic {lfun=l;lmatch=[];debug=get_debug()})
+    interp_tactic {lfun=l;debug=get_debug()})
 let _ = Auto.set_extern_intern_tac 
-  (fun l -> intern_tactic {(make_empty_glob_sign()) with metavars=l})
+  (fun l -> intern_tactic {(make_empty_glob_sign()) with ltacvars=(l,[])})
 let _ = Auto.set_extern_subst_tactic subst_tactic
 let _ = Dhyp.set_extern_interp eval_tactic
 let _ = Dhyp.set_extern_intern_tac
diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli
index ddd5175da4..9d8a7e57c4 100644
--- a/tactics/tacinterp.mli
+++ b/tactics/tacinterp.mli
@@ -36,7 +36,6 @@ type value =
 (* Signature for interpretation: val\_interp and interpretation functions *)
 and interp_sign =
   { lfun : (identifier * value) list;
-    lmatch : Pattern.patvar_map;
     debug : debug_info }
 
 (* Gives the identifier corresponding to an Identifier [tactic_arg] *)
@@ -70,7 +69,6 @@ val add_tacdef :
 type glob_sign = {
   ltacvars : identifier list * identifier list;
   ltacrecvars : (identifier * Nametab.ltac_constant) list;
-  metavars : Rawterm.patvar list;
   gsigma : Evd.evar_map;
   genv : Environ.env }
 
@@ -99,7 +97,7 @@ val interp_redexp : Environ.env -> Evd.evar_map -> raw_red_expr
   -> Tacred.red_expr
 
 (* Interprets tactic expressions *)
-val interp_tac_gen : (identifier * value) list -> Pattern.patvar_map ->
+val interp_tac_gen : (identifier * value) list -> 
                  debug_info -> raw_tactic_expr -> tactic
 
 (* Initial call for interpretation *)
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 43785836af..9be6eb3932 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -726,7 +726,7 @@ let add_notation_in_scope local df c (assoc,n,etyps,onlyparse) omodv8 sc toks =
     if onlyparse then None
     else
       let r = interp_rawconstr_gen
-          false Evd.empty (Global.env()) [] (Some []) (vars,[]) c in
+          false Evd.empty (Global.env()) [] false (vars,[]) c in
       Some (make_old_pp_rule ppn ppsymbols pptyps r notation scope vars) in
   (* Declare the interpretation *)
   let vars = List.map (fun id -> id,[] (* insert the right scope *)) vars in
@@ -802,7 +802,7 @@ let add_notation local df c modifiers mv8 sc =
 		let onlyparse = modifiers = [SetOnlyParsing] in
 		let a = interp_aconstr vars c in
 		let a_for_old = interp_rawconstr_gen
-		  false Evd.empty (Global.env()) [] (Some []) (vars,[]) c in
+		  false Evd.empty (Global.env()) [] false (vars,[]) c in
 		add_notation_interpretation_core local vars symbs df
 		  (a,a_for_old) sc onlyparse
 	  | Some n ->
diff --git a/translate/ppconstrnew.ml b/translate/ppconstrnew.ml
index a3b430c7d9..cd208fa09c 100644
--- a/translate/ppconstrnew.ml
+++ b/translate/ppconstrnew.ml
@@ -531,7 +531,7 @@ let transf_pattern env c =
   if Options.do_translate() then
     Constrextern.extern_rawconstr (Termops.vars_of_env env)
       (Constrintern.for_grammar
-	(Constrintern.interp_rawconstr_gen false Evd.empty env [] None ([],[]))
+	(Constrintern.interp_rawconstr_gen false Evd.empty env [] true ([],[]))
 	c)
   else c
 
diff --git a/translate/pptacticnew.ml b/translate/pptacticnew.ml
index 67d6638a07..0c4f571d7c 100644
--- a/translate/pptacticnew.ml
+++ b/translate/pptacticnew.ml
@@ -39,10 +39,6 @@ let pr_quantified_hypothesis = function
 
 let pr_quantified_hypothesis_arg h = spc () ++ pr_quantified_hypothesis h
 
-let pr_or_metanum pr = function
-  | AN x -> pr x
-  | MetaNum (_,n) -> Pattern.pr_patvar n
-
 (*
 let pr_binding prc = function
   | NamedHyp id, c -> hov 1 (pr_id id ++ str " := " ++ cut () ++ prc c)
@@ -296,7 +292,7 @@ and pr_atom1 env = function
   | TacDecompose (l,c) ->
       let vars = Termops.vars_of_env env in
       hov 1 (str "decompose" ++ spc () ++
-        hov 0 (str "[" ++ prlist_with_sep spc (pr_or_metanum (pr_ind vars)) l
+        hov 0 (str "[" ++ prlist_with_sep spc (pr_ind vars) l
 	  ++ str "]" ++ pr_lconstrarg env c))
   | TacSpecialize (n,c) ->
       hov 1 (str "specialize " ++ pr_opt int n ++ pr_with_bindings env c)
@@ -321,19 +317,19 @@ and pr_atom1 env = 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 env l)
@@ -502,7 +498,7 @@ let rec raw_printers =
      Ppconstrnew.pr_constr_env,
      Ppconstrnew.pr_lconstr_env,
      Ppconstrnew.pr_pattern,
-     pr_or_metanum pr_reference,
+     pr_reference,
      (fun _ -> pr_reference),
      pr_reference,
      pr_or_metaid (pr_located pr_id),
@@ -525,7 +521,7 @@ let rec glob_printers =
      (fun env -> pr_and_constr_expr (Ppconstrnew.pr_rawconstr_env env)),
      (fun env -> pr_and_constr_expr (Ppconstrnew.pr_lrawconstr_env env)),
      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),
      (fun vars -> pr_or_var (pr_inductive vars)),
      pr_or_var (pr_located pr_ltac_constant),
      pr_located pr_id,
diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml
index da4d7928a7..08ec0d87aa 100644
--- a/translate/ppvernacnew.ml
+++ b/translate/ppvernacnew.ml
@@ -508,7 +508,7 @@ let rec pr_vernac = function
         | None -> mt()
         | Some r ->
             str"Eval" ++ spc() ++
-            pr_red_expr (pr_constr, pr_lconstr, Pptactic.pr_or_metanum pr_reference) r ++
+            pr_red_expr (pr_constr, pr_lconstr, pr_reference) r ++
             str" in" ++ spc() in
       let pr_def_body = function
         | DefineBody (bl,red,c,d) ->
@@ -826,7 +826,7 @@ let rec pr_vernac = function
       let pr_mayeval r c = match r with 
       | Some r0 ->
           hov 2 (str"Eval" ++ spc() ++
-          pr_red_expr (pr_constr,pr_lconstr,Pptactic.pr_or_metanum pr_reference) r0 ++
+          pr_red_expr (pr_constr,pr_lconstr,pr_reference) r0 ++
           spc() ++ str"in" ++ spc () ++ pr_lconstr c)
       | None -> hov 2 (str"Check" ++ spc() ++ pr_lconstr c) 
       in pr_mayeval r c