Reorganisation des interp_constr

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

1 files changed, 10 insertions, 9 deletions

diff --git a/parsing/astterm.ml b/parsing/astterm.ml
index 080fd7b21..bdd818b6a 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)