When declaring constants/inductives use ContextSet if monomorphic.

Also use constant_universes_entry instead of a bool flag to indicate
polymorphism in ParameterEntry.

There are a few places where we convert back to ContextSet because
check_univ_decl returns a UContext, this could be improved.

1 files changed, 7 insertions, 5 deletions

diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index ea0408169..905173efc 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -331,7 +331,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now
   let initial_euctx = Proof.initial_euctx proof in
   let fpl, univs = Future.split2 fpl in
   let universes = if poly || now then Future.force univs else initial_euctx in
-  let univctx = Evd.check_univ_decl (Evd.from_ctx universes) universe_decl in
+  let univctx = UState.check_univ_decl universes universe_decl in
   let binders = if poly then Some (UState.universe_binders universes) else None in
   (* Because of dependent subgoals at the beginning of proofs, we could
      have existential variables in the initial types of goals, we need to
@@ -360,7 +360,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now
              the body.  So we keep the two sets distinct. *)
 	  let used_univs = Univ.LSet.union used_univs_body used_univs_typ in
           let ctx_body = UState.restrict ctx used_univs in
-          let univs = Evd.check_univ_decl (Evd.from_ctx ctx_body) universe_decl in
+          let univs = UState.check_univ_decl ctx_body universe_decl in
           (initunivs, typ), ((body, Univ.ContextSet.of_context univs), eff)
         else
           (* Since the proof is computed now, we can simply have 1 set of
@@ -370,7 +370,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now
              TODO: check if restrict is really necessary now. *)
           let used_univs = Univ.LSet.union used_univs_body used_univs_typ in
           let ctx = UState.restrict universes used_univs in
-          let univs = Evd.check_univ_decl (Evd.from_ctx ctx) universe_decl in
+          let univs = UState.check_univ_decl ctx universe_decl in
           (univs, typ), ((body, Univ.ContextSet.empty), eff)
       in 
        fun t p -> Future.split2 (Future.chain p (make_body t))
@@ -383,7 +383,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now
              the declaration as well. If the declaration is non-extensible,
              this will prevent the body from adding universes and constraints. *)
           let bodyunivs = constrain_variables univctx (Future.force univs) in
-          let univs = Evd.check_univ_decl (Evd.from_ctx bodyunivs) universe_decl in
+          let univs = UState.check_univ_decl bodyunivs universe_decl in
           (pt,Univ.ContextSet.of_context univs),eff)
   in
   let entry_fn p (_, t) =
@@ -392,7 +392,9 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now
     let univs, typ = Future.force univstyp in
     let univs =
       if poly then Entries.Polymorphic_const_entry univs
-      else Entries.Monomorphic_const_entry univs
+      else
+        (* FIXME be smarter about the unnecessary context linearisation in make_body *)
+        Entries.Monomorphic_const_entry (Univ.ContextSet.of_context univs)
     in
     {Entries.
       const_entry_body = body;