Local universes for opaque polymorphic constants.

30 files changed, 222 insertions, 75 deletions

diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index ed617d73c2..c36d96f2ba 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -20,7 +20,13 @@ let check_constant_declaration env kn cb =
     | Monomorphic_const ctx -> false, push_context_set ~strict:true ctx env
     | Polymorphic_const auctx ->
       let ctx = Univ.AUContext.repr auctx in
-      true, push_context ~strict:false ctx env
+      let env = push_context ~strict:false ctx env in
+      true, env
+  in
+  let env' = match cb.const_private_poly_univs, (cb.const_body, poly) with
+    | None, _ -> env'
+    | Some local, (OpaqueDef _, true) -> push_subgraph local env'
+    | Some _, _ -> assert false
   in
   let ty = cb.const_type in
   let _ = infer_type env' ty in
diff --git a/checker/values.ml b/checker/values.ml
index 0de8a3e03f..388123baaf 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -227,6 +227,7 @@ let v_cb = v_tuple "constant_body"
     v_constr;
     Any;
     v_const_univs;
+    Opt v_context_set;
     v_bool;
     v_typing_flags|]
 
diff --git a/engine/uState.ml b/engine/uState.ml
index 5747ae2ad4..5b0671c06e 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -441,11 +441,13 @@ let restrict_universe_context (univs, csts) keep =
   if LSet.is_empty removed then univs, csts
   else
   let allunivs = Constraint.fold (fun (u,_,v) all -> LSet.add u (LSet.add v all)) csts univs in
-  let g = UGraph.empty_universes in
-  let g = LSet.fold UGraph.add_universe_unconstrained allunivs g in
+  let g = UGraph.initial_universes in
+  let g = LSet.fold (fun v g -> if Level.is_small v then g else UGraph.add_universe v false g) allunivs g in
   let g = UGraph.merge_constraints csts g in
-  let allkept = LSet.diff allunivs removed in
+  let allkept = LSet.union (UGraph.domain UGraph.initial_universes) (LSet.diff allunivs removed) in
   let csts = UGraph.constraints_for ~kept:allkept g in
+  let csts = Constraint.filter (fun (l,d,r) ->
+      not ((Level.is_set l && d == Le) || (Level.is_prop l && d == Lt && Level.is_set r))) csts in
   (LSet.inter univs keep, csts)
 
 let restrict ctx vars =
diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index b39aed01e8..f4b4834d98 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -158,6 +158,7 @@ type result = {
   cook_body : constant_def;
   cook_type : types;
   cook_universes : constant_universes;
+  cook_private_univs : Univ.ContextSet.t option;
   cook_inline : inline;
   cook_context : Constr.named_context option;
 }
@@ -204,7 +205,8 @@ let lift_univs cb subst auctx0 =
     else
       let ainst = Univ.make_abstract_instance auctx in
       let subst = Instance.append subst ainst in
