From 946c6c7e58a1dfbe57445a0a1508a587193bb7c3 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Fri, 22 May 2020 03:55:40 +0200
Subject: [declare] Simplify exported type of definition_entry

This reduces the amount of exported internals, in particular
w.r.t. proof delaying and side effects which we will need in future
refactorings.

Actually turning the type from `Evd.side_effects proof_entry` to `unit
proof_entry` is left for the next commits.
---
 vernac/declare.ml  | 11 ++++++++---
 vernac/declare.mli |  9 +--------
 2 files changed, 9 insertions(+), 11 deletions(-)

diff --git a/vernac/declare.ml b/vernac/declare.ml
index c77d4909da..7394f7f9c2 100644
--- a/vernac/declare.ml
+++ b/vernac/declare.ml
@@ -138,7 +138,9 @@ type 'a proof_entry = {
 
 let default_univ_entry = Entries.Monomorphic_entry Univ.ContextSet.empty
 
-let definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?feedback_id ?section_vars ?types
+(** [univsbody] are universe-constraints attached to the body-only,
+   used in vio-delayed opaque constants and private poly universes *)
+let definition_entry_core ?fix_exn ?(opaque=false) ?(inline=false) ?feedback_id ?section_vars ?types
     ?(univs=default_univ_entry) ?(eff=Evd.empty_side_effects) ?(univsbody=Univ.ContextSet.empty) body =
   { proof_entry_body = Future.from_val ?fix_exn ((body,univsbody), eff);
     proof_entry_secctx = section_vars;
@@ -148,6 +150,9 @@ let definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?feedback_id ?sect
     proof_entry_feedback = feedback_id;
     proof_entry_inline_code = inline}
 
+let definition_entry =
+  definition_entry_core ?fix_exn:None ?eff:None ?univsbody:None ?feedback_id:None ?section_vars:None
+
 type proof_object =
   { name : Names.Id.t
   (* [name] only used in the STM *)
@@ -241,7 +246,7 @@ let close_proof ~opaque ~keep_body_ucst_separate ps =
         let utyp = UState.check_univ_decl ~poly ctx udecl in
         utyp, Univ.ContextSet.empty
     in
-    definition_entry ~opaque ?section_vars ~univs:utyp ~univsbody:ubody ~types:typ ~eff body
+    definition_entry_core ~opaque ?section_vars ~univs:utyp ~univsbody:ubody ~types:typ ~eff body
   in
   let entries = CList.map make_entry elist  in
   { name; entries; uctx }
@@ -998,7 +1003,7 @@ let prepare_definition ?opaque ?inline ?fix_exn ~poly ~udecl ~types ~body sigma
       sigma (fun nf -> nf body, Option.map nf types)
   in
   let univs = Evd.check_univ_decl ~poly sigma udecl in
-  let entry = definition_entry ?fix_exn ?opaque ?inline ?types ~univs body in
+  let entry = definition_entry_core ?fix_exn ?opaque ?inline ?types ~univs body in
   let uctx = Evd.evar_universe_context sigma in
   entry, uctx
 
diff --git a/vernac/declare.mli b/vernac/declare.mli
index 647896e2f5..b380afc97d 100644
--- a/vernac/declare.mli
+++ b/vernac/declare.mli
@@ -144,17 +144,10 @@ val declare_variable
    for removal from the public API, use higher-level declare APIs
    instead *)
 val definition_entry
-  : ?fix_exn:Future.fix_exn
-  -> ?opaque:bool
+  :  ?opaque:bool
   -> ?inline:bool
-  -> ?feedback_id:Stateid.t
-  -> ?section_vars:Id.Set.t
   -> ?types:types
   -> ?univs:Entries.universes_entry
-  -> ?eff:Evd.side_effects
-  -> ?univsbody:Univ.ContextSet.t
-  (** Universe-constraints attached to the body-only, used in
-     vio-delayed opaque constants and private poly universes *)
   -> constr
   -> Evd.side_effects proof_entry
 
-- 
cgit v1.2.3


From 09891acd9bfc80c7dc13f5fefb8906ce5d2d4d1d Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Fri, 22 May 2020 03:13:09 +0200
Subject: [declare] Don't expose internal parameter obls

---
 vernac/declare.ml  | 14 +++++++++-----
 vernac/declare.mli |  2 --
 2 files changed, 9 insertions(+), 7 deletions(-)

