Conséquences nettoyage pretyping.ml

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

2 files changed, 10 insertions, 14 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 89d4e57ae..b2b657c5f 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1102,8 +1102,10 @@ let interp_constr sigma env c =
 let interp_openconstr 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)
+*)
 
 let interp_type sigma env c =
   understand_type sigma env (interp_rawtype sigma env c)
@@ -1129,11 +1131,8 @@ let retype_list sigma env lst =
 
 (*  List.map (fun (x,csr) -> (x,Retyping.get_judgment_of env sigma csr)) lst*)
 
-type ltac_sign = 
-  identifier list * (identifier * identifier option) list
-
-type ltac_env = 
-  (identifier * Term.constr) list * (identifier * identifier option) list
+type ltac_sign = identifier list * unbound_ltac_var_map
+type ltac_env = (identifier * Term.constr) list * unbound_ltac_var_map
 
 (* Interprets a constr according to two lists *)
 (* of instantiations (variables and metas)    *)
@@ -1142,7 +1141,7 @@ 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
+  understand_gen_ltac sigma env (typs,[]) exptyp c
 
 (*Interprets a casted constr according to two lists of instantiations
   (variables and metas)*)
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 03ad950c7..757f02a46 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -20,6 +20,7 @@ open Pattern
 open Coqast
 open Topconstr
 open Termops
+open Pretyping
 (*i*)
 
 (*s Translation from front abstract syntax of term to untyped terms (rawconstr)
@@ -41,11 +42,8 @@ type var_internalisation_data =
 type implicits_env = (identifier * var_internalisation_data) list
 type full_implicits_env = identifier list * implicits_env
 
-type ltac_sign = 
-  identifier list * (identifier * identifier option) list
-
-type ltac_env = 
-  (identifier * constr) list * (identifier * identifier option) list
+type ltac_sign = identifier list * unbound_ltac_var_map
+type ltac_env = (identifier * constr) list * unbound_ltac_var_map
 
 (* Interprets global names, including syntactic defs and section variables *)
 val interp_rawconstr     : evar_map -> env -> constr_expr -> rawconstr
@@ -58,8 +56,6 @@ val interp_casted_constr : evar_map -> env -> constr_expr -> types -> constr
 val interp_type          : evar_map -> env -> constr_expr -> types
 val interp_binder        : evar_map -> env -> name -> constr_expr -> types
 val interp_openconstr    : evar_map -> env -> constr_expr -> evar_map * constr
-val interp_casted_openconstr    :
-  evar_map -> env -> constr_expr -> constr -> evar_map * constr
 
 (* [interp_type_with_implicits] extends [interp_type] by allowing
    implicits arguments in the ``rel'' part of [env]; the extra
@@ -83,7 +79,8 @@ 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 -> constr_expr -> constr option -> constr
+  evar_map -> env -> ltac_env -> constr_expr -> constr option ->
+    evar_defs * constr
 
 (* Interprets a constr according to two lists of instantiations (variables and
   metas), possibly casting it, and turning unresolved evar into metas*)