diff options
| -rw-r--r-- | vernac/declareDef.ml | 2 | ||||
| -rw-r--r-- | vernac/lemmas.ml | 3 |
2 files changed, 2 insertions, 3 deletions
diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml index ba4b42c4e0..bd857a6e38 100644 --- a/vernac/declareDef.ml +++ b/vernac/declareDef.ml @@ -87,6 +87,8 @@ let declare_assumption ?fix_exn ~name ~scope ~hook ~impargs ~uctx pe = let kn = Declare.declare_constant ~name ~local ~kind decl in let dref = Names.GlobRef.ConstRef kn in let () = Impargs.maybe_declare_manual_implicits false dref impargs in + let () = Declare.assumption_message name in + let () = DeclareUniv.declare_univ_binders dref (UState.universe_binders uctx) in let () = Hook.(call ?fix_exn ?hook { S.uctx; obls = []; scope; dref}) in dref diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 1d3132d525..5eacd7aca7 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -255,9 +255,6 @@ let compute_proof_using_for_admitted proof typ pproofs = let finish_admitted ~name ~poly ~scope pe uctx hook ~udecl impargs other_thms = let dref = DeclareDef.declare_assumption ~name ~scope ~hook ~uctx ~impargs pe in - (* Should both of those be done in declare_axiom? *) - let () = Declare.assumption_message name in - DeclareUniv.declare_univ_binders dref (UState.universe_binders uctx); process_recthms ?fix_exn:None ?hook uctx ~udecl ~poly ~scope dref other_thms let save_lemma_admitted ~(lemma : t) : unit = |