-      let auctx' = Univ.subst_univs_level_abstract_universe_context (Univ.make_instance_subst subst) auctx in
+      let substf = Univ.make_instance_subst subst in
+      let auctx' = Univ.subst_univs_level_abstract_universe_context substf auctx in
       subst, (Polymorphic_const (AUContext.union auctx0 auctx'))
 
 let cook_constant ~hcons { from = cb; info } =
@@ -229,10 +231,15 @@ let cook_constant ~hcons { from = cb; info } =
 		  hyps)
       hyps0 ~init:cb.const_hyps in
   let typ = abstract_constant_type (expmod cb.const_type) hyps in
+  let private_univs = Option.map (on_snd (Univ.subst_univs_level_constraints
+                                            (Univ.make_instance_subst usubst)))
+      cb.const_private_poly_univs
+  in
   {
     cook_body = body;
     cook_type = typ;
     cook_universes = univs;
+    cook_private_univs = private_univs;
     cook_inline = cb.const_inline_code;
     cook_context = Some const_hyps;
   }
diff --git a/kernel/cooking.mli b/kernel/cooking.mli
index 6ebe691b83..7ff4b657d3 100644
--- a/kernel/cooking.mli
+++ b/kernel/cooking.mli
@@ -21,6 +21,7 @@ type result = {
   cook_body : constant_def;
   cook_type : types;
   cook_universes : constant_universes;
+  cook_private_univs : Univ.ContextSet.t option;
   cook_inline : inline;
   cook_context : Constr.named_context option;
 }
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index c1b38b4156..68ccd933e7 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -78,6 +78,7 @@ type constant_body = {
     const_type : types;
     const_body_code : Cemitcodes.to_patch_substituted option;
     const_universes : constant_universes;
+    const_private_poly_univs : Univ.ContextSet.t option;
     const_inline_code : bool;
     const_typing_flags : typing_flags; (** The typing options which
                                            were used for
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 3ed599c538..90638be3ec 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -101,6 +101,7 @@ let subst_const_body sub cb =
         const_body_code =
           Option.map (Cemitcodes.subst_to_patch_subst sub) cb.const_body_code;
         const_universes = cb.const_universes;
+        const_private_poly_univs = cb.const_private_poly_univs;
         const_inline_code = cb.const_inline_code;
         const_typing_flags = cb.const_typing_flags }
 
@@ -126,14 +127,20 @@ let hcons_const_universes cbu =
   match cbu with
   | Monomorphic_const ctx -> 
     Monomorphic_const (Univ.hcons_universe_context_set ctx)
-  | Polymorphic_const ctx -> 
+  | Polymorphic_const ctx ->
     Polymorphic_const (Univ.hcons_abstract_universe_context ctx)
 
+let hcons_const_private_univs = function
+  | None -> None
+  | Some univs -> Some (Univ.hcons_universe_context_set univs)
+
 let hcons_const_body cb =
   { cb with
     const_body = hcons_const_def cb.const_body;
     const_type = Constr.hcons cb.const_type;
-    const_universes = hcons_const_universes cb.const_universes }
+    const_universes = hcons_const_universes cb.const_universes;
+    const_private_poly_univs = hcons_const_private_univs cb.const_private_poly_univs;
+  }
 
 (** {6 Inductive types } *)
 
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 019c0a6819..a6bc579cf7 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -380,6 +380,18 @@ let add_universes_set strict ctx g =
 let push_context_set ?(strict=false) ctx env =
   map_universes (add_universes_set strict ctx) env
 
+let push_subgraph (levels,csts) env =
+  let add_subgraph g =
+    let newg = Univ.LSet.fold (fun v g -> UGraph.add_universe v false g) levels g in
+    let newg = UGraph.merge_constraints csts newg in
+    (if not (Univ.Constraint.is_empty csts) then
+       let restricted = UGraph.constraints_for ~kept:(UGraph.domain g) newg in
+       (if not (UGraph.check_constraints restricted g) then
+          CErrors.anomaly Pp.(str "Local constraints imply new transitive constraints.")));
+    newg
+  in
+  map_universes add_subgraph env
+
 let set_engagement c env = (* Unsafe *)
   { env with env_stratification =
     { env.env_stratification with env_engagement = c } }
diff --git a/kernel/environ.mli b/kernel/environ.mli
index c285f907fc..dd0df7d3d6 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -268,6 +268,12 @@ val push_context : ?strict:bool -> Univ.UContext.t -> env -> env
 val push_context_set : ?strict:bool -> Univ.ContextSet.t -> env -> env
 val push_constraints_to_env : 'a Univ.constrained -> env -> env
 
+val push_subgraph : Univ.ContextSet.t -> env -> env
+(** [push_subgraph univs env] adds the universes and constraints in
+   [univs] to [env] as [push_context_set ~strict:false univs env], and
+   also checks that they do not imply new transitive constraints
+   between pre-existing universes in [env]. *)
+
 val set_engagement : engagement -> env -> env
 val set_typing_flags : typing_flags -> env -> env
 
diff --git a/kernel/modops.ml b/kernel/modops.ml
index 0dde1c7e75..f43dbd88f9 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -338,7 +338,8 @@ let strengthen_const mp_from l cb resolver =
       | Polymorphic_const ctx -> Univ.make_abstract_instance ctx
     in
       { cb with
-	const_body = Def (Mod_subst.from_val (mkConstU (con,u)));
+        const_body = Def (Mod_subst.from_val (mkConstU (con,u)));
+        const_private_poly_univs = None;
 	const_body_code = Some (Cemitcodes.from_val (Cbytegen.compile_alias con)) }
 
 let rec strengthen_mod mp_from mp_to mb =
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 2464df799e..98a7014bee 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -599,7 +599,7 @@ let inline_side_effects env body side_eff =
         let subst = Cmap_env.add c (Inr var) subst in
         let ctx = Univ.ContextSet.union ctx univs in
         (subst, var + 1, ctx, (cname c, b, ty, opaque) :: args)
-      | Polymorphic_const _auctx ->
+      | Polymorphic_const _ ->
         (** Inline the term to emulate universe polymorphism *)
         let subst = Cmap_env.add c (Inl b) subst in
         (subst, var, ctx, args)
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 35fa871b4e..f9fdbdd68e 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -88,6 +88,7 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
         Cooking.cook_body = Undef nl;
         cook_type = t;
         cook_universes = univs;
+        cook_private_univs = None;
         cook_inline = false;
         cook_context = ctx;
       }
@@ -130,6 +131,7 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
         Cooking.cook_body = def;
         cook_type = typ;
         cook_universes = Monomorphic_const univs;
+        cook_private_univs = None;
         cook_inline = c.const_entry_inline_code;
         cook_context = c.const_entry_secctx;
       }
