diff options
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/command.ml | 4 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 31 |
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") (*** |