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

4 files changed, 29 insertions, 34 deletions

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 *)