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, 17 insertions, 18 deletions

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")
     
 (***