un typage sûr pour Goal et Check

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

1 files changed, 11 insertions, 4 deletions

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index f72712cc8e..d1ca1a52fa 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -166,12 +166,11 @@ let execute_type env constr =
   let (j,cst) = execute env constr in
   (type_judgment env Evd.empty j, cst)
 
+(* Renaming for the following. *)
 
-(* Exported machines. *)
+let safe_infer = execute
 
-let safe_infer env constr = execute env constr
-
-let safe_infer_type env constr = execute_type env constr
+let safe_infer_type = execute_type
 
 (* Typing of several terms. *)
 
@@ -471,3 +470,11 @@ let import = import
 
 let env_of_safe_env e = e
 
+(* Exported typing functions *)
+
+let typing env c = 
+  let (j,cst) = safe_infer env c in
+  let _ = add_constraints cst env in
+  j
+
+let typing_in_unsafe_env = typing