diff options
| author |  filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-04-20 12:07:01 +0000 |
|---|---|---|
| committer | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-04-20 12:07:01 +0000 |
| commit | 7ee76fc83bfdec43eca9b9f9c57ea32c64914f3a (patch) | |
| tree | 51c3163a110e866f2ecc67136aa9a415c1304b50 /toplevel/command.ml | |
| parent | 38d5db3b7502c5a3e18290938422a7bc58aacc5a (diff) | |
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
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 baf99646c..dd8b9fb50 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" |