diff options
| author |  ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-08-28 07:44:17 +0000 |
|---|---|---|
| committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-08-28 07:44:17 +0000 |
| commit | 12dce194c9b0825971d75c76e5fa944edf5b6e38 (patch) | |
| tree | 48a89d8c1ed43d55d85719479185782136107561 | |
| parent | 90a73b08da2fe80b0298997f1f9adb65afdfbf54 (diff) | |
Fixing bug #3083.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16739 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | toplevel/lemmas.ml | 10 |
1 files changed, 8 insertions, 2 deletions
diff --git a/toplevel/lemmas.ml b/toplevel/lemmas.ml index 846714db7..3267e9497 100644 --- a/toplevel/lemmas.ml +++ b/toplevel/lemmas.ml @@ -366,8 +366,14 @@ let admit () = let (id,k,typ,hook) = Pfedit.current_proof_statement () in let e = Pfedit.get_used_variables(), typ, None in let kn = declare_constant id (ParameterEntry e,IsAssumption Conjectural) in - Pfedit.delete_current_proof (); - assumption_message id; + let () = Pfedit.delete_current_proof () in + let () = match fst k with + | Global -> () + | Local | Discharge -> + msg_warning (str "Let definition" ++ spc () ++ pr_id id ++ spc () ++ + str "declared as an axiom.") + in + let () = assumption_message id in Option.iter (fun f -> f Global (ConstRef kn)) hook (* Miscellaneous *) |