@@ -145,24 +147,25 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
         let body, ctx', _ = handle env body side_eff in
         body, Univ.ContextSet.union ctx ctx'
       in
-      let env, usubst, univs = match c.const_entry_universes with
+      let env, usubst, univs, private_univs = match c.const_entry_universes with
       | Monomorphic_const_entry univs ->
         let ctx = Univ.ContextSet.union univs ctx in
         let env = push_context_set ~strict:true ctx env in
-        env, Univ.empty_level_subst, Monomorphic_const ctx
+        env, Univ.empty_level_subst, Monomorphic_const ctx, None
       | Polymorphic_const_entry (nas, uctx) ->
-        (** Ensure not to generate internal constraints in polymorphic mode.
-            The only way for this to happen would be that either the body
-            contained deferred universes, or that it contains monomorphic
-            side-effects. The first property is ruled out by upper layers,
-            and the second one is ensured by the fact we currently
-            unconditionally export side-effects from polymorphic definitions,
-            i.e. [trust] is always [Pure]. *)
-        let () = assert (Univ.ContextSet.is_empty ctx) in
+        (** [ctx] must contain local universes, such that it has no impact
+            on the rest of the graph (up to transitivity). *)
         let env = push_context ~strict:false uctx env in
         let sbst, auctx = Univ.abstract_universes nas uctx in
         let sbst = Univ.make_instance_subst sbst in
-        env, sbst, Polymorphic_const auctx
+        let env, local =
+          if opaque then
+            push_subgraph ctx env, Some (on_snd (Univ.subst_univs_level_constraints sbst) ctx)
+          else
+          if Univ.ContextSet.is_empty ctx then env, None
+          else CErrors.anomaly Pp.(str "Local universes in non-opaque polymorphic definition.")
+        in
+        env, sbst, Polymorphic_const auctx, local
       in
       let j = infer env body in
       let typ = match typ with
@@ -183,6 +186,7 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
         Cooking.cook_body = def;
         cook_type = typ;
         cook_universes = univs;
+        cook_private_univs = private_univs;
         cook_inline = c.const_entry_inline_code;
         cook_context = c.const_entry_secctx;
       }
@@ -277,6 +281,7 @@ let build_constant_declaration _kn env result =
     const_type = typ;
     const_body_code = tps;
     const_universes = univs;
+    const_private_poly_univs = result.cook_private_univs;
     const_inline_code = result.cook_inline;
     const_typing_flags = Environ.typing_flags env }
 
diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml
index 9083156745..fe07a1c90e 100644
--- a/kernel/uGraph.ml
+++ b/kernel/uGraph.ml
@@ -866,6 +866,8 @@ let constraints_for ~kept g =
         arc.ltle csts)
     kept csts
 
+let domain g = LMap.domain g.entries
+
 (** [sort_universes g] builds a totally ordered universe graph.  The
     output graph should imply the input graph (and the implication
     will be strict most of the time), but is not necessarily minimal.
diff --git a/kernel/uGraph.mli b/kernel/uGraph.mli
index a2cc5b3116..a389b35993 100644
--- a/kernel/uGraph.mli
+++ b/kernel/uGraph.mli
@@ -79,6 +79,9 @@ val constraints_of_universes : t -> Constraint.t * LSet.t list
     eg if [g] is [a <= b <= c] then [constraints_for ~kept:{a, c} g] is [a <= c]. *)
 val constraints_for : kept:LSet.t -> t -> Constraint.t
 
+val domain : t -> LSet.t
+(** Known universes *)
+
 val check_subtype : AUContext.t check_function
 (** [check_subtype univ ctx1 ctx2] checks whether [ctx2] is an instance of
     [ctx1]. *)
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 1cf952576d..5ba9735690 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -322,7 +322,7 @@ let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_prin
     (* 	end; *)
 
       let open Proof_global in
-      let { id; entries; persistence } = fst @@ close_proof ~keep_body_ucst_separate:false (fun x -> x) in
+      let { id; entries; persistence } = fst @@ close_proof ~opaque:Transparent ~keep_body_ucst_separate:false (fun x -> x) in
       match entries with
       | [entry] ->
         discard_current ();
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index 712eb21ee6..f9f4d7f7f8 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -96,8 +96,9 @@ let print_ref reduce ref udecl =
     then Printer.pr_universe_instance sigma inst
     else mt ()
   in
+  let priv = None in (* We deliberately don't print private univs in About. *)
   hov 0 (pr_global ref ++ inst ++ str " :" ++ spc () ++ pr_letype_env env sigma typ ++ 
-           Printer.pr_abstract_universe_ctx sigma ?variance univs)
+           Printer.pr_abstract_universe_ctx sigma ?variance univs ~priv)
 
 (********************************)
 (** Printing implicit arguments *)
