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

4 files changed, 33 insertions, 23 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
+
+
diff --git a/toplevel/command.ml b/toplevel/command.ml
index baf99646c1..dd8b9fb500 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -431,7 +431,9 @@ let start_proof_com sopt stre com =
 	next_ident_away (id_of_string "Unnamed_thm")
 	  (Pfedit.get_all_proof_names ())
   in
-  Pfedit.start_proof id stre sign (interp_type Evd.empty env com)
+  let c = interp_type Evd.empty env com in
+  let _ = Safe_typing.typing_in_unsafe_env env c in
+  Pfedit.start_proof id stre sign c
 
 let apply_tac_not_declare id pft = function
   | None -> error "Type of Let missing"
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index f5be089e73..fbe75eb9d4 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1005,23 +1005,20 @@ let _ =
 let _ =
   add "Check"
     (function 
-       | VARG_STRING kind :: VARG_CONSTR c :: g ->
-	   (match kind with
-	     | "PRINTTYPE" ->
-                 (fun () ->
-                   let evmap = Evd.empty in
-                   let env = Global.env() in
-                   let c = interp_constr evmap env c in
-                   let senv = Global.safe_env() in
-                   let (j, univ) = Safe_typing.safe_infer senv c in
-                   let _ = Safe_typing.add_constraints univ senv in
-                   mSG (print_safe_judgment env j))
-             | "CHECK" ->
-	         let (evmap, env) = get_current_context_of_args g in
-                 (fun () ->
-                   mSG (print_judgment env
-                         (judgment_of_rawconstr evmap env c)))
-             | _ -> anomaly "Unexpected string")
+       | VARG_STRING "PRINTTYPE" :: VARG_CONSTR c :: _ ->
+           (fun () ->
+              let evmap = Evd.empty in
+              let env = Global.env() in
+              let c = interp_constr evmap env c in
+              let senv = Global.safe_env() in
+              let j = Safe_typing.typing senv c in
+              mSG (print_safe_judgment env j))
+       | VARG_STRING "CHECK" :: VARG_CONSTR c :: g ->
+	   (fun () ->
+	      let (evmap, env) = get_current_context_of_args g in
+              let c = interp_constr evmap env c in
+              let j = Safe_typing.typing_in_unsafe_env env c in
+              mSG (print_safe_judgment env j))
        | _ -> bad_vernac_args "Check")
     
 (***