Reorganisation des interp_constr

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

2 files changed, 18 insertions, 16 deletions

diff --git a/parsing/astterm.ml b/parsing/astterm.ml
index 080fd7b21c..bdd818b6a9 100644
--- a/parsing/astterm.ml
+++ b/parsing/astterm.ml
@@ -554,24 +554,25 @@ let type_judgment_of_rawconstr sigma env c =
 let retype_list sigma env lst=
   List.map (fun (x,csr) -> (x,Retyping.get_judgment_of env sigma csr)) lst;;
 
+(*Interprets a constr according to two lists of instantiations (variables and
+  metas)*)
 (* Note: typ is retyped *)
-
-let interp_casted_gen_constr1 sigma env lvar lmeta exptyp com =
+let interp_constr_gen sigma env lvar lmeta com exptyp =
   let c =
     interp_rawconstr_gen sigma env false (List.map (fun x -> string_of_id (fst
       x)) lvar) com
   and rtype=fun lst -> retype_list sigma env lst in
   understand_gen sigma env (rtype lvar) (rtype lmeta) exptyp c;;
 
-(*Interprets a constr according to two lists of instantiations (variables and
-  metas)*)
-let interp_constr1 sigma env lvar lmeta com =
-  interp_casted_gen_constr1 sigma env lvar lmeta None com
-
 (*Interprets a casted constr according to two lists of instantiations
   (variables and metas)*)
-let interp_casted_constr1 sigma env lvar lmeta com typ =
-  interp_casted_gen_constr1 sigma env lvar lmeta (Some typ) com
+let interp_openconstr_gen sigma env lvar lmeta com exptyp =
+  let c =
+    interp_rawconstr_gen sigma env false (List.map (fun x -> string_of_id (fst
+      x)) lvar) com
+  and rtype=fun lst -> retype_list sigma env lst in
+  understand_gen_tcc sigma env (rtype lvar) (rtype lmeta) exptyp c;;
+
 
 let interp_casted_constr sigma env com typ = 
   understand_gen sigma env [] [] (Some typ) (interp_rawconstr sigma env com)
diff --git a/parsing/astterm.mli b/parsing/astterm.mli
index 3274cf6f4f..fdb930c999 100644
--- a/parsing/astterm.mli
+++ b/parsing/astterm.mli
@@ -29,16 +29,17 @@ val type_judgment_of_rawconstr :
   'a evar_map -> env -> Coqast.t -> unsafe_type_judgment
 
 (*Interprets a constr according to two lists of instantiations (variables and
-  metas)*)
-val interp_constr1     :
+  metas), possibly casting it*)
+val interp_constr_gen     :
   'a evar_map -> env -> (identifier * constr) list ->
-    (int * constr) list -> Coqast.t -> constr
+    (int * constr) list -> Coqast.t -> constr option -> constr
 
-(*Interprets a casted constr according to two lists of instantiations
-  (variables and metas)*)
-val interp_casted_constr1 :
+(*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     :
   'a evar_map -> env -> (identifier * constr) list ->
-    (int * constr) list -> Coqast.t -> constr -> constr
+    (int * constr) list -> Coqast.t -> constr option
+      -> (int * constr) list * constr
 
 (*Interprets constr patterns according to a list of instantiations
   (variables)*)