@@ -580,11 +581,11 @@ let print_constant with_values sep sp udecl =
 	str"*** [ " ++
 	print_basename sp ++ print_instance sigma cb ++ str " : " ++ cut () ++ pr_ltype typ ++
 	str" ]" ++
-        Printer.pr_constant_universes sigma univs
+        Printer.pr_constant_universes sigma univs ~priv:cb.const_private_poly_univs
     | Some (c, ctx) ->
 	print_basename sp ++ print_instance sigma cb ++ str sep ++ cut () ++
 	(if with_values then print_typed_body env sigma (Some c,typ) else pr_ltype typ)++
-        Printer.pr_constant_universes sigma univs)
+        Printer.pr_constant_universes sigma univs ~priv:cb.const_private_poly_univs)
 
 let gallina_print_constant_with_infos sp udecl =
   print_constant true " = " sp udecl ++
diff --git a/printing/printer.ml b/printing/printer.ml
index 4840577cbf..ebe8e3eebb 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -211,16 +211,21 @@ let pr_universe_ctx sigma ?variance c =
   else
     mt()
 
-let pr_abstract_universe_ctx sigma ?variance c =
-  if !Detyping.print_universes && not (Univ.AUContext.is_empty c) then
+let pr_abstract_universe_ctx sigma ?variance c ~priv =
+  let open Univ in
+  let priv = Option.default Univ.ContextSet.empty priv in
+  if !Detyping.print_universes && not (Univ.AUContext.is_empty c && Univ.ContextSet.is_empty priv) then
+    let local = if ContextSet.is_empty priv then mt() else
+        str "local: " ++ Univ.pr_universe_context_set (Termops.pr_evd_level sigma) priv
+    in
     fnl()++pr_in_comment (fun c -> v 0
-      (Univ.pr_abstract_universe_context (Termops.pr_evd_level sigma) ?variance c)) c
+      (Univ.pr_abstract_universe_context (Termops.pr_evd_level sigma) ?variance c) ++ v 0 local) c
   else
     mt()
 
-let pr_constant_universes sigma = function
+let pr_constant_universes sigma ~priv = function
   | Declarations.Monomorphic_const ctx -> pr_universe_ctx_set sigma ctx
-  | Declarations.Polymorphic_const ctx -> pr_abstract_universe_ctx sigma ctx
+  | Declarations.Polymorphic_const ctx -> pr_abstract_universe_ctx sigma ctx ~priv
 
 let pr_cumulativity_info sigma cumi =
   if !Detyping.print_universes 
diff --git a/printing/printer.mli b/printing/printer.mli
index cefc005c74..b0232ec4ac 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -87,10 +87,10 @@ val pr_universe_instance   : evar_map -> Univ.Instance.t -> Pp.t
 val pr_universe_instance_constraints : evar_map -> Univ.Instance.t -> Univ.Constraint.t -> Pp.t
 val pr_universe_ctx        : evar_map -> ?variance:Univ.Variance.t array ->
   Univ.UContext.t -> Pp.t
-val pr_abstract_universe_ctx        : evar_map -> ?variance:Univ.Variance.t array ->
-  Univ.AUContext.t -> Pp.t
+val pr_abstract_universe_ctx : evar_map -> ?variance:Univ.Variance.t array ->
+  Univ.AUContext.t -> priv:Univ.ContextSet.t option -> Pp.t
 val pr_universe_ctx_set    : evar_map -> Univ.ContextSet.t -> Pp.t
-val pr_constant_universes  : evar_map -> Declarations.constant_universes -> Pp.t
+val pr_constant_universes  : evar_map -> priv:Univ.ContextSet.t option -> Declarations.constant_universes -> Pp.t
 val pr_cumulativity_info   : evar_map -> Univ.CumulativityInfo.t -> Pp.t
 val pr_abstract_cumulativity_info   : evar_map -> Univ.ACumulativityInfo.t -> Pp.t
 
diff --git a/printing/printmod.ml b/printing/printmod.ml
index 2c3ab46670..1360ad4af4 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -310,7 +310,7 @@ let print_body is_impl extent env mp (l,body) =
 		hov 2 (str ":= " ++
                        Printer.pr_lconstr_env env sigma (Mod_subst.force_constr l))
 	      | _ -> mt ()) ++ str "." ++
