From 12dce194c9b0825971d75c76e5fa944edf5b6e38 Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Wed, 28 Aug 2013 07:44:17 +0000
Subject: Fixing bug #3083.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16739 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 toplevel/lemmas.ml | 10 ++++++++--
 1 file changed, 8 insertions(+), 2 deletions(-)

diff --git a/toplevel/lemmas.ml b/toplevel/lemmas.ml
index 846714db7a..3267e9497c 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 *)
-- 
cgit v1.2.3