[save proof] Declare universe_binders unconditionally for mutual assumptions.

As suggested by Gaëtan in review, we move declaration of universe
binders to the common code in `DeclareDef`; this changes the semantics
for the assumption case when Recthms is not empty.

1 files changed, 2 insertions, 0 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