Canonisation de certains noms dans Pretyping, Asterm et Safe_typing

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

2 files changed, 13 insertions, 25 deletions

diff --git a/parsing/astterm.ml b/parsing/astterm.ml
index 3b881b516..853798dab 100644
--- a/parsing/astterm.ml
+++ b/parsing/astterm.ml
@@ -545,27 +545,21 @@ let _ =
 
 (* Endless^H^H^H^H^H^H^HShort list of alternative ways to call pretyping *)
 
-let interp_constr_gen is_ass sigma env com = 
-  let c = interp_rawconstr sigma env com in
-  try 
-    ise_resolve1 is_ass sigma env c
-  with e -> 
-    Stdpp.raise_with_loc (Ast.loc com) e
-
-let interp_constr sigma env c = interp_constr_gen false sigma env c
-let interp_type sigma env   c = interp_constr_gen true sigma env c
+let interp_constr sigma env c =
+  ise_resolve sigma env (interp_rawconstr sigma env c)
+let interp_type sigma env   c =
+  ise_resolve_type sigma env (interp_rawconstr sigma env c)
 let interp_sort = function
   | Node(loc,"PROP", []) -> Prop Null
   | Node(loc,"SET", [])  -> Prop Pos
   | Node(loc,"TYPE", []) -> Type Univ.dummy_univ
   | a -> user_err_loc (Ast.loc a,"interp_sort", [< 'sTR "Not a sort" >])
 
-let judgment_of_com sigma env com = 
-  let c = interp_rawconstr sigma env com in
-  try
-    ise_resolve false sigma [] env [] [] c
-  with e -> 
-    Stdpp.raise_with_loc (Ast.loc com) e
+let judgment_of_rawconstr sigma env c =
+  ise_infer sigma env (interp_rawconstr sigma env c)
+
+let type_judgment_of_rawconstr sigma env c =
+  ise_infer_type sigma env (interp_rawconstr sigma env c)
 
 (*To retype a list of key*constr with undefined key*)
 let retype_list sigma env lst=
@@ -583,13 +577,6 @@ let interp_constr1 sigma env lvar lmeta com =
   with e -> 
     Stdpp.raise_with_loc (Ast.loc com) e
 
-let typed_type_of_com sigma env com =
-  let c = interp_rawconstr sigma env com in
-  try 
-    ise_resolve_type true sigma [] env c
-  with e -> 
-    Stdpp.raise_with_loc (Ast.loc com) e
-
 (* Note: typ is retyped *)
 
 let interp_casted_constr sigma env com typ = 
diff --git a/parsing/astterm.mli b/parsing/astterm.mli
index 285f997ce..95810a36f 100644
--- a/parsing/astterm.mli
+++ b/parsing/astterm.mli
@@ -17,11 +17,12 @@ val interp_rawconstr     : 'a evar_map -> env -> Coqast.t -> rawconstr
 val interp_constr        : 'a evar_map -> env -> Coqast.t -> constr
 val interp_casted_constr : 'a evar_map -> env -> Coqast.t -> constr -> constr
 val interp_type          : 'a evar_map -> env -> Coqast.t -> constr
-val typed_type_of_com    : 'a evar_map -> env -> Coqast.t -> typed_type
-val judgment_of_com      : 'a evar_map -> env -> Coqast.t -> unsafe_judgment
-
 val interp_sort          : Coqast.t -> sorts
 
+val judgment_of_rawconstr : 'a evar_map -> env -> Coqast.t -> unsafe_judgment
+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     :