-            Printer.pr_abstract_universe_ctx sigma ctx)
+            Printer.pr_abstract_universe_ctx sigma ctx ~priv:cb.const_private_poly_univs)
     | SFBmind mib ->
       match extent with
       | WithContents ->
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 81122e6858..647e87150b 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -138,7 +138,7 @@ let build_constant_by_tactic id ctx sign ?(goal_kind = Global, false, Proof Theo
   try
     let status = by tac in
     let open Proof_global in
-    let { entries; universes } = fst @@ close_proof ~keep_body_ucst_separate:false (fun x -> x) in
+    let { entries; universes } = fst @@ close_proof ~opaque:Transparent ~keep_body_ucst_separate:false (fun x -> x) in
     match entries with
     | [entry] ->
       discard_current ();
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index cb4b5759dc..af97d40579 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -318,10 +318,23 @@ let get_open_goals () =
 
 type closed_proof_output = (Constr.t * Safe_typing.private_constants) list * UState.t
 
-let close_proof ~keep_body_ucst_separate ?feedback_id ~now
+let private_poly_univs =
+  let b = ref true in
+  let _ = Goptions.(declare_bool_option {
+      optdepr = false;
+      optname = "use private polymorphic universes for Qed constants";
+      optkey = ["Private";"Polymorphic";"Universes"];
+      optread = (fun () -> !b);
+      optwrite = ((:=) b);
+    })
+  in
+  fun () -> !b
+
+let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now
                 (fpl : closed_proof_output Future.computation) =
   let { pid; section_vars; strength; proof; terminator; universe_decl } =
     cur_pstate () in
+  let opaque = match opaque with Opaque -> true | Transparent -> false in
   let poly = pi2 strength (* Polymorphic *) in
   let initial_goals = Proof.initial_goals proof in
   let initial_euctx = Proof.initial_euctx proof in
@@ -358,6 +371,16 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now
           let ctx_body = UState.restrict ctx used_univs in
           let univs = UState.check_mono_univ_decl ctx_body universe_decl in
           (initunivs, typ), ((body, univs), eff)
+        else if poly && opaque && private_poly_univs () then
+          let used_univs = Univ.LSet.union used_univs_body used_univs_typ in
+          let universes = UState.restrict universes used_univs in
+          let typus = UState.restrict universes used_univs_typ in
+          let udecl = UState.check_univ_decl ~poly typus universe_decl in
+          let ubody = Univ.ContextSet.diff
+              (UState.context_set universes)
+              (UState.context_set typus)
+          in
+          (udecl, typ), ((body, ubody), eff)
         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
@@ -394,7 +417,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now
       const_entry_feedback = feedback_id;
       const_entry_type  = Some typ;
       const_entry_inline_code = false;
-      const_entry_opaque = true;
+      const_entry_opaque = opaque;
       const_entry_universes = univs; }
   in
   let entries = Future.map2 entry_fn fpl initial_goals in
@@ -425,10 +448,10 @@ let return_proof ?(allow_partial=false) () =
     List.map (fun (c, _) -> (EConstr.to_constr evd c, eff)) initial_goals in
     proofs, Evd.evar_universe_context evd
 
-let close_future_proof ~feedback_id proof =
-  close_proof ~keep_body_ucst_separate:true ~feedback_id ~now:false proof
-let close_proof ~keep_body_ucst_separate fix_exn =
-  close_proof ~keep_body_ucst_separate ~now:true
+let close_future_proof ~opaque ~feedback_id proof =
+  close_proof ~opaque ~keep_body_ucst_separate:true ~feedback_id ~now:false proof
+let close_proof ~opaque ~keep_body_ucst_separate fix_exn =
+  close_proof ~opaque ~keep_body_ucst_separate ~now:true
     (Future.from_val ~fix_exn (return_proof ()))
 
 (** Gets the current terminator without checking that the proof has
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index e3808bc36d..d9c32cf9d5 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -86,7 +86,7 @@ val update_global_env : unit -> unit
 
 (* Takes a function to add to the exceptions data relative to the
    state in which the proof was built *)
-val close_proof : keep_body_ucst_separate:bool -> Future.fix_exn -> closed_proof
+val close_proof : opaque:opacity_flag -> keep_body_ucst_separate:bool -> Future.fix_exn -> closed_proof
 
 (* Intermediate step necessary to delegate the future.
  * Both access the current proof state. The former is supposed to be
@@ -97,7 +97,7 @@ type closed_proof_output = (Constr.t * Safe_typing.private_constants) list * USt
 (* If allow_partial is set (default no) then an incomplete proof
  * is allowed (no error), and a warn is given if the proof is complete. *)
 val return_proof : ?allow_partial:bool -> unit -> closed_proof_output
-val close_future_proof : feedback_id:Stateid.t ->
+val close_future_proof : opaque:opacity_flag -> feedback_id:Stateid.t ->
   closed_proof_output Future.computation -> closed_proof
 
 (** Gets the current terminator without checking that the proof has
diff --git a/stm/stm.ml b/stm/stm.ml
index 9359ab15e2..74e951b3b6 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -20,6 +20,8 @@ let stm_pperr_endline s = if !stm_debug then begin stm_pp_err (s ()) end else ()
 
 let stm_prerr_debug   s = if !Flags.debug then begin stm_pr_err (s ()) end else ()
 
+let is_vtkeep = function Vernacextend.VtKeep _ -> true | _ -> false
+
 open Pp
 open CErrors
 open Names
@@ -1532,12 +1534,13 @@ end = struct (* {{{ *)
       let st = Vernacstate.freeze_interp_state `No in
       if not drop then begin
         let checked_proof = Future.chain future_proof (fun p ->
+          let opaque = Proof_global.Opaque in
 
           (* Unfortunately close_future_proof and friends are not pure so we need
              to set the state manually here *)
           Vernacstate.unfreeze_interp_state st;
           let pobject, _ =
-            Proof_global.close_future_proof ~feedback_id:stop (Future.from_val ~fix_exn p) in
+            Proof_global.close_future_proof ~opaque ~feedback_id:stop (Future.from_val ~fix_exn p) in
           let terminator = (* The one sent by master is an InvalidKey *)
             Lemmas.(standard_proof_terminator [] (mk_hook (fun _ _ -> ()))) in
 
@@ -1545,7 +1548,7 @@ end = struct (* {{{ *)
           stm_vernac_interp stop
             ~proof:(pobject, terminator) st
             { verbose = false; loc; indentation = 0; strlen = 0;
-              expr = VernacExpr ([], VernacEndProof (Proved (Proof_global.Opaque,None))) }) in
+              expr = VernacExpr ([], VernacEndProof (Proved (opaque,None))) }) in
         ignore(Future.join checked_proof);
       end;
       (* STATE: Restore the state XXX: handle exn *)
@@ -1680,9 +1683,10 @@ end = struct (* {{{ *)
       (* The original terminator, a hook, has not been saved in the .vio*)
       Proof_global.set_terminator
         (Lemmas.standard_proof_terminator []
-          (Lemmas.mk_hook (fun _ _ -> ())));
+           (Lemmas.mk_hook (fun _ _ -> ())));
+      let opaque = Proof_global.Opaque in
       let proof =
-        Proof_global.close_proof ~keep_body_ucst_separate:true (fun x -> x) in
+        Proof_global.close_proof ~opaque ~keep_body_ucst_separate:true (fun x -> x) in
       (* We jump at the beginning since the kernel handles side effects by also
        * looking at the ones that happen to be present in the current env *)
       Reach.known_state ~doc:dummy_doc (* XXX should be document *) ~cache:`No start;
@@ -1695,7 +1699,7 @@ end = struct (* {{{ *)
       let st = Vernacstate.freeze_interp_state `No in
       ignore(stm_vernac_interp stop ~proof st
         { verbose = false; loc; indentation = 0; strlen = 0;
-          expr = VernacExpr ([], VernacEndProof (Proved (Proof_global.Opaque,None))) });
+          expr = VernacExpr ([], VernacEndProof (Proved (opaque,None))) });
       `OK proof
       end
     with e ->
@@ -2252,7 +2256,7 @@ let collect_proof keep cur hd brkind id =
      else
        let rc = collect (Some cur) [] id in
        if is_empty rc then make_sync `AlreadyEvaluated rc
-       else if (keep == VtKeep || keep == VtKeepAsAxiom) &&
+       else if (is_vtkeep keep || keep == VtKeepAsAxiom) &&
           (not(State.is_cached_and_valid id) || !cur_opt.async_proofs_full)
        then check_policy rc
        else make_sync `AlreadyEvaluated rc
@@ -2441,7 +2445,7 @@ let known_state ~doc ?(redefine_qed=false) ~cache id =
       | `Qed ({ qast = x; keep; brinfo; brname } as qed, eop) ->
           let rec aux = function
           | `ASync (block_start, nodes, name, delegate) -> (fun () ->
-                assert(keep == VtKeep || keep == VtKeepAsAxiom);
+                assert(is_vtkeep keep || keep == VtKeepAsAxiom);
                 let drop_pt = keep == VtKeepAsAxiom in
                 let block_stop, exn_info, loc = eop, (id, eop), x.loc in
                 log_processing_async id name;
@@ -2450,11 +2454,11 @@ let known_state ~doc ?(redefine_qed=false) ~cache id =
                 | { VCS.kind = `Edit _ }, None -> assert false
                 | { VCS.kind = `Edit (_,_,_, okeep, _) }, Some (ofp, cancel) ->
                     assert(redefine_qed = true);
-                    if okeep != keep then
+                    if okeep <> keep then
                       msg_warning(strbrk("The command closing the proof changed. "
                         ^"The kernel cannot take this into account and will "
-                        ^(if keep == VtKeep then "not check " else "reject ")
-                        ^"the "^(if keep == VtKeep then "new" else "incomplete")
+                        ^(if is_vtkeep keep then "not check " else "reject ")
+                        ^"the "^(if is_vtkeep keep then "new" else "incomplete")
                         ^" proof. Reprocess the command declaring "
                         ^"the proof's statement to avoid that."));
                     let fp, cancel =
@@ -2477,8 +2481,12 @@ let known_state ~doc ?(redefine_qed=false) ~cache id =
                           ~drop_pt exn_info block_stop, ref false
                     in
                     qed.fproof <- Some (fp, cancel);
+                    let opaque = match keep with
+                      | VtKeep opaque -> opaque
+                      | _ -> Proof_global.Opaque (* this seems strange *)
+                    in
                     let proof =
-                      Proof_global.close_future_proof ~feedback_id:id fp in
+                      Proof_global.close_future_proof ~opaque ~feedback_id:id fp in
                     if not delegate then ignore(Future.compute fp);
                     reach view.next;
                     let st = Vernacstate.freeze_interp_state `No in
@@ -2506,8 +2514,8 @@ let known_state ~doc ?(redefine_qed=false) ~cache id =
                       let ctx = UState.empty in
                       let fp = Future.from_val ([],ctx) in
                       qed.fproof <- Some (fp, ref false); None
-                  | VtKeep ->
-                      Some(Proof_global.close_proof
+                  | VtKeep opaque ->
+                      Some(Proof_global.close_proof ~opaque
                                 ~keep_body_ucst_separate:false
                                 (State.exn_on id ~valid:eop)) in
                 if keep != VtKeepAsAxiom then
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index 526858bd73..e026539751 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -26,7 +26,7 @@ let string_of_vernac_type = function
   | VtUnknown -> "Unknown"
   | VtStartProof _ -> "StartProof"
   | VtSideff _ -> "Sideff"
-  | VtQed VtKeep -> "Qed(keep)"
+  | VtQed (VtKeep _) -> "Qed(keep)"
   | VtQed VtKeepAsAxiom -> "Qed(admitted)"
   | VtQed VtDrop -> "Qed(drop)"
   | VtProofStep { parallel; proof_block_detection } ->
@@ -66,7 +66,8 @@ let classify_vernac e =
     (* Qed *)
     | VernacAbort _ -> VtQed VtDrop, VtLater
     | VernacEndProof Admitted -> VtQed VtKeepAsAxiom, VtLater
-    | VernacEndProof _ | VernacExactProof _ -> VtQed VtKeep, VtLater
+    | VernacEndProof (Proved (opaque,_)) -> VtQed (VtKeep opaque), VtLater
+    | VernacExactProof _ -> VtQed (VtKeep Proof_global.Opaque), VtLater
     (* Query *)
     | VernacShow _ | VernacPrint _ | VernacSearch _ | VernacLocate _
     | VernacCheckMayEval _ -> VtQuery, VtLater
diff --git a/test-suite/success/polymorphism.v b/test-suite/success/polymorphism.v
index d76b307914..339f798240 100644
--- a/test-suite/success/polymorphism.v
+++ b/test-suite/success/polymorphism.v
@@ -165,19 +165,13 @@ Module binders.
     exact A.
   Defined.
 
-  Definition nomoreu@{i j | i < j +} (A : Type@{i}) : Type@{j}.
-    pose(foo:=Type).
-    exact A.
-    Fail Defined.
-  Abort.
-
-  Polymorphic Definition moreu@{i j +} (A : Type@{i}) : Type@{j}.
-    pose(foo:=Type).
-    exact A.
-  Defined.
+  Polymorphic Lemma hidden_strict_type : Type.
+  Proof.
+    exact Type.
+  Qed.
+  Check hidden_strict_type@{_}.
+  Fail Check hidden_strict_type@{Set}.
 
-  Check moreu@{_ _ _ _}.
-  
   Fail Definition morec@{i j|} (A : Type@{i}) : Type@{j} := A.
 
   (* By default constraints are extensible *)
diff --git a/test-suite/success/private_univs.v b/test-suite/success/private_univs.v
new file mode 100644
index 0000000000..5c30b33435
--- /dev/null
+++ b/test-suite/success/private_univs.v
@@ -0,0 +1,50 @@
+Set Universe Polymorphism. Set Printing Universes.
+
+Definition internal_defined@{i j | i < j +} (A : Type@{i}) : Type@{j}.
+  pose(foo:=Type). (* 1 universe for the let body + 1 for the type *)
+  exact A.
+  Fail Defined.
+Abort.
+
+Definition internal_defined@{i j +} (A : Type@{i}) : Type@{j}.
+pose(foo:=Type).
+exact A.
+Defined.
+Check internal_defined@{_ _ _ _}.
+
+Module M.
+Lemma internal_qed@{i j|i<=j} (A:Type@{i}) : Type@{j}.
+Proof.
+  pose (foo := Type).
+  exact A.
+Qed.
+Check internal_qed@{_ _}.
+End M.
+Include M.
+(* be careful to remove const_private_univs in Include! will be coqchk'd *)
+
+Unset Strict Universe Declaration.
+Lemma private_transitivity@{i j} (A:Type@{i}) : Type@{j}.
+Proof.
+  pose (bar := Type : Type@{j}).
+  pose (foo := Type@{i} : bar).
+  exact bar.
+Qed.
+
+Definition private_transitivity'@{i j|i < j} := private_transitivity@{i j}.
+Fail Definition dummy@{i j|j <= i +} := private_transitivity@{i j}.
+
+Unset Private Polymorphic Universes.
+Lemma internal_noprivate_qed@{i j|i<=j} (A:Type@{i}) : Type@{j}.
+Proof.
+  pose (foo := Type).
+  exact A.
+  Fail Qed.
+Abort.
+
+Lemma internal_noprivate_qed@{i j +} (A:Type@{i}) : Type@{j}.
+Proof.
+  pose (foo := Type).
+  exact A.
+Qed.
+Check internal_noprivate_qed@{_ _ _ _}.
diff --git a/theories/Compat/Coq89.v b/theories/Compat/Coq89.v
index 49b9e4c951..81a087b525 100644
--- a/theories/Compat/Coq89.v
+++ b/theories/Compat/Coq89.v
@@ -10,3 +10,5 @@
 
 (** Compatibility file for making Coq act similar to Coq v8.9 *)
 Local Set Warnings "-deprecated".
+
+Unset Private Polymorphic Universes.
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index de020926f6..5204a16f9c 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -311,7 +311,7 @@ let universe_proof_terminator compute_guard hook =
       | Transparent -> false, true
       | Opaque      -> true, false
     in
-    let const = {const with const_entry_opaque = is_opaque} in
+    assert (is_opaque == const.const_entry_opaque);
     let id = match idopt with
       | None -> id
       | Some { CAst.v = save_id } -> check_anonymity id save_id; save_id in
@@ -498,13 +498,13 @@ let save_proof ?proof = function
             Admitted(id,k,(sec_vars, (typ, ctx), None), universes)
       in
       Proof_global.apply_terminator (Proof_global.get_terminator ()) pe
-  | Vernacexpr.Proved (is_opaque,idopt) ->
+  | Vernacexpr.Proved (opaque,idopt) ->
       let (proof_obj,terminator) =
         match proof with
         | None ->
-            Proof_global.close_proof ~keep_body_ucst_separate:false (fun x -> x)
+            Proof_global.close_proof ~opaque ~keep_body_ucst_separate:false (fun x -> x)
         | Some proof -> proof
       in
       (* if the proof is given explicitly, nothing has to be deleted *)
       if Option.is_empty proof then Proof_global.discard_current ();
-      Proof_global.(apply_terminator terminator (Proved (is_opaque,idopt,proof_obj)))
+      Proof_global.(apply_terminator terminator (Proved (opaque,idopt,proof_obj)))
diff --git a/vernac/vernacextend.ml b/vernac/vernacextend.ml
index 3a321ecdb4..23e1223501 100644
--- a/vernac/vernacextend.ml
+++ b/vernac/vernacextend.ml
@@ -12,6 +12,11 @@ open Util
 open Pp
 open CErrors
 
+type vernac_qed_type =
+  | VtKeep of Proof_global.opacity_flag
+  | VtKeepAsAxiom
+  | VtDrop
+
 type vernac_type =
   (* Start of a proof *)
   | VtStartProof of vernac_start
@@ -33,7 +38,6 @@ type vernac_type =
   (* To be removed *)
   | VtMeta
   | VtUnknown
-and vernac_qed_type = VtKeep | VtKeepAsAxiom | VtDrop (* Qed/Admitted, Abort *)
 and vernac_start = string * opacity_guarantee * Names.Id.t list
 and vernac_sideff_type = Names.Id.t list
 and opacity_guarantee =
diff --git a/vernac/vernacextend.mli b/vernac/vernacextend.mli
index 7feaccd9a3..07ba6ee00d 100644
--- a/vernac/vernacextend.mli
+++ b/vernac/vernacextend.mli
@@ -27,6 +27,12 @@
    considered safe to delegate to a worker.
 
 *)
+
+type vernac_qed_type =
+  | VtKeep of Proof_global.opacity_flag (** Defined/Qed *)
+  | VtKeepAsAxiom (** Admitted *)
+  | VtDrop (** Abort *)
+
 type vernac_type =
   (* Start of a proof *)
   | VtStartProof of vernac_start
@@ -48,7 +54,6 @@ type vernac_type =
   (* To be removed *)
   | VtMeta
   | VtUnknown
-and vernac_qed_type = VtKeep | VtKeepAsAxiom | VtDrop (* Qed/Admitted, Abort *)
 and vernac_start = string * opacity_guarantee * Names.Id.t list
 and vernac_sideff_type = Names.Id.t list
 and opacity_guarantee =