diff options
| author |  gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-04-25 14:14:19 +0000 |
|---|---|---|
| committer | gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-04-25 14:14:19 +0000 |
| commit | d284deddaf736d2387a79b219f328915bc12614c (patch) | |
| tree | c335d0d3de81f75bdb93b5cf6b2a033d51b6475a /tactics | |
| parent | db7b19f0f1d6b18bcc62fbedccad7a56f72315f2 (diff) | |
raise UnsafeSuccess -> feedback AddedAxiom
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16452 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/tactics.ml | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 210800955..c531a34fa 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 |