From c9f7a31ef67ce638ec591f9e5760941706bc12bc Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Fri, 21 Feb 2020 19:08:22 -0500
Subject: [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.
---
 vernac/declareDef.ml | 2 ++
 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 =
-- 
cgit v1.2.3