Merge PR #10664: Putting sections libstack inside the kernel

Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Ack-by: ejgallego
Reviewed-by: gares
Reviewed-by: maximedenes

16 files changed, 502 insertions, 194 deletions

diff --git a/dev/doc/critical-bugs b/dev/doc/critical-bugs
index d00c8cb11a..78d7061259 100644
--- a/dev/doc/critical-bugs
+++ b/dev/doc/critical-bugs
@@ -129,6 +129,18 @@ Universes
   GH issue number: #9294
   risk: moderate risk to be activated by chance
 
+  component: universe polymorphism, asynchronous proofs
+  summary: universe constraints erroneously discarded when forcing an asynchronous proof containing delayed monomorphic constraints inside a universe polymorphic section
+  introduced: between 8.4 and 8.5 by merging the asynchronous proofs feature branch and universe polymorphism one
+  impacted released: V8.5-V8.10
+  impacted development branches: none
+  impacted coqchk versions: immune
+  fixed in: PR#10664
+  found by: Pédrot
+  exploit: no test
+  GH issue number: none
+  risk: unlikely to be triggered in interactive mode, not present in batch mode (i.e. coqc)
+
 Primitive projections
 
   component: primitive projections, guard condition
diff --git a/doc/changelog/01-kernel/10664-sections-stack-in-kernel.rst b/doc/changelog/01-kernel/10664-sections-stack-in-kernel.rst
new file mode 100644
index 0000000000..bac08d12ea
--- /dev/null
+++ b/doc/changelog/01-kernel/10664-sections-stack-in-kernel.rst
@@ -0,0 +1,6 @@
+- Section data is now part of the kernel. Solves a soundness issue
+  in interactive mode where global monomorphic universe constraints would be
+  dropped when forcing a delayed opaque proof inside a polymorphic section. Also
+  relaxes the nesting criterion for sections, as polymorphic sections can now
+  appear inside a monomorphic one
+  (#10664, <https://github.com/coq/coq/pull/10664> by Pierre-Marie Pédrot).
diff --git a/doc/sphinx/addendum/universe-polymorphism.rst b/doc/sphinx/addendum/universe-polymorphism.rst
index 7e698bfb66..1d0b732e7d 100644
--- a/doc/sphinx/addendum/universe-polymorphism.rst
+++ b/doc/sphinx/addendum/universe-polymorphism.rst
@@ -147,14 +147,7 @@ Many other commands support the ``Polymorphic`` flag, including:
 - :cmd:`Section` will locally set the polymorphism flag inside the section.
 
 - ``Variables``, ``Context``, ``Universe`` and ``Constraint`` in a section support
-  polymorphism. This means that the universe variables (and associated
-  constraints) are discharged polymorphically over definitions that use
-  them. In other words, two definitions in the section sharing a common
-  variable will both get parameterized by the universes produced by the
-  variable declaration. This is in contrast to a “mononorphic” variable
-  which introduces global universes and constraints, making the two
-  definitions depend on the *same* global universes associated to the
-  variable.
+  polymorphism. See :ref:`universe-polymorphism-in-sections` for more details.
 
 - :cmd:`Hint Resolve` and :cmd:`Hint Rewrite` will use the auto/rewrite hint
   polymorphically, not at a single instance.
@@ -375,9 +368,7 @@ to universes and explicitly instantiate polymorphic definitions.
    as well. Global universe names live in a separate namespace. The
    command supports the ``Polymorphic`` flag only in sections, meaning the
    universe quantification will be discharged on each section definition
-   independently. One cannot mix polymorphic and monomorphic
-   declarations in the same section.
-
+   independently.
 
 .. cmd:: Constraint @universe_constraint
          Polymorphic Constraint @universe_constraint
@@ -510,3 +501,23 @@ underscore or by omitting the annotation to a polymorphic definition.
 
       Lemma baz : Type@{outer}. Proof. exact Type@{inner}. Qed.
       About baz.
+
+.. _universe-polymorphism-in-sections:
+
+Universe polymorphism and sections
+----------------------------------
+
+The universe polymorphic or monomorphic status is
+attached to each individual section, and all term or universe declarations
+contained inside must respect it, as described below. It is possible to nest a
+polymorphic section inside a monomorphic one, but the converse is not allowed.
+
+:cmd:`Variables`, :cmd:`Context`, :cmd:`Universe` and :cmd:`Constraint` in a section support
+polymorphism. This means that the universe variables and their associated
+constraints are discharged polymorphically over definitions that use
+them. In other words, two definitions in the section sharing a common
+variable will both get parameterized by the universes produced by the
+variable declaration. This is in contrast to a “mononorphic” variable
+which introduces global universes and constraints, making the two
+definitions depend on the *same* global universes associated to the
+variable.
diff --git a/pretyping/inferCumulativity.ml b/kernel/inferCumulativity.ml
index ed069eace0..3b8c2cd788 100644
--- a/pretyping/inferCumulativity.ml
+++ b/kernel/inferCumulativity.ml
@@ -77,7 +77,7 @@ let infer_sort cv_pb variances s =
   | CUMUL ->
     LSet.fold infer_level_leq (Universe.levels (Sorts.univ_of_sort s)) variances
 
-let infer_table_key infos variances c =
+let infer_table_key variances c =
   let open Names in
   match c with
   | ConstKey (_, u) ->
@@ -103,7 +103,7 @@ let rec infer_fterm cv_pb infos variances hd stk =
   | FRel _ -> infer_stack infos variances stk
   | FInt _ -> infer_stack infos variances stk
   | FFlex fl ->
-    let variances = infer_table_key infos variances fl in
+    let variances = infer_table_key variances fl in
     infer_stack infos variances stk
   | FProj (_,c) ->
     let variances = infer_fterm CONV infos variances c [] in
@@ -152,7 +152,7 @@ and infer_stack infos variances (stk:CClosure.stack) =
       | Zfix (fx,a) ->
         let variances = infer_fterm CONV infos variances fx [] in
         infer_stack infos variances a
-      | ZcaseT (ci,p,br,e) ->
+      | ZcaseT (_, p, br, e) ->
         let variances = infer_fterm CONV infos variances (mk_clos e p) [] in
         infer_vect infos variances (Array.map (mk_clos e) br)
       | Zshift _ -> variances
@@ -195,7 +195,7 @@ let infer_inductive_core env params entries uctx =
     Array.fold_left (fun variances u -> LMap.add u IrrelevantI variances)
       LMap.empty uarray
   in
-  let env, params = Typeops.check_context env params in
+  let env, _ = Typeops.check_context env params in
   let variances = List.fold_left (fun variances entry ->
       let variances = infer_arity_constructor true
           env variances entry.mind_entry_arity
@@ -213,9 +213,8 @@ let infer_inductive_core env params entries uctx =
 
 let infer_inductive env mie =
   let open Entries in
-  let { mind_entry_params = params;
-        mind_entry_inds = entries; } = mie
-  in
+  let params = mie.mind_entry_params in
+  let entries = mie.mind_entry_inds in
   let variances =
     match mie.mind_entry_variance with
     | None -> None
diff --git a/pretyping/inferCumulativity.mli b/kernel/inferCumulativity.mli
index a234e334d1..a234e334d1 100644
--- a/pretyping/inferCumulativity.mli
+++ b/kernel/inferCumulativity.mli
diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib
index 59c1d5890f..20e742d7f8 100644
--- a/kernel/kernel.mllib
+++ b/kernel/kernel.mllib
@@ -43,9 +43,11 @@ Inductive
 Typeops
 IndTyping
 Indtypes
+InferCumulativity
 Cooking
 Term_typing
 Subtyping
 Mod_typing
 Nativelibrary
+Section
 Safe_typing
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 6970a11e72..8d34f3a34f 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -115,6 +115,7 @@ type module_parameters = (MBId.t * module_type_body) list
 
 type safe_environment =
   { env : Environ.env;
+    sections : Section.t;
     modpath : ModPath.t;
     modvariant : modvariant;
     modresolver : Mod_subst.delta_resolver;
@@ -151,6 +152,7 @@ let empty_environment =
     revstruct = [];
     modlabels = Label.Set.empty;
     objlabels = Label.Set.empty;
+    sections = Section.empty;
     future_cst = [];
     univ = Univ.ContextSet.empty;
     engagement = None;
@@ -317,11 +319,16 @@ let universes_of_private eff =
 let env_of_safe_env senv = senv.env
 let env_of_senv = env_of_safe_env
 
+let sections_of_safe_env senv = senv.sections
+
 type constraints_addition =
   | Now of Univ.ContextSet.t
   | Later of Univ.ContextSet.t Future.computation
 
 let push_context_set poly cst senv =
+  let () = if Section.is_polymorphic senv.sections && not (Univ.ContextSet.is_empty cst) then
+    CErrors.user_err (Pp.str "Cannot add global universe constraints inside a polymorphic section.")
+  in
   { senv with
     env = Environ.push_context_set ~strict:(not poly) cst senv.env;
     univ = Univ.ContextSet.union cst senv.univ }
@@ -386,7 +393,7 @@ let check_current_library dir senv = match senv.modvariant with
 (** When operating on modules, we're normally outside sections *)
 
 let check_empty_context senv =
-  assert (Environ.empty_context senv.env)
+  assert (Environ.empty_context senv.env && Section.is_empty senv.sections)
 
 (** When adding a parameter to the current module/modtype,
     it must have been freshly started *)
@@ -433,19 +440,30 @@ let safe_push_named d env =
     with Not_found -> () in
   Environ.push_named d env
 
-
 let push_named_def (id,de) senv =
+  let sections = Section.push_local senv.sections in
   let c, r, typ = Term_typing.translate_local_def senv.env id de in
   let x = Context.make_annot id r in
   let env'' = safe_push_named (LocalDef (x, c, typ)) senv.env in
-  { senv with env = env'' }
+  { senv with sections; env = env'' }
 
 let push_named_assum (x,t) senv =
+  let sections = Section.push_local senv.sections in
   let t, r = Term_typing.translate_local_assum senv.env t in
   let x = Context.make_annot x r in
   let env'' = safe_push_named (LocalAssum (x,t)) senv.env in
-    {senv with env=env''}
-
+  { senv with sections; env = env'' }
+
+let push_section_context (nas, ctx) senv =
+  let sections = Section.push_context (nas, ctx) senv.sections in
+  let senv = { senv with sections } in
+  let ctx = Univ.ContextSet.of_context ctx in
+  (* We check that the universes are fresh. FIXME: This should be done
+     implicitly, but we have to work around the API. *)
+  let () = assert (Univ.LSet.for_all (fun u -> not (Univ.LSet.mem u (fst senv.univ))) (fst ctx)) in
+  { senv with
+    env = Environ.push_context_set ~strict:false ctx senv.env;
+    univ = Univ.ContextSet.union ctx senv.univ }
 
 (** {6 Insertion of new declarations to current environment } *)
 
@@ -527,8 +545,19 @@ let add_field ?(is_include=false) ((l,sfb) as field) gn senv =
     | SFBmodule mb, M -> Modops.add_module mb senv.env
     | _ -> assert false
   in
+  let sections = match sfb, gn with
+  | SFBconst cb, C con ->
+    let poly = Declareops.constant_is_polymorphic cb in
+    Section.push_constant ~poly con senv.sections
+  | SFBmind mib, I mind ->
+    let poly = Declareops.inductive_is_polymorphic mib in
+    Section.push_inductive ~poly mind senv.sections
+  | _, (M | MT) -> senv.sections
+  | _ -> assert false
+  in
   { senv with
     env = env';
+    sections;
     revstruct = field :: senv.revstruct;
     modlabels = Label.Set.union mlabs senv.modlabels;
     objlabels = Label.Set.union olabs senv.objlabels }
@@ -902,6 +931,16 @@ let add_module l me inl senv =
   in
   (mp,mb.mod_delta),senv''
 
+(** {6 Interactive sections *)
+
+let open_section ~poly senv =
+  let sections = Section.open_section ~poly senv.sections in
+  { senv with sections }
+
+let close_section senv =
+  (* TODO: implement me when discharging in kernel *)
+  let sections = Section.close_section senv.sections in
+  { senv with sections }
 
 (** {6 Starting / ending interactive modules and module types } *)
 
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index fa53fa33fa..10fedc2faf 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -33,6 +33,8 @@ val is_initial : safe_environment -> bool
 
 val env_of_safe_env : safe_environment -> Environ.env
 
+val sections_of_safe_env : safe_environment -> Section.t
+
 (** The safe_environment state monad *)
 
 type safe_transformer0 = safe_environment -> safe_environment
@@ -67,15 +69,6 @@ val join_safe_environment :
 val is_joined_environment : safe_environment -> bool
 (** {6 Enriching a safe environment } *)
 
-(** Insertion of local declarations (Local or Variables) *)
-
-val push_named_assum : (Id.t * Constr.types) -> safe_transformer0
-
-(** Returns the full universe context necessary to typecheck the definition
-  (futures are forced) *)
-val push_named_def :
-  Id.t * Entries.section_def_entry -> safe_transformer0
-
 (** Insertion of global axioms or definitions *)
 
 type 'a effect_entry =
@@ -140,6 +133,22 @@ val set_allow_sprop : bool -> safe_transformer0
 
 val check_engagement : Environ.env -> Declarations.set_predicativity -> unit
 
+(** {6 Interactive section functions } *)
+
+val open_section : poly:bool -> safe_transformer0
+
+val close_section : safe_transformer0
+
+(** Insertion of local declarations (Local or Variables) *)
+
+val push_named_assum : (Id.t * Constr.types) -> safe_transformer0
+
+val push_named_def :
+  Id.t * Entries.section_def_entry -> safe_transformer0
+
+(** Add local universes to a polymorphic section *)
+val push_section_context : (Name.t array * Univ.UContext.t) -> safe_transformer0
+
 (** {6 Interactive module functions } *)
 
 val start_module : Label.t -> ModPath.t safe_transformer
diff --git a/kernel/section.ml b/kernel/section.ml
new file mode 100644
index 0000000000..12e9c2fd60
--- /dev/null
+++ b/kernel/section.ml
@@ -0,0 +1,250 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+open Util
+open Names
+open Univ
+
+module NamedDecl = Context.Named.Declaration
+
+type _ section_kind =
+| SecMono : [ `mono ] section_kind
+| SecPoly : [ `poly ] section_kind
+
+type _ section_universes =
+| SecMonoUniv : [ `mono ] section_universes
+| SecPolyUniv : Name.t array * UContext.t -> [ `poly ] section_universes
+
+type section_entry =
+| SecDefinition of Constant.t
+| SecInductive of MutInd.t
+
+type 'a entry_map = 'a Cmap.t * 'a Mindmap.t
+
+type 'a section = {
+  sec_context : int;
+  (** Length of the named context suffix that has been introduced locally *)
+  sec_universes : 'a section_universes;
+  (** Universes local to the section *)
+  sec_entries : section_entry list;
+  (** Definitions introduced in the section *)
+  sec_data : 'a section_universes entry_map;
+}
+
+(** Sections can be nested with the proviso that no monomorphic section can be
+    opened inside a polymorphic one. The reverse is allowed. *)
+type t = {
+  sec_poly : [ `poly ] section list;
+  sec_mono : [ `mono ] section list;
+}
+
+let empty = {
+  sec_poly = [];
+  sec_mono = [];
+}
+
+let is_empty s =
+  List.is_empty s.sec_poly && List.is_empty s.sec_mono
+
+let is_polymorphic s =
+  not (List.is_empty s.sec_poly)
+
+let find_emap e (cmap, imap) = match e with
+| SecDefinition con -> Cmap.find con cmap
+| SecInductive ind -> Mindmap.find ind imap
+
+let add_emap e v (cmap, imap) = match e with
+| SecDefinition con -> (Cmap.add con v cmap, imap)
+| SecInductive ind -> (cmap, Mindmap.add ind v imap)
+
+type on_sec = { on_sec : 'a. 'a section_kind -> 'a section -> 'a section }
+
+let on_last_section f { sec_poly; sec_mono } = match sec_poly, sec_mono with
+| [], [] -> CErrors.user_err (Pp.str "No opened section")
+| sec :: rem, _ ->
+  let sec_poly = f.on_sec SecPoly sec :: rem in
+  { sec_mono; sec_poly }
+| [], sec :: rem ->
+  let sec_mono = f.on_sec SecMono sec :: rem in
+  { sec_mono; sec_poly }
+
+type 'r with_sec = { with_sec : 'a. ('a section_kind * 'a section) option -> 'r }
+
+let with_last_section f { sec_poly; sec_mono } = match sec_poly, sec_mono with
+| [], [] -> f.with_sec None
+| sec :: _, _ -> f.with_sec (Some (SecPoly, sec))
+| [], sec :: _ -> f.with_sec (Some (SecMono, sec))
+
+let push_local s =
+  let on_sec _ sec = { sec with sec_context = sec.sec_context + 1 } in
+  on_last_section { on_sec } s
+
+let push_context (nas, ctx) s =
+  let on_sec (type a) (kind : a section_kind) (sec : a section) : a section = match kind with
+  | SecMono ->
+    CErrors.anomaly (Pp.str "Adding polymorphic constraints to monomorphic section")
+  | SecPoly ->
+    let SecPolyUniv (snas, sctx) = sec.sec_universes in
+    let sec_universes = SecPolyUniv (Array.append snas nas, UContext.union sctx ctx) in
+    { sec with sec_universes }
+  in
+  on_last_section { on_sec } s
+
+let open_section ~poly sections =
+  if poly then
+    let sec = {
+      sec_context = 0;
+      sec_universes = SecPolyUniv ([||], Univ.UContext.empty);
+      sec_entries = [];
+      sec_data = (Cmap.empty, Mindmap.empty);
+    } in
+    { sections with sec_poly = sec :: sections.sec_poly }
+  else if List.is_empty sections.sec_poly then
+    let sec = {
+      sec_context = 0;
+      sec_universes = SecMonoUniv;
+      sec_entries = [];
+      sec_data = (Cmap.empty, Mindmap.empty);
+    } in
+    { sections with sec_mono = sec :: sections.sec_mono }
+  else
+    CErrors.user_err (Pp.str "Cannot open a monomorphic section inside a polymorphic one")
+
+let close_section sections =
+  (* TODO: implement me correctly when discharging in kernel *)
+  match sections.sec_poly, sections.sec_mono with
+  | _sec :: psecs, _ ->
+    let sections = { sections with sec_poly = psecs } in
+    sections
+  | [], _sec :: msecs ->
+    let sections = { sections with sec_mono = msecs } in
+    sections
+  | [], [] ->
+    CErrors.user_err (Pp.str "No opened section.")
+
+let same_poly (type a) ~poly (knd : a section_kind) = match knd with
+| SecPoly -> poly
+| SecMono -> not poly
+
+let push_global ~poly e s =
+  if is_empty s then s
+  else
+    let on_sec knd sec =
+      if same_poly ~poly knd then { sec with
+        sec_entries = e :: sec.sec_entries;
+        sec_data = add_emap e sec.sec_universes sec.sec_data;
+      } else
+        CErrors.user_err (Pp.str "Cannot mix universe polymorphic and \
+          monomorphic declarations in sections.")
+    in
+    on_last_section { on_sec } s
+
+let push_constant ~poly con s = push_global ~poly (SecDefinition con) s
+
+let push_inductive ~poly ind s = push_global ~poly (SecInductive ind) s
+
+type abstr_info = {
+  abstr_ctx : Constr.named_context;
+  abstr_subst : Univ.Instance.t;
+  abstr_uctx : Univ.AUContext.t;
+}
+
+let empty_segment = {
+  abstr_ctx = [];
+  abstr_subst = Instance.empty;
+  abstr_uctx = AUContext.empty;
+}
+
+let extract_hyps sec vars hyps =
+  (* FIXME: this code is fishy. It is supposed to check that declared section
+     variables are an ordered subset of the ambient ones, but it doesn't check
+     e.g. uniqueness of naming nor convertibility of the section data. *)
+  let rec aux ids hyps = match ids, hyps with
+  | id :: ids, decl :: hyps when Names.Id.equal id (NamedDecl.get_id decl) ->
+    decl :: aux ids hyps
+  | _ :: ids, hyps ->
+    aux ids hyps
+  | [], _ -> []
+  in
+  let ids = List.map NamedDecl.get_id @@ List.firstn sec.sec_context vars in
+  aux ids hyps
+
+let section_segment_of_entry vars e hyps sections =
+  (* [vars] are the named hypotheses, [hyps] the subset that is declared by the
+    global *)
+  let with_sec (type a) (s : (a section_kind * a section) option) = match s with
+  | None ->
+    CErrors.user_err (Pp.str "No opened section.")
+  | Some (knd, sec) ->
+    let hyps = extract_hyps sec vars hyps in
+    let inst, auctx = match knd, find_emap e sec.sec_data with
+    | SecMono, SecMonoUniv ->
+      Instance.empty, AUContext.empty
+    | SecPoly, SecPolyUniv (nas, ctx) ->
+      Univ.abstract_universes nas ctx
+    in
+    {
+      abstr_ctx = hyps;
+      abstr_subst = inst;
+      abstr_uctx = auctx;
+    }
+  in
+  with_last_section { with_sec } sections
+
+let segment_of_constant env con s =
+  let body = Environ.lookup_constant con env in
+  let vars = Environ.named_context env in
+  section_segment_of_entry vars (SecDefinition con) body.Declarations.const_hyps s
+
+let segment_of_inductive env mind s =
+  let mib = Environ.lookup_mind mind env in
+  let vars = Environ.named_context env in
+  section_segment_of_entry vars (SecInductive mind) mib.Declarations.mind_hyps s
+
+let instance_from_variable_context =
+  List.rev %> List.filter NamedDecl.is_local_assum %> List.map NamedDecl.get_id %> Array.of_list
+
+let extract_worklist info =
+  let args = instance_from_variable_context info.abstr_ctx in
+  info.abstr_subst, args
+
+let replacement_context env s =
+  let with_sec sec = match sec with
+  | None -> CErrors.user_err (Pp.str "No opened section.")
+  | Some (_, sec) ->
+    let cmap, imap = sec.sec_data in
+    let cmap = Cmap.mapi (fun con _ -> extract_worklist @@ segment_of_constant env con s) cmap in
+    let imap = Mindmap.mapi (fun ind _ -> extract_worklist @@ segment_of_inductive env ind s) imap in
+    (cmap, imap)
+  in
+  with_last_section { with_sec } s
+
+let is_in_section env gr s =
+  let with_sec sec = match sec with
+  | None -> false
+  | Some (_, sec) ->
+    let open GlobRef in
+    match gr with
+    | VarRef id ->
+      let vars = List.firstn sec.sec_context (Environ.named_context env) in
+      List.exists (fun decl -> Id.equal id (NamedDecl.get_id decl)) vars
+    | ConstRef con ->
+      Cmap.mem con (fst sec.sec_data)
+    | IndRef (ind, _) | ConstructRef ((ind, _), _) ->
+      Mindmap.mem ind (snd sec.sec_data)
+  in
+  with_last_section { with_sec } s
+
+let is_polymorphic_univ u s =
+  let check sec =
+    let SecPolyUniv (_, uctx) = sec.sec_universes in
+    Array.mem u (Instance.to_array (UContext.instance uctx))
+  in
+  List.exists check s.sec_poly
diff --git a/kernel/section.mli b/kernel/section.mli
new file mode 100644
index 0000000000..4b23115ca2
--- /dev/null
+++ b/kernel/section.mli
@@ -0,0 +1,78 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+open Names
+open Univ
+
+(** Kernel implementation of sections. *)
+
+type t
+(** Type of sections *)
+
+val empty : t
+
+val is_empty : t -> bool
+(** Checks whether there is no opened section *)
+
+val is_polymorphic : t -> bool
+(** Checks whether last opened section is polymorphic *)
+
+(** {6 Manipulating sections} *)
+
+val open_section : poly:bool -> t -> t
+(** Open a new section with the provided universe polymorphic status. Sections
+    can be nested, with the proviso that polymorphic sections cannot appear
+    inside a monomorphic one. *)
+
+val close_section : t -> t
+
+(** {6 Extending sections} *)
+
+val push_local : t -> t
+(** Extend the current section with a local definition (cf. push_named). *)
+
+val push_context : Name.t array * UContext.t -> t -> t
+(** Extend the current section with a local universe context. Assumes that the
+    last opened section is polymorphic. *)
+
+val push_constant : poly:bool -> Constant.t -> t -> t
+(** Make the constant as having been defined in this section. *)
+
+val push_inductive : poly:bool -> MutInd.t -> t -> t
+(** Make the inductive block as having been defined in this section. *)
+
+(** {6 Retrieving section data} *)
+
+type abstr_info = private {
+  abstr_ctx : Constr.named_context;
+  (** Section variables of this prefix *)
+  abstr_subst : Univ.Instance.t;
+  (** Actual names of the abstracted variables *)
+  abstr_uctx : Univ.AUContext.t;
+  (** Universe quantification, same length as the substitution *)
+}
+(** Data needed to abstract over the section variable and universe hypotheses *)
+
+
+val empty_segment : abstr_info
+(** Nothing to abstract *)
+
+val segment_of_constant : Environ.env -> Constant.t -> t -> abstr_info
+(** Section segment at the time of the constant declaration *)
+
+val segment_of_inductive : Environ.env -> MutInd.t -> t -> abstr_info
+(** Section segment at the time of the inductive declaration *)
+
+val replacement_context : Environ.env -> t -> Opaqueproof.work_list
+(** Section segments of all declarations from this section. *)
+
+val is_in_section : Environ.env -> GlobRef.t -> t -> bool
+
+val is_polymorphic_univ : Level.t -> t -> bool
diff --git a/library/global.ml b/library/global.ml
index 6bb4614aa4..3d28178d7b 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -83,6 +83,7 @@ let i2l = Label.of_id
 
 let push_named_assum a = globalize0 (Safe_typing.push_named_assum a)
 let push_named_def d = globalize0 (Safe_typing.push_named_def d)
+let push_section_context c = globalize0 (Safe_typing.push_section_context c)
 let add_constraints c = globalize0 (Safe_typing.add_constraints c)
 let push_context_set b c = globalize0 (Safe_typing.push_context_set b c)
 
@@ -104,6 +105,13 @@ let add_modtype id me inl = globalize (Safe_typing.add_modtype (i2l id) me inl)
 let add_module id me inl = globalize (Safe_typing.add_module (i2l id) me inl)
 let add_include me ismod inl = globalize (Safe_typing.add_include me ismod inl)
 
+let open_section ~poly = globalize0 (Safe_typing.open_section ~poly)
+let close_section fs =
+  (* TODO: use globalize0_with_summary *)
+  Summary.unfreeze_summaries fs;
+  let env = Safe_typing.close_section (safe_env ()) in
+  GlobalSafeEnv.set_safe_env env
+
 let start_module id = globalize (Safe_typing.start_module (i2l id))
 let start_modtype id = globalize (Safe_typing.start_modtype (i2l id))
 
diff --git a/library/global.mli b/library/global.mli
index d0bd556d70..b809e9b241 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -44,6 +44,7 @@ val sprop_allowed : unit -> bool
 
 val push_named_assum : (Id.t * Constr.types) -> unit
 val push_named_def   : (Id.t * Entries.section_def_entry) -> unit
+val push_section_context : (Name.t array * Univ.UContext.t) -> unit
 
 val export_private_constants : in_section:bool ->
   Safe_typing.private_constants Entries.proof_output ->
@@ -71,6 +72,15 @@ val add_include :
   Entries.module_struct_entry -> bool -> Declarations.inline ->
     Mod_subst.delta_resolver
 
+(** Sections *)
+
+val open_section : poly:bool -> unit
+(** [poly] is true when the section should be universe polymorphic *)
+
+val close_section : Summary.frozen -> unit
+(** Close the section and reset the global state to the one at the time when
+    the section what opened. *)
+
 (** Interactive modules and module types *)
 
 val start_module : Id.t -> ModPath.t
diff --git a/library/lib.ml b/library/lib.ml
index 851f086961..1c6f82e8a6 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -410,87 +410,11 @@ let find_opening_node id =
    - the list of substitution to do at section closing
 *)
 
-type abstr_info = {
+type abstr_info = Section.abstr_info = private {
   abstr_ctx : Constr.named_context;
   abstr_subst : Univ.Instance.t;
   abstr_uctx : Univ.AUContext.t;
 }
-type abstr_list = abstr_info Names.Cmap.t * abstr_info Names.Mindmap.t
-
-type secentry =
-  | Variable of {
-      id:Names.Id.t;
-    }
-  | Context of Univ.ContextSet.t
-
-type section_data = {
-  sec_entry : secentry list;
-  sec_abstr : abstr_list;
-  sec_poly  : bool;
-}
-
-let empty_section_data ~poly = {
-  sec_entry = [];
-  sec_abstr = (Names.Cmap.empty,Names.Mindmap.empty);
-  sec_poly  = poly;
-}
-
-let sectab =
-  Summary.ref ([] : section_data list) ~name:"section-context"
-
-let check_same_poly p sec =
-  if p != sec.sec_poly then
-    user_err Pp.(str  "Cannot mix universe polymorphic and monomorphic declarations in sections.")
-
-let add_section ~poly () =
-  List.iter (fun tab -> check_same_poly poly tab) !sectab;
-  sectab := empty_section_data ~poly :: !sectab
-
-let add_section_variable ~name ~poly =
-  match !sectab with
-    | [] -> () (* because (Co-)Fixpoint temporarily uses local vars *)
-    | s :: sl ->
-       List.iter (fun tab -> check_same_poly poly tab) !sectab;
-       let s = { s with sec_entry = Variable {id=name} :: s.sec_entry } in
-       sectab := s :: sl
-
-let add_section_context ctx =
-  match !sectab with
-    | [] -> () (* because (Co-)Fixpoint temporarily uses local vars *)
-    | s :: sl ->
-       check_same_poly true s;
-       let s = { s with sec_entry = Context ctx :: s.sec_entry } in
-       sectab := s :: sl
-
-exception PolyFound (* make this a let exception once possible *)
-let is_polymorphic_univ u =
-  try
-    let open Univ in
-    List.iter (fun s ->
-      let vars = s.sec_entry in
-        List.iter (function
-            | Variable _ -> ()
-            | Context (univs,_) ->
-              if LSet.mem u univs then raise PolyFound
-          ) vars
-      ) !sectab;
-    false
-  with PolyFound -> true
-
-let extract_hyps poly (secs,ohyps) =
-  let rec aux = function
-    | (Variable {id}::idl, decl::hyps) when Names.Id.equal id (NamedDecl.get_id decl) ->
-      let l, r = aux (idl,hyps) in 
-      decl :: l, r
-    | (Variable _::idl,hyps) ->
-        let l, r = aux (idl,hyps) in
-          l, r
-    | (Context ctx :: idl, hyps) ->
-      let () = assert poly in
-       let l, r = aux (idl, hyps) in
-       l, Univ.ContextSet.union r ctx
-    | [], _ -> [],Univ.ContextSet.empty
-  in aux (secs,ohyps)
 
 let instance_from_variable_context =
   List.rev %> List.filter is_local_assum %> List.map NamedDecl.get_id %> Array.of_list
@@ -499,66 +423,21 @@ let extract_worklist info =
   let args = instance_from_variable_context info.abstr_ctx in
   info.abstr_subst, args
 
-let make_worklist (cmap, mmap) =
-  Cmap.map extract_worklist cmap, Mindmap.map extract_worklist mmap
-
-let name_instance inst =
-  (* FIXME: this should probably be done at an upper level, by storing the
-     name information in the section data structure. *)
-  let map lvl = match Univ.Level.name lvl with
-    | None -> (* Having Prop/Set/Var as section universes makes no sense *)
-      assert false
-    | Some na ->
-      try
-        let qid = Nametab.shortest_qualid_of_universe na in
-        Name (Libnames.qualid_basename qid)
-      with Not_found ->
-        (* Best-effort naming from the string representation of the level.
-           See univNames.ml for a similar hack. *)
-        Name (Id.of_string_soft (Univ.Level.to_string lvl))
-  in
-  Array.map map (Univ.Instance.to_array inst)
-
-let add_section_replacement g poly hyps =
-  match !sectab with
-  | [] -> ()
-  | s :: sl ->
-    let () = check_same_poly poly s in
-    let sechyps,ctx = extract_hyps s.sec_poly (s.sec_entry, hyps) in
-    let ctx = Univ.ContextSet.to_context ctx in
-    let nas = name_instance (Univ.UContext.instance ctx) in
-    let subst, ctx = Univ.abstract_universes nas ctx in
-    let info = {
-      abstr_ctx = sechyps;
-      abstr_subst = subst;
-      abstr_uctx = ctx;
-    } in
-    let s = { s with
-      sec_abstr = g info s.sec_abstr;
-    } in
-    sectab := s :: sl
-
-let add_section_kn ~poly kn =
-  let f x (l1,l2) = (l1,Names.Mindmap.add kn x l2) in
-    add_section_replacement f poly
-
-let add_section_constant ~poly kn =
-  let f x (l1,l2) = (Names.Cmap.add kn x l1,l2) in
-    add_section_replacement f poly
-
-let replacement_context () = make_worklist (List.hd !sectab).sec_abstr
+let sections () = Safe_typing.sections_of_safe_env @@ Global.safe_env ()
+
+let is_polymorphic_univ u =
+  Section.is_polymorphic_univ u (sections ())
+
+let replacement_context () =
+  Section.replacement_context (Global.env ()) (sections ())
 
 let section_segment_of_constant con =
-  Names.Cmap.find con (fst (List.hd !sectab).sec_abstr)
+  Section.segment_of_constant (Global.env ()) con (sections ())
 
 let section_segment_of_mutual_inductive kn =
-  Names.Mindmap.find kn (snd (List.hd !sectab).sec_abstr)
+  Section.segment_of_inductive (Global.env ()) kn (sections ())
 
-let empty_segment = {
-  abstr_ctx = [];
-  abstr_subst = Univ.Instance.empty;
-  abstr_uctx = Univ.AUContext.empty;
-}
+let empty_segment = Section.empty_segment
 
 let section_segment_of_reference = let open GlobRef in function
 | ConstRef c -> section_segment_of_constant c
@@ -569,28 +448,24 @@ let section_segment_of_reference = let open GlobRef in function
 let variable_section_segment_of_reference gr =
   (section_segment_of_reference gr).abstr_ctx
 
+let is_in_section ref =
+  Section.is_in_section (Global.env ()) ref (sections ())
+
 let section_instance = let open GlobRef in function
   | VarRef id ->
-     let eq = function
-       | Variable {id=id'} -> Names.Id.equal id id'
-       | Context _ -> false
-     in
-     if List.exists eq (List.hd !sectab).sec_entry
-     then Univ.Instance.empty, [||]
-     else raise Not_found
+    if is_in_section (VarRef id) then (Univ.Instance.empty, [||])
+    else raise Not_found
   | ConstRef con ->
-    let data = Names.Cmap.find con (fst (List.hd !sectab).sec_abstr) in
+    let data = section_segment_of_constant con in
     extract_worklist data
   | IndRef (kn,_) | ConstructRef ((kn,_),_) ->
-    let data = Names.Mindmap.find kn (snd (List.hd !sectab).sec_abstr) in
+    let data = section_segment_of_mutual_inductive kn in
     extract_worklist data
 
-let is_in_section ref =
-  try ignore (section_instance ref); true with Not_found -> false
-
 (*************)
 (* Sections. *)
 let open_section ~poly id =
+  let () = Global.open_section ~poly in
   let opp = !lib_state.path_prefix in
   let obj_dir = add_dirpath_suffix opp.Nametab.obj_dir id in
   let prefix = Nametab.{ obj_dir; obj_mp = opp.obj_mp; obj_sec = add_dirpath_suffix opp.obj_sec id } in
@@ -600,9 +475,7 @@ let open_section ~poly id =
   add_entry (make_foname id) (OpenedSection (prefix, fs));
   (*Pushed for the lifetime of the section: removed by unfrozing the summary*)
   Nametab.(push_dir (Until 1) obj_dir (GlobDirRef.DirOpenSection prefix));
-  lib_state := { !lib_state with path_prefix = prefix };
-  add_section ~poly ()
-
+  lib_state := { !lib_state with path_prefix = prefix }
 
 (* Restore lib_stk and summaries as before the section opening, and
    add a ClosedSection object. *)
@@ -631,7 +504,7 @@ let close_section () =
   lib_state := { !lib_state with lib_stk = before };
   pop_path_prefix ();
   let newdecls = List.map discharge_item secdecls in
-  Summary.unfreeze_summaries fs;
+  let () = Global.close_section fs in
   List.iter (Option.iter (fun (id,o) -> add_discharged_leaf id o)) newdecls
 
 (* State and initialization. *)
diff --git a/library/lib.mli b/library/lib.mli
index 9ffa69ef93..5ce601f2d3 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -163,7 +163,7 @@ val drop_objects : frozen -> frozen
 val init : unit -> unit
 
 (** {6 Section management for discharge } *)
-type abstr_info = private {
+type abstr_info = Section.abstr_info = private {
   abstr_ctx : Constr.named_context;
   (** Section variables of this prefix *)
   abstr_subst : Univ.Instance.t;
@@ -181,10 +181,6 @@ val variable_section_segment_of_reference : GlobRef.t -> Constr.named_context
 val section_instance : GlobRef.t -> Univ.Instance.t * Id.t array
 val is_in_section : GlobRef.t -> bool
 
-val add_section_variable : name:Id.t -> poly:bool -> unit
-val add_section_context : Univ.ContextSet.t -> unit
-val add_section_constant : poly:bool -> Constant.t -> Constr.named_context -> unit
-val add_section_kn : poly:bool -> MutInd.t -> Constr.named_context -> unit
 val replacement_context : unit -> Opaqueproof.work_list
 
 val is_polymorphic_univ : Univ.Level.t -> bool
diff --git a/pretyping/pretyping.mllib b/pretyping/pretyping.mllib
index 0ca39f0404..7e140f4399 100644
--- a/pretyping/pretyping.mllib
+++ b/pretyping/pretyping.mllib
@@ -4,7 +4,6 @@ Locusops
 Pretype_errors
 Reductionops
 Inductiveops
-InferCumulativity
 Arguments_renaming
 Retyping
 Vnorm
diff --git a/tactics/declare.ml b/tactics/declare.ml
index 3a02e5451a..208b8e28a7 100644
--- a/tactics/declare.ml
+++ b/tactics/declare.ml
@@ -40,9 +40,30 @@ let input_universe_context : Univ.ContextSet.t -> Libobject.obj =
     ~cache:(fun (na, uctx) -> Global.push_context_set false uctx)
     ~discharge:(fun (_, x) -> Some x)
 
+let name_instance inst =
+  let map lvl = match Univ.Level.name lvl with
+    | None -> (* Having Prop/Set/Var as section universes makes no sense *)
+      assert false
+    | Some na ->
+      try
+        let qid = Nametab.shortest_qualid_of_universe na in
+        Name (Libnames.qualid_basename qid)
+      with Not_found ->
+        (* Best-effort naming from the string representation of the level.
+           See univNames.ml for a similar hack. *)
+        Name (Id.of_string_soft (Univ.Level.to_string lvl))
+  in
+  Array.map map (Univ.Instance.to_array inst)
+
 let declare_universe_context ~poly ctx =
   if poly then
-    (Global.push_context_set true ctx; Lib.add_section_context ctx)
+    (* FIXME: some upper layers declare universes several times, we hack around
+      by checking whether the universes already exist. *)
+    let (univs, cstr) = ctx in
+    let univs = Univ.LSet.filter (fun u -> not (Lib.is_polymorphic_univ u)) univs in
+    let uctx = Univ.ContextSet.to_context (univs, cstr) in
+    let nas = name_instance (Univ.UContext.instance uctx) in
+    Global.push_section_context (nas, uctx)
   else
     Lib.add_anonymous_leaf (input_universe_context ctx)
 
@@ -118,8 +139,6 @@ let cache_constant ((sp,kn), obj) =
   in
   assert (Constant.equal kn' (Constant.make1 kn));
   Nametab.push (Nametab.Until 1) sp (GlobRef.ConstRef (Constant.make1 kn));
-  let cst = Global.lookup_constant kn' in
-  add_section_constant ~poly:(Declareops.constant_is_polymorphic cst) kn' cst.const_hyps;
   Dumpglob.add_constant_kind (Constant.make1 kn) obj.cst_kind
 
 let discharge_constant ((sp, kn), obj) =
@@ -352,7 +371,6 @@ let declare_variable ~name ~kind d =
       poly
   in
   Nametab.push (Nametab.Until 1) (Libnames.make_path DirPath.empty name) (GlobRef.VarRef name);
-  add_section_variable ~name ~poly;
   Decls.(add_variable_data name {opaque;kind});
   add_anonymous_leaf (inVariable ());
   Impargs.declare_var_implicits ~impl name;
@@ -401,8 +419,6 @@ let cache_inductive ((sp,kn),mie) =
   let id = Libnames.basename sp in
   let kn' = Global.add_mind id mie in
   assert (MutInd.equal kn' (MutInd.make1 kn));
-  let mind = Global.lookup_mind kn' in
-  add_section_kn ~poly:(Declareops.inductive_is_polymorphic mind) kn' mind.mind_hyps;
   List.iter (fun (sp, ref) -> Nametab.push (Nametab.Until 1) sp ref) names
 
 let discharge_inductive ((sp,kn),mie) =
@@ -632,9 +648,9 @@ let do_universe ~poly l =
   let ctx = List.fold_left (fun ctx (_,qid) -> Univ.LSet.add (Univ.Level.make qid) ctx)
       Univ.LSet.empty l, Univ.Constraint.empty
   in
-  let () = declare_universe_context ~poly ctx in
   let src = if poly then BoundUniv else UnqualifiedUniv in
-  Lib.add_anonymous_leaf (input_univ_names (src, l))
+  let () = Lib.add_anonymous_leaf (input_univ_names (src, l)) in
+  declare_universe_context ~poly ctx
 
 let do_constraint ~poly l =
   let open Univ in