diff --git a/vernac/declare.ml b/vernac/declare.ml
index 7394f7f9c2..0c98ac9070 100644
--- a/vernac/declare.ml
+++ b/vernac/declare.ml
@@ -894,7 +894,7 @@ module Hook = struct
 end
 
 (* Locality stuff *)
-let declare_entry ~name ~scope ~kind ?hook ?(obls=[]) ~impargs ~uctx entry =
+let declare_entry_core ~name ~scope ~kind ?hook ~obls ~impargs ~uctx entry =
   let should_suggest = entry.proof_entry_opaque &&
                        Option.is_empty entry.proof_entry_secctx in
   let ubind = UState.universe_binders uctx in
@@ -915,6 +915,8 @@ let declare_entry ~name ~scope ~kind ?hook ?(obls=[]) ~impargs ~uctx entry =
   Option.iter (fun hook -> Hook.call ~hook { Hook.S.uctx; obls; scope; dref }) hook;
   dref
 
+let declare_entry = declare_entry_core ~obls:[]
+
 let mutual_make_bodies ~fixitems ~rec_declaration ~possible_indexes =
   match possible_indexes with
   | Some possible_indexes ->
@@ -1007,10 +1009,12 @@ let prepare_definition ?opaque ?inline ?fix_exn ~poly ~udecl ~types ~body sigma
   let uctx = Evd.evar_universe_context sigma in
   entry, uctx
 
-let declare_definition ~name ~scope ~kind ~opaque ~impargs ~udecl ?hook
-    ?obls ~poly ?inline ~types ~body ?fix_exn sigma =
+let declare_definition_core ~name ~scope ~kind ~opaque ~impargs ~udecl ?hook
+    ~obls ~poly ?inline ~types ~body ?fix_exn sigma =
   let entry, uctx = prepare_definition ?fix_exn ~opaque ~poly ~udecl ~types ~body ?inline sigma in
-  declare_entry ~name ~scope ~kind ~impargs ?obls ?hook ~uctx entry
+  declare_entry_core ~name ~scope ~kind ~impargs ~obls ?hook ~uctx entry
+
+let declare_definition = declare_definition_core ~obls:[]
 
 let prepare_obligation ~name ~types ~body sigma =
   let env = Global.env () in
@@ -1450,7 +1454,7 @@ let declare_definition prg =
   let obls = List.map (fun (id, (_, c)) -> (id, c)) varsubst in
   (* XXX: This is doing normalization twice *)
   let kn =
-    declare_definition ~name ~scope ~kind ~impargs ?hook ~obls
+    declare_definition_core ~name ~scope ~kind ~impargs ?hook ~obls
       ~fix_exn ~opaque ~poly ~udecl ~types ~body sigma
   in
   let pm = progmap_remove !State.prg_ref prg in
diff --git a/vernac/declare.mli b/vernac/declare.mli
index b380afc97d..4e2ba1833f 100644
--- a/vernac/declare.mli
+++ b/vernac/declare.mli
@@ -288,7 +288,6 @@ val declare_entry
   -> scope:locality
   -> kind:Decls.logical_kind
   -> ?hook:Hook.t
-  -> ?obls:(Id.t * Constr.t) list
   -> impargs:Impargs.manual_implicits
   -> uctx:UState.t
   -> Evd.side_effects proof_entry
@@ -308,7 +307,6 @@ val declare_definition
   -> impargs:Impargs.manual_implicits
   -> udecl:UState.universe_decl
   -> ?hook:Hook.t
-  -> ?obls:(Id.t * Constr.t) list
   -> poly:bool
   -> ?inline:bool
   -> types:EConstr.t option
-- 
cgit v1.2.3


From baef9828c3e6ea11fce2e172797f0f67e51885ad Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Fri, 22 May 2020 02:52:36 +0200
Subject: [nit] Remove unused exported error message in obligations

---
 vernac/obligations.mli | 1 -
 1 file changed, 1 deletion(-)

diff --git a/vernac/obligations.mli b/vernac/obligations.mli
index 102a17b216..c21951373b 100644
--- a/vernac/obligations.mli
+++ b/vernac/obligations.mli
@@ -132,5 +132,4 @@ val show_obligations : ?msg:bool -> Names.Id.t option -> unit
 val show_term : Names.Id.t option -> Pp.t
 val admit_obligations : Names.Id.t option -> unit
 
-val explain_no_obligations : Names.Id.t option -> Pp.t
 val check_program_libraries : unit -> unit
-- 
cgit v1.2.3


From d9d4dcb41d8a63b7d535200b68bcbef4a38993df Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Fri, 22 May 2020 03:34:03 +0200
Subject: [declare] Turn restrict_ucontext hack into an internal parameter

This is not needed outside of `Declare` now.
---
 vernac/comFixpoint.ml | 2 +-
 vernac/declare.ml     | 6 ++++--
 vernac/declare.mli    | 3 ---
 3 files changed, 5 insertions(+), 6 deletions(-)

diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index 80ca85e9a6..0b75e7f410 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -285,7 +285,7 @@ let declare_fixpoint_generic ?indexes ~scope ~poly ((fixnames,fixrs,fixdefs,fixt
   let fix_kind = Decls.IsDefinition fix_kind in
   let _ : GlobRef.t list =
     Declare.declare_mutually_recursive ~scope ~opaque:false ~kind:fix_kind ~poly ~uctx
-      ~possible_indexes:indexes ~restrict_ucontext:true ~udecl ~ntns ~rec_declaration
+      ~possible_indexes:indexes ~udecl ~ntns ~rec_declaration
       fixitems
   in
   ()
diff --git a/vernac/declare.ml b/vernac/declare.ml
index 0c98ac9070..65f0265b3e 100644
--- a/vernac/declare.ml
+++ b/vernac/declare.ml
@@ -943,7 +943,7 @@ module Recthm = struct
     }
 end
 
-let declare_mutually_recursive ~opaque ~scope ~kind ~poly ~uctx ~udecl ~ntns ~rec_declaration ~possible_indexes ?(restrict_ucontext=true) fixitems =
+let declare_mutually_recursive_core ~opaque ~scope ~kind ~poly ~uctx ~udecl ~ntns ~rec_declaration ~possible_indexes ?(restrict_ucontext=true) fixitems =
   let vars, fixdecls, indexes =
     mutual_make_bodies ~fixitems ~rec_declaration ~possible_indexes in
   let uctx, univs =
@@ -969,6 +969,8 @@ let declare_mutually_recursive ~opaque ~scope ~kind ~poly ~uctx ~udecl ~ntns ~re
   List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns;
   csts
 
+let declare_mutually_recursive = declare_mutually_recursive_core ~restrict_ucontext:true
+
 let warn_let_as_axiom =
   CWarnings.create ~name:"let-as-axiom" ~category:"vernacular"
     Pp.(fun id -> strbrk "Let definition" ++ spc () ++ Names.Id.print id ++
@@ -1540,7 +1542,7 @@ let declare_mutual_definition l =
   (* Declare the recursive definitions *)
   let udecl = UState.default_univ_decl in
   let kns =
-    declare_mutually_recursive ~scope ~opaque ~kind ~udecl ~ntns
+    declare_mutually_recursive_core ~scope ~opaque ~kind ~udecl ~ntns
       ~uctx:first.prg_ctx ~rec_declaration ~possible_indexes ~poly
       ~restrict_ucontext:false fixitems
   in
diff --git a/vernac/declare.mli b/vernac/declare.mli
index 4e2ba1833f..5339f4702b 100644
--- a/vernac/declare.mli
+++ b/vernac/declare.mli
@@ -350,9 +350,6 @@ val declare_mutually_recursive
   -> ntns:Vernacexpr.decl_notation list
   -> rec_declaration:Constr.rec_declaration
   -> possible_indexes:lemma_possible_guards option
-  -> ?restrict_ucontext:bool
-  (** XXX: restrict_ucontext should be always true, this seems like a
-     bug in obligations, so this parameter should go away *)
   -> Recthm.t list
   -> Names.GlobRef.t list
 
-- 
cgit v1.2.3


From e1a3216700427853bd5fba36e84da78b46b6cea0 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Fri, 22 May 2020 03:36:36 +0200
Subject: [declare] Nit on errors.

---
 vernac/declare.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/vernac/declare.ml b/vernac/declare.ml
index 65f0265b3e..5be819e109 100644
--- a/vernac/declare.ml
+++ b/vernac/declare.ml
@@ -1266,8 +1266,8 @@ let not_transp_msg =
     ++ spc ()
     ++ str "Use 'Defined' instead.")
 
-let pperror cmd = CErrors.user_err ~hdr:"Program" cmd
-let err_not_transp () = pperror not_transp_msg
+let err_not_transp () =
+  CErrors.user_err ~hdr:"Program" not_transp_msg
 
 module ProgMap = Id.Map
 
-- 
cgit v1.2.3


From 3b3836466c795265778424c05fe75a507149a8c0 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 25 May 2020 01:07:05 +0200
Subject: [declare] Factor out universe computation in close_proof

A step towards enforcing some more static invariants.
---
 vernac/declare.ml | 67 ++++++++++++++++++++++++++++---------------------------
 1 file changed, 34 insertions(+), 33 deletions(-)

diff --git a/vernac/declare.ml b/vernac/declare.ml
index 5be819e109..35ecb614b9 100644
--- a/vernac/declare.ml
+++ b/vernac/declare.ml
@@ -199,6 +199,39 @@ let prepare_proof ~unsafe_typ { proof } =
   let proofs = List.map (fun (body, typ) -> (to_constr_body body, eff), to_constr_typ typ) initial_goals in
   proofs, Evd.evar_universe_context evd
 
+let make_univs ~poly ~initial_euctx ~uctx ~opaque ~udecl ~allow_deferred typ body =
+
+  let used_univs_body = Vars.universes_of_constr body in
+  let used_univs_typ = Vars.universes_of_constr typ in
+  let used_univs = Univ.LSet.union used_univs_body used_univs_typ in
+  if allow_deferred then
+    let utyp = UState.univ_entry ~poly initial_euctx in
+    let uctx = UState.constrain_variables (fst (UState.context_set initial_euctx)) uctx in
+    (* For vi2vo compilation proofs are computed now but we need to
+       complement the univ constraints of the typ with the ones of
+       the body.  So we keep the two sets distinct. *)
+    let uctx_body = UState.restrict uctx used_univs in
+    let ubody = UState.check_mono_univ_decl uctx_body udecl in
+    utyp, ubody
+  else if poly && opaque && private_poly_univs () then
+    let universes = UState.restrict uctx used_univs in
+    let typus = UState.restrict universes used_univs_typ in
+    let utyp = UState.check_univ_decl ~poly typus udecl in
+    let ubody = Univ.ContextSet.diff
+        (UState.context_set universes)
+        (UState.context_set typus)
+    in
+    utyp, ubody
+  else
+    (* Since the proof is computed now, we can simply have 1 set of
+       constraints in which we merge the ones for the body and the ones
+       for the typ. We recheck the declaration after restricting with
+       the actually used universes.
+       TODO: check if restrict is really necessary now. *)
+    let ctx = UState.restrict uctx used_univs in
+    let utyp = UState.check_univ_decl ~poly ctx udecl in
+    utyp, Univ.ContextSet.empty
+
 let close_proof ~opaque ~keep_body_ucst_separate ps =
 
   let { section_vars; proof; udecl; initial_euctx } = ps in
@@ -208,44 +241,12 @@ let close_proof ~opaque ~keep_body_ucst_separate ps =
   let opaque = match opaque with Opaque -> true | Transparent -> false in
 
   let make_entry ((body, eff), typ) =
-
     let allow_deferred =
       not poly &&
       (keep_body_ucst_separate
        || not (Safe_typing.is_empty_private_constants eff.Evd.seff_private))
     in
-    let used_univs_body = Vars.universes_of_constr body in
-    let used_univs_typ = Vars.universes_of_constr typ in
-    let used_univs = Univ.LSet.union used_univs_body used_univs_typ in
-    let utyp, ubody =
-      if allow_deferred then
-        let utyp = UState.univ_entry ~poly initial_euctx in
-        let uctx = UState.constrain_variables (fst (UState.context_set initial_euctx)) uctx in
-        (* For vi2vo compilation proofs are computed now but we need to
-           complement the univ constraints of the typ with the ones of
-           the body.  So we keep the two sets distinct. *)
-        let uctx_body = UState.restrict uctx used_univs in
-        let ubody = UState.check_mono_univ_decl uctx_body udecl in
-        utyp, ubody
-      else if poly && opaque && private_poly_univs () then
-        let universes = UState.restrict uctx used_univs in
-        let typus = UState.restrict universes used_univs_typ in
-        let utyp = UState.check_univ_decl ~poly typus udecl in
-        let ubody = Univ.ContextSet.diff
-            (UState.context_set universes)
-            (UState.context_set typus)
-        in
-        utyp, ubody
-      else
-        (* Since the proof is computed now, we can simply have 1 set of
-           constraints in which we merge the ones for the body and the ones
-           for the typ. We recheck the declaration after restricting with
-           the actually used universes.
-           TODO: check if restrict is really necessary now. *)
-        let ctx = UState.restrict uctx used_univs in
-        let utyp = UState.check_univ_decl ~poly ctx udecl in
-        utyp, Univ.ContextSet.empty
-    in
+    let utyp, ubody = make_univs ~initial_euctx ~poly ~opaque ~uctx ~allow_deferred ~udecl typ body in
     definition_entry_core ~opaque ?section_vars ~univs:utyp ~univsbody:ubody ~types:typ ~eff body
   in
   let entries = CList.map make_entry elist  in
-- 
cgit v1.2.3


From 7661029ab7611bd96128b5ab5f788c18c203a7ff Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 25 May 2020 01:24:07 +0200
Subject: [declare] Split univs_deferred in close_proof

A step towards enforcing some more static invariants.
---
 vernac/declare.ml | 38 ++++++++++++++++++++++----------------
 1 file changed, 22 insertions(+), 16 deletions(-)

diff --git a/vernac/declare.ml b/vernac/declare.ml
index 35ecb614b9..514ab52935 100644
--- a/vernac/declare.ml
+++ b/vernac/declare.ml
@@ -199,21 +199,25 @@ let prepare_proof ~unsafe_typ { proof } =
   let proofs = List.map (fun (body, typ) -> (to_constr_body body, eff), to_constr_typ typ) initial_goals in
   proofs, Evd.evar_universe_context evd
 
-let make_univs ~poly ~initial_euctx ~uctx ~opaque ~udecl ~allow_deferred typ body =
+let make_univs_deferred ~poly ~initial_euctx ~uctx ~udecl typ body =
+  let used_univs_body = Vars.universes_of_constr body in
+  let used_univs_typ = Vars.universes_of_constr typ in
+  let used_univs = Univ.LSet.union used_univs_body used_univs_typ in
+  let utyp = UState.univ_entry ~poly initial_euctx in
+  let uctx = UState.constrain_variables (fst (UState.context_set initial_euctx)) uctx in
+  (* For vi2vo compilation proofs are computed now but we need to
+     complement the univ constraints of the typ with the ones of
+     the body.  So we keep the two sets distinct. *)
+  let uctx_body = UState.restrict uctx used_univs in
+  let ubody = UState.check_mono_univ_decl uctx_body udecl in
+  utyp, ubody
+
+let make_univs ~poly ~uctx ~opaque ~udecl typ body =
 
   let used_univs_body = Vars.universes_of_constr body in
   let used_univs_typ = Vars.universes_of_constr typ in
   let used_univs = Univ.LSet.union used_univs_body used_univs_typ in
-  if allow_deferred then
-    let utyp = UState.univ_entry ~poly initial_euctx in
-    let uctx = UState.constrain_variables (fst (UState.context_set initial_euctx)) uctx in
-    (* For vi2vo compilation proofs are computed now but we need to
-       complement the univ constraints of the typ with the ones of
-       the body.  So we keep the two sets distinct. *)
-    let uctx_body = UState.restrict uctx used_univs in
-    let ubody = UState.check_mono_univ_decl uctx_body udecl in
-    utyp, ubody
-  else if poly && opaque && private_poly_univs () then
+  if poly && opaque && private_poly_univs () then
     let universes = UState.restrict uctx used_univs in
     let typus = UState.restrict universes used_univs_typ in
     let utyp = UState.check_univ_decl ~poly typus udecl in
@@ -241,12 +245,14 @@ let close_proof ~opaque ~keep_body_ucst_separate ps =
   let opaque = match opaque with Opaque -> true | Transparent -> false in
 
   let make_entry ((body, eff), typ) =
-    let allow_deferred =
-      not poly &&
-      (keep_body_ucst_separate
-       || not (Safe_typing.is_empty_private_constants eff.Evd.seff_private))
+    (* allow_deferred case *)
+    let utyp, ubody =
+      if not poly &&
+         (keep_body_ucst_separate
+          || not (Safe_typing.is_empty_private_constants eff.Evd.seff_private))
+      then make_univs_deferred ~initial_euctx ~poly ~uctx ~udecl typ body
+      else make_univs ~poly ~opaque ~uctx ~udecl typ body
     in
-    let utyp, ubody = make_univs ~initial_euctx ~poly ~opaque ~uctx ~allow_deferred ~udecl typ body in
     definition_entry_core ~opaque ?section_vars ~univs:utyp ~univsbody:ubody ~types:typ ~eff body
   in
   let entries = CList.map make_entry elist  in
-- 
cgit v1.2.3


From afa3d2f09c1a55d38a4c2e02ecac20846d2dc20a Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 25 May 2020 01:30:48 +0200
Subject: [declare] Factor common universe computation in close proof.

---
 vernac/declare.ml | 29 ++++++++++++++++-------------
 1 file changed, 16 insertions(+), 13 deletions(-)

diff --git a/vernac/declare.ml b/vernac/declare.ml
index 514ab52935..5d213abb7a 100644
--- a/vernac/declare.ml
+++ b/vernac/declare.ml
@@ -178,11 +178,17 @@ let prepare_proof ~unsafe_typ { proof } =
   let evd = Evd.minimize_universes evd in
   let to_constr_body c =
     match EConstr.to_constr_opt evd c with
-    | Some p -> p
-    | None -> CErrors.user_err Pp.(str "Some unresolved existential variables remain")
+    | Some p ->
+      Vars.universes_of_constr p, p
+    | None ->
+      CErrors.user_err Pp.(str "Some unresolved existential variables remain")
   in
   let to_constr_typ t =
-    if unsafe_typ then EConstr.Unsafe.to_constr t else to_constr_body t
+    if unsafe_typ
+    then
+      let t = EConstr.Unsafe.to_constr t in
+      Vars.universes_of_constr t, t
+    else to_constr_body t
   in
   (* ppedrot: FIXME, this is surely wrong. There is no reason to duplicate
      side-effects... This may explain why one need to uniquize side-effects
@@ -199,9 +205,8 @@ let prepare_proof ~unsafe_typ { proof } =
   let proofs = List.map (fun (body, typ) -> (to_constr_body body, eff), to_constr_typ typ) initial_goals in
   proofs, Evd.evar_universe_context evd
 
-let make_univs_deferred ~poly ~initial_euctx ~uctx ~udecl typ body =
-  let used_univs_body = Vars.universes_of_constr body in
-  let used_univs_typ = Vars.universes_of_constr typ in
+let make_univs_deferred ~poly ~initial_euctx ~uctx ~udecl
+    (used_univs_typ, typ) (used_univs_body, body) =
   let used_univs = Univ.LSet.union used_univs_body used_univs_typ in
   let utyp = UState.univ_entry ~poly initial_euctx in
   let uctx = UState.constrain_variables (fst (UState.context_set initial_euctx)) uctx in
@@ -212,10 +217,8 @@ let make_univs_deferred ~poly ~initial_euctx ~uctx ~udecl typ body =
   let ubody = UState.check_mono_univ_decl uctx_body udecl in
   utyp, ubody
 
-let make_univs ~poly ~uctx ~opaque ~udecl typ body =
+let make_univs ~poly ~uctx ~opaque ~udecl (used_univs_typ, typ) (used_univs_body, body) =
 
-  let used_univs_body = Vars.universes_of_constr body in
-  let used_univs_typ = Vars.universes_of_constr typ in
   let used_univs = Univ.LSet.union used_univs_body used_univs_typ in
   if poly && opaque && private_poly_univs () then
     let universes = UState.restrict uctx used_univs in
@@ -244,14 +247,14 @@ let close_proof ~opaque ~keep_body_ucst_separate ps =
   let elist, uctx = prepare_proof ~unsafe_typ ps in
   let opaque = match opaque with Opaque -> true | Transparent -> false in
 
-  let make_entry ((body, eff), typ) =
+  let make_entry ((((_ub, body) as b), eff), ((_ut, typ) as t)) =
     (* allow_deferred case *)
     let utyp, ubody =
       if not poly &&
          (keep_body_ucst_separate
           || not (Safe_typing.is_empty_private_constants eff.Evd.seff_private))
-      then make_univs_deferred ~initial_euctx ~poly ~uctx ~udecl typ body
-      else make_univs ~poly ~opaque ~uctx ~udecl typ body
+      then make_univs_deferred ~initial_euctx ~poly ~uctx ~udecl t b
+      else make_univs ~poly ~opaque ~uctx ~udecl t b
     in
     definition_entry_core ~opaque ?section_vars ~univs:utyp ~univsbody:ubody ~types:typ ~eff body
   in
@@ -746,7 +749,7 @@ let return_partial_proof { proof } =
 
 let return_proof ps =
   let p, uctx = prepare_proof ~unsafe_typ:false ps in
-  List.map fst p, uctx
+  List.map (fun (((_ub, body),eff),_) -> (body,eff)) p, uctx
 
 let update_global_env =
   map_proof (fun p ->
-- 
cgit v1.2.3


From 288110c85c364dadbaf7d8cac87b264b6b538bc4 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 25 May 2020 01:42:16 +0200
Subject: [declare] Split univs_poly_private in close_proof

A step towards enforcing some more static invariants.
---
 vernac/declare.ml | 45 ++++++++++++++++++++++++---------------------
 1 file changed, 24 insertions(+), 21 deletions(-)

diff --git a/vernac/declare.ml b/vernac/declare.ml
index 5d213abb7a..6ed7a9e39d 100644
--- a/vernac/declare.ml
+++ b/vernac/declare.ml
@@ -217,27 +217,27 @@ let make_univs_deferred ~poly ~initial_euctx ~uctx ~udecl
   let ubody = UState.check_mono_univ_decl uctx_body udecl in
   utyp, ubody
 
-let make_univs ~poly ~uctx ~opaque ~udecl (used_univs_typ, typ) (used_univs_body, body) =
+let make_univs_private_poly ~poly ~uctx ~udecl (used_univs_typ, typ) (used_univs_body, body) =
+  let used_univs = Univ.LSet.union used_univs_body used_univs_typ in
+  let universes = UState.restrict uctx used_univs in
+  let typus = UState.restrict universes used_univs_typ in
+  let utyp = UState.check_univ_decl ~poly typus udecl in
+  let ubody = Univ.ContextSet.diff
+      (UState.context_set universes)
+      (UState.context_set typus)
+  in
+  utyp, ubody
 
+let make_univs ~poly ~uctx ~udecl (used_univs_typ, typ) (used_univs_body, body) =
   let used_univs = Univ.LSet.union used_univs_body used_univs_typ in
-  if poly && opaque && private_poly_univs () then
-    let universes = UState.restrict uctx used_univs in
-    let typus = UState.restrict universes used_univs_typ in
-    let utyp = UState.check_univ_decl ~poly typus udecl in
-    let ubody = Univ.ContextSet.diff
-        (UState.context_set universes)
-        (UState.context_set typus)
-    in
-    utyp, ubody
-  else
-    (* Since the proof is computed now, we can simply have 1 set of
-       constraints in which we merge the ones for the body and the ones
-       for the typ. We recheck the declaration after restricting with
-       the actually used universes.
-       TODO: check if restrict is really necessary now. *)
-    let ctx = UState.restrict uctx used_univs in
-    let utyp = UState.check_univ_decl ~poly ctx udecl in
-    utyp, Univ.ContextSet.empty
+  (* Since the proof is computed now, we can simply have 1 set of
+     constraints in which we merge the ones for the body and the ones
+     for the typ. We recheck the declaration after restricting with
+     the actually used universes.
+     TODO: check if restrict is really necessary now. *)
+  let ctx = UState.restrict uctx used_univs in
+  let utyp = UState.check_univ_decl ~poly ctx udecl in
+  utyp, Univ.ContextSet.empty
 
 let close_proof ~opaque ~keep_body_ucst_separate ps =
 
@@ -248,13 +248,16 @@ let close_proof ~opaque ~keep_body_ucst_separate ps =
   let opaque = match opaque with Opaque -> true | Transparent -> false in
 
   let make_entry ((((_ub, body) as b), eff), ((_ut, typ) as t)) =
-    (* allow_deferred case *)
     let utyp, ubody =
+      (* allow_deferred case *)
       if not poly &&
          (keep_body_ucst_separate
           || not (Safe_typing.is_empty_private_constants eff.Evd.seff_private))
       then make_univs_deferred ~initial_euctx ~poly ~uctx ~udecl t b
-      else make_univs ~poly ~opaque ~uctx ~udecl t b
+      (* private_poly_univs case *)
+      else if poly && opaque && private_poly_univs ()
+      then make_univs_private_poly ~poly ~uctx ~udecl t b
+      else make_univs ~poly ~uctx ~udecl t b
     in
     definition_entry_core ~opaque ?section_vars ~univs:utyp ~univsbody:ubody ~types:typ ~eff body
   in
-- 
cgit v1.2.3