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

2 files changed, 16 insertions, 5 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
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 4f94b904e3..04fbe21bb1 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -69,7 +69,7 @@ val import : compiled_env -> safe_environment -> safe_environment
 val env_of_safe_env : safe_environment -> env
 
 
-(*s Typing judgments without modifying the global safe env - used in minicoq *)
+(*s Typing judgments *)
 
 type judgment
 
@@ -78,3 +78,7 @@ val j_type : judgment -> constr
 
 val safe_infer : safe_environment -> constr -> judgment * constraints
 
+val typing : safe_environment -> constr -> judgment
+val typing_in_unsafe_env : env -> constr -> judgment
+
+