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

1 files changed, 9 insertions, 22 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 =