From d284deddaf736d2387a79b219f328915bc12614c Mon Sep 17 00:00:00 2001
From: gareuselesinge
Date: Thu, 25 Apr 2013 14:14:19 +0000
Subject: raise UnsafeSuccess -> feedback AddedAxiom

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16452 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/tactics.ml | 9 ++++++---
 1 file changed, 6 insertions(+), 3 deletions(-)

(limited to 'tactics')

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 2108009552..c531a34fab 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -3574,10 +3574,13 @@ let admit_as_an_axiom gl =
   (** ppedrot: seems legit to have admitted subproofs as local*)
   let con = Declare.declare_constant ~internal:Declare.KernelSilent ~local:true na decl in
   let axiom = constr_of_global (ConstRef con) in
-  exact_no_check
-    (applist (axiom,
+  let gl =
+    exact_no_check
+      (applist (axiom,
               List.rev (Array.to_list (instance_from_named_context sign))))
-    gl
+    gl in
+  Pp.feedback Interface.AddedAxiom;
+  gl
 
 let unify ?(state=full_transparent_state) x y gl =
   try
-- 
cgit v1.2.3