diff options
Diffstat (limited to 'toplevel/command.ml')
| -rw-r--r-- | toplevel/command.ml | 4 |
1 files changed, 3 insertions, 1 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" |