diff options
Diffstat (limited to 'vernac/lemmas.ml')
| -rw-r--r-- | vernac/lemmas.ml | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 6a754a0cde..adfb058942 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -336,8 +336,7 @@ let finish_admitted env sigma ~name ~poly ~scope pe ctx hook ~udecl impargs othe let () = Declare.assumption_message name in Declare.declare_univ_binders (GlobRef.ConstRef kn) (UState.universe_binders ctx); (* This takes care of the implicits and hook for the current constant*) - process_recthms ?fix_exn:None ?hook env sigma ctx ~udecl ~poly ~scope:(Global local) (GlobRef.ConstRef kn) impargs other_thms; - Feedback.feedback Feedback.AddedAxiom + process_recthms ?fix_exn:None ?hook env sigma ctx ~udecl ~poly ~scope:(Global local) (GlobRef.ConstRef kn) impargs other_thms let save_lemma_admitted ~(lemma : t) : unit = (* Used for printing in recthms *) |