From c73fa639eb0a8eaf4e5121aa600f88f2d4349a0c Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 13 Dec 2017 10:42:41 +0100
Subject: Using a dedicated type for Lib.abstr_info.

---
 interp/declare.ml               |  5 +++--
 interp/discharge.ml             |  4 ++--
 interp/impargs.ml               |  2 +-
 library/lib.ml                  | 38 +++++++++++++++++++++++++++-----------
 library/lib.mli                 | 11 ++++++++++-
 pretyping/arguments_renaming.ml |  8 +-------
 pretyping/reductionops.ml       |  6 +++---
 pretyping/typeclasses.ml        |  3 ++-
 8 files changed, 49 insertions(+), 28 deletions(-)

diff --git a/interp/declare.ml b/interp/declare.ml
index d1b79ffcdd..55f825c251 100644
--- a/interp/declare.ml
+++ b/interp/declare.ml
@@ -104,7 +104,7 @@ let discharge_constant ((sp, kn), obj) =
   let con = Constant.make1 kn in
   let from = Global.lookup_constant con in
   let modlist = replacement_context () in
-  let hyps,subst,uctx = section_segment_of_constant con in
+  let { abstr_ctx = hyps; abstr_subst = subst; abstr_uctx = uctx } = section_segment_of_constant con in
   let new_hyps = (discharged_hyps kn hyps) @ obj.cst_hyps in
   let abstract = (named_of_variable_context hyps, subst, uctx) in
   let new_decl = GlobalRecipe{ from; info = { Opaqueproof.modlist; abstract}} in
@@ -333,7 +333,8 @@ let discharge_inductive ((sp,kn),(dhyps,mie)) =
   let mind = Global.mind_of_delta_kn kn in
   let mie = Global.lookup_mind mind in
   let repl = replacement_context () in
-  let sechyps, _, _ as info = section_segment_of_mutual_inductive mind in
+  let info = section_segment_of_mutual_inductive mind in
+  let sechyps = info.Lib.abstr_ctx in
   Some (discharged_hyps kn sechyps,
         Discharge.process_inductive info repl mie)
 
diff --git a/interp/discharge.ml b/interp/discharge.ml
index 5b4b5f67b8..75bfca3078 100644
--- a/interp/discharge.ml
+++ b/interp/discharge.ml
@@ -78,8 +78,8 @@ let refresh_polymorphic_type_of_inductive (_,mip) =
     let ctx = List.rev mip.mind_arity_ctxt in
       mkArity (List.rev ctx, Type ar.template_level), true
 
-let process_inductive (section_decls,_,_ as info) modlist mib =
-  let section_decls = Lib.named_of_variable_context section_decls in
+let process_inductive info modlist mib =
+  let section_decls = Lib.named_of_variable_context info.Lib.abstr_ctx in
   let nparamdecls = Context.Rel.length mib.mind_params_ctxt in
   let subst, ind_univs =
     match mib.mind_universes with
diff --git a/interp/impargs.ml b/interp/impargs.ml
index 3105214d5e..ed1cd5276c 100644
--- a/interp/impargs.ml
+++ b/interp/impargs.ml
@@ -548,7 +548,7 @@ let discharge_implicits (_,(req,l)) =
   | ImplConstant (con,flags) ->
     (try
       let con' = pop_con con in
-      let vars,_,_ = section_segment_of_constant con in
+      let vars = variable_section_segment_of_reference (ConstRef con) in
       let extra_impls = impls_of_context vars in
       let newimpls = List.map (add_section_impls vars extra_impls) (snd (List.hd l)) in
       let l' = [ConstRef con',newimpls] in
diff --git a/library/lib.ml b/library/lib.ml
index 499e2ae21f..16dd7fdd01 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -417,8 +417,11 @@ let find_opening_node id =
 type variable_info = Context.Named.Declaration.t * Decl_kinds.binding_kind
 
 type variable_context = variable_info list
-type abstr_info = variable_context * Univ.universe_level_subst * Univ.AUContext.t
-		  
+type abstr_info = {
+  abstr_ctx : variable_context;
+  abstr_subst : Univ.universe_level_subst;
+  abstr_uctx : Univ.AUContext.t;
+}
 type abstr_list = abstr_info Names.Cmap.t * abstr_info Names.Mindmap.t
 
 type secentry =
@@ -483,8 +486,12 @@ let add_section_replacement f g poly hyps =
     let inst = Univ.UContext.instance ctx in
     let subst, ctx = Univ.abstract_universes ctx in
     let args = instance_from_variable_context (List.rev sechyps) in
-    sectab := (vars,f (inst,args) exps,
-	      g (sechyps,subst,ctx) abs)::sl
+    let info = {
+      abstr_ctx = sechyps;
+      abstr_subst = subst;
+      abstr_uctx = ctx;
+    } in
+    sectab := (vars,f (inst,args) exps, g info abs) :: sl
 
 let add_section_kn poly kn =
   let f x (l1,l2) = (l1,Names.Mindmap.add kn x l2) in
@@ -502,12 +509,21 @@ let section_segment_of_constant con =
 let section_segment_of_mutual_inductive kn =
   Names.Mindmap.find kn (snd (pi3 (List.hd !sectab)))
 
-let variable_section_segment_of_reference = function
-  | ConstRef con -> pi1 (section_segment_of_constant con)
-  | IndRef (kn,_) | ConstructRef ((kn,_),_) ->
-      pi1 (section_segment_of_mutual_inductive kn)
-  | _ -> []
-                     
+let empty_segment = {
+  abstr_ctx = [];
+  abstr_subst = Univ.LMap.empty;
+  abstr_uctx = Univ.AUContext.empty;
+}
+
+let section_segment_of_reference = function
+| ConstRef c -> section_segment_of_constant c
+| IndRef (kn,_) | ConstructRef ((kn,_),_) ->
+  section_segment_of_mutual_inductive kn
+| VarRef _ -> empty_segment
+
+let variable_section_segment_of_reference gr =
+  (section_segment_of_reference gr).abstr_ctx
+
 let section_instance = function
   | VarRef id ->
      let eq = function
@@ -654,7 +670,7 @@ let discharge_con cst =
 let discharge_inductive (kn,i) =
   (discharge_kn kn,i)
 
-let discharge_abstract_universe_context (_, subst, abs_ctx) auctx =
+let discharge_abstract_universe_context { abstr_subst = subst; abstr_uctx = abs_ctx } auctx =
   let open Univ in
   let len = LMap.cardinal subst in
   let rec gen_subst i acc =
diff --git a/library/lib.mli b/library/lib.mli
index 721e2896f7..2f4d0d56ff 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -153,13 +153,22 @@ val init : unit -> unit
 (** {6 Section management for discharge } *)
 type variable_info = Context.Named.Declaration.t * Decl_kinds.binding_kind
 type variable_context = variable_info list 
-type abstr_info = variable_context * Univ.universe_level_subst * Univ.AUContext.t
+type abstr_info = private {
+  abstr_ctx : variable_context;
+  (** Section variables of this prefix *)
+  abstr_subst : Univ.universe_level_subst;
+  (** Abstract substitution: named universes are mapped to De Bruijn indices *)
+  abstr_uctx : Univ.AUContext.t;
+  (** Universe quantification, same length as the substitution *)
+}
 
 val instance_from_variable_context : variable_context -> Names.Id.t array
 val named_of_variable_context : variable_context -> Context.Named.t
 
 val section_segment_of_constant : Names.Constant.t -> abstr_info
 val section_segment_of_mutual_inductive: Names.MutInd.t -> abstr_info
+val section_segment_of_reference : Globnames.global_reference -> abstr_info
+
 val variable_section_segment_of_reference : Globnames.global_reference -> variable_context
 
 val section_instance : Globnames.global_reference -> Univ.Instance.t * Names.Id.t array
diff --git a/pretyping/arguments_renaming.ml b/pretyping/arguments_renaming.ml
index d59102b6c7..8ac471404a 100644
--- a/pretyping/arguments_renaming.ml
+++ b/pretyping/arguments_renaming.ml
@@ -40,16 +40,10 @@ let subst_rename_args (subst, (_, (r, names as orig))) =
   let r' = fst (subst_global subst r) in 
   if r==r' then orig else (r', names)
 
-let section_segment_of_reference = function
-  | ConstRef con -> Lib.section_segment_of_constant con
-  | IndRef (kn,_) | ConstructRef ((kn,_),_) ->
-      Lib.section_segment_of_mutual_inductive kn
-  | _ -> [], Univ.LMap.empty, Univ.AUContext.empty
-
 let discharge_rename_args = function
   | _, (ReqGlobal (c, names), _ as req) ->
      (try 
-       let vars,_,_ = section_segment_of_reference c in
+       let vars = Lib.variable_section_segment_of_reference c in
        let c' = pop_global_reference c in
        let var_names = List.map (fst %> NamedDecl.get_id %> Name.mk_name) vars in
        let names' = var_names @ names in
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index ac88468545..78de0437d0 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -121,10 +121,10 @@ module ReductionBehaviour = struct
     let r' = fst (subst_global subst r) in if r==r' then orig else (r',o)
 
   let discharge = function
-    | _,(ReqGlobal (ConstRef c, req), (_, b)) ->
+    | _,(ReqGlobal (ConstRef c as gr, req), (_, b)) ->
       let b =
-        if Lib.is_in_section (ConstRef c) then
-          let vars, _, _ = Lib.section_segment_of_constant c in
+        if Lib.is_in_section gr then
+          let vars = Lib.variable_section_segment_of_reference gr in
           let extra = List.length vars in
           let nargs' =
              if b.b_nargs = max_int then max_int
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index f153b63410..3f947fd23f 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -219,7 +219,8 @@ let discharge_class (_,cl) =
     in grs', discharge_rel_context subst 1 ctx @ ctx' in
   let cl_impl' = Lib.discharge_global cl.cl_impl in
   if cl_impl' == cl.cl_impl then cl else
-    let ctx, _, _ as info = abs_context cl in
+    let info = abs_context cl in
+    let ctx = info.Lib.abstr_ctx in
     let ctx, subst = rel_of_variable_context ctx in
     let usubst, cl_univs' = Lib.discharge_abstract_universe_context info cl.cl_univs in
     let context = discharge_context ctx (subst, usubst) cl.cl_context in
-- 
cgit v1.2.3


From 6e49d0bee79cd68495955deb115b495fb01f01fd Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 13 Dec 2017 11:52:19 +0100
Subject: Hardening universe abstraction in Cooking.

---
 kernel/cooking.ml | 21 ++++++++-------------
 1 file changed, 8 insertions(+), 13 deletions(-)

diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index 7b921d35be..31988ac1c1 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -177,12 +177,14 @@ let cook_constr { Opaqueproof.modlist ; abstract } c =
   let hyps = Context.Named.map expmod (pi1 abstract) in
   abstract_constant_body (expmod c) hyps
 
-let lift_univs cb subst =
+let lift_univs cb subst auctx0 =
   match cb.const_universes with
-  | Monomorphic_const ctx -> subst, (Monomorphic_const ctx)
-  | Polymorphic_const auctx ->  
+  | Monomorphic_const ctx ->
+    assert (AUContext.is_empty auctx0);
+    subst, (Monomorphic_const ctx)
+  | Polymorphic_const auctx ->
     if (Univ.LMap.is_empty subst) then
-      subst, (Polymorphic_const auctx)
+      subst, (Polymorphic_const (AUContext.union auctx0 auctx))
     else
       let len = Univ.LMap.cardinal subst in
       let rec gen_subst i acc =
@@ -193,13 +195,13 @@ let lift_univs cb subst =
       in
       let subst = gen_subst (Univ.AUContext.size auctx - 1) subst in
       let auctx' = Univ.subst_univs_level_abstract_universe_context subst auctx in
-      subst, (Polymorphic_const auctx')
+      subst, (Polymorphic_const (AUContext.union auctx0 auctx'))
 
 let cook_constant ~hcons env { from = cb; info } =
   let { Opaqueproof.modlist; abstract } = info in
   let cache = RefTable.create 13 in
   let abstract, usubst, abs_ctx = abstract in
-  let usubst, univs = lift_univs cb usubst in
+  let usubst, univs = lift_univs cb usubst abs_ctx in
   let expmod = expmod_constr_subst cache modlist usubst in
   let hyps = Context.Named.map expmod abstract in
   let map c =
@@ -234,13 +236,6 @@ let cook_constant ~hcons env { from = cb; info } =
 	proj_eta = etab, etat;
 	proj_type = ty'; proj_body = c' }
   in
-  let univs =
-    match univs with
-    | Monomorphic_const ctx -> 
-      assert (AUContext.is_empty abs_ctx); univs
-    | Polymorphic_const auctx -> 
-      Polymorphic_const (AUContext.union abs_ctx auctx)
-  in
   {
     cook_body = body;
     cook_type = typ;
-- 
cgit v1.2.3


From 441bea723c511ed9e18ef005678bd01242b45c49 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 13 Dec 2017 13:57:10 +0100
Subject: Returning instance instead of substitution in universe context
 abstraction.

This datatype enforces stronger invariants, e.g. that we only have in the
substitution codomain a connex interval of variables from 0 to n - 1.
---
 kernel/cooking.ml      | 22 +++++++++-------------
 kernel/indtypes.ml     |  8 ++++++--
 kernel/mod_typing.ml   |  4 ++--
 kernel/opaqueproof.ml  |  2 +-
 kernel/opaqueproof.mli |  2 +-
 kernel/term_typing.ml  |  1 +
 kernel/univ.ml         |  2 +-
 kernel/univ.mli        |  4 ++--
 library/lib.ml         | 15 +++++----------
 library/lib.mli        |  4 ++--
 vernac/record.ml       |  1 +
 11 files changed, 31 insertions(+), 34 deletions(-)

diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index 31988ac1c1..1f407fc298 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -168,13 +168,14 @@ let on_body ml hy f = function
                  { Opaqueproof.modlist = ml; abstract = hy } o)
 
 let expmod_constr_subst cache modlist subst c =
+  let subst = Univ.make_instance_subst subst in
   let c = expmod_constr cache modlist c in
     Vars.subst_univs_level_constr subst c
 
-let cook_constr { Opaqueproof.modlist ; abstract } c =
+let cook_constr { Opaqueproof.modlist ; abstract = (vars, subst, _) } c =
   let cache = RefTable.create 13 in
-  let expmod = expmod_constr_subst cache modlist (pi2 abstract) in
-  let hyps = Context.Named.map expmod (pi1 abstract) in
+  let expmod = expmod_constr_subst cache modlist subst in
+  let hyps = Context.Named.map expmod vars in
   abstract_constant_body (expmod c) hyps
 
 let lift_univs cb subst auctx0 =
@@ -183,18 +184,13 @@ let lift_univs cb subst auctx0 =
     assert (AUContext.is_empty auctx0);
     subst, (Monomorphic_const ctx)
   | Polymorphic_const auctx ->
-    if (Univ.LMap.is_empty subst) then
+    if (Univ.Instance.is_empty subst) then
+      (** Still need to take the union for the constraints between globals *)
       subst, (Polymorphic_const (AUContext.union auctx0 auctx))
     else
-      let len = Univ.LMap.cardinal subst in
-      let rec gen_subst i acc =
-        if i < 0 then acc
-        else
-          let acc = Univ.LMap.add (Level.var i) (Level.var (i + len)) acc in
-          gen_subst (pred i) acc
-      in
-      let subst = gen_subst (Univ.AUContext.size auctx - 1) subst in
-      let auctx' = Univ.subst_univs_level_abstract_universe_context subst auctx in
+      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
       subst, (Polymorphic_const (AUContext.union auctx0 auctx'))
 
 let cook_constant ~hcons env { from = cb; info } =
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 1f2ae0b6cc..b117f8714b 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -879,9 +879,13 @@ let abstract_inductive_universes iu =
   match iu with
   | Monomorphic_ind_entry ctx -> (Univ.empty_level_subst, Monomorphic_ind ctx)
   | Polymorphic_ind_entry ctx -> 
-    let (inst, auctx) = Univ.abstract_universes ctx in (inst, Polymorphic_ind auctx)
+    let (inst, auctx) = Univ.abstract_universes ctx in
+    let inst = Univ.make_instance_subst inst in
+    (inst, Polymorphic_ind auctx)
   | Cumulative_ind_entry cumi -> 
-    let (inst, acumi) = Univ.abstract_cumulativity_info cumi in (inst, Cumulative_ind acumi)
+    let (inst, acumi) = Univ.abstract_cumulativity_info cumi in
+    let inst = Univ.make_instance_subst inst in
+    (inst, Cumulative_ind acumi)
 
 let build_inductive env prv iu env_ar paramsctxt kn isrecord isfinite inds nmr recargs =
   let ntypes = Array.length inds in
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index f7e755f005..b7eb481ee3 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -94,8 +94,8 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv =
           let ctx = Univ.ContextSet.of_context ctx in
           c', Monomorphic_const ctx, Univ.ContextSet.add_constraints cst ctx
         | Polymorphic_const uctx ->
-          let subst, ctx = Univ.abstract_universes ctx in
-          let c = Vars.subst_univs_level_constr subst c in
+          let inst, ctx = Univ.abstract_universes ctx in
+          let c = Vars.subst_univs_level_constr (Univ.make_instance_subst inst) c in
           let () =
             if not (UGraph.check_subtype (Environ.universes env) uctx ctx) then
               error_incorrect_with_constraint lab
diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml
index 45a62d55a1..c2fcfbfd6a 100644
--- a/kernel/opaqueproof.ml
+++ b/kernel/opaqueproof.ml
@@ -16,7 +16,7 @@ type work_list = (Instance.t * Id.t array) Cmap.t *
 
 type cooking_info = { 
   modlist : work_list; 
-  abstract : Context.Named.t * Univ.universe_level_subst * Univ.AUContext.t } 
+  abstract : Context.Named.t * Univ.Instance.t * Univ.AUContext.t }
 type proofterm = (constr * Univ.ContextSet.t) Future.computation
 type opaque =
   | Indirect of substitution list * DirPath.t * int (* subst, lib, index *)
diff --git a/kernel/opaqueproof.mli b/kernel/opaqueproof.mli
index 20d76ce238..c8339e6eb3 100644
--- a/kernel/opaqueproof.mli
+++ b/kernel/opaqueproof.mli
@@ -49,7 +49,7 @@ type work_list = (Univ.Instance.t * Id.t array) Cmap.t *
 
 type cooking_info = { 
   modlist : work_list; 
-  abstract : Context.Named.t * Univ.universe_level_subst * Univ.AUContext.t } 
+  abstract : Context.Named.t * Univ.Instance.t * Univ.AUContext.t }
 
 (* The type has two caveats:
    1) cook_constr is defined after
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 2e4426d621..cbc4ee2ec4 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -232,6 +232,7 @@ let abstract_constant_universes = function
     Univ.empty_level_subst, Monomorphic_const uctx
   | Polymorphic_const_entry uctx ->
     let sbst, auctx = Univ.abstract_universes uctx in
+    let sbst = Univ.make_instance_subst sbst in
     sbst, Polymorphic_const auctx
 
 let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 8cf9028fb1..fee431ff43 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -1168,7 +1168,7 @@ let abstract_universes ctx =
       (UContext.constraints ctx)
   in
   let ctx = UContext.make (instance, cstrs) in
-  subst, ctx
+  instance, ctx
 
 let abstract_cumulativity_info (univcst, substcst) = 
   let instance, univcst = abstract_universes univcst in
diff --git a/kernel/univ.mli b/kernel/univ.mli
index 4593944395..324167890a 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -470,9 +470,9 @@ val subst_instance_universe : Instance.t -> Universe.t -> Universe.t
 val make_instance_subst : Instance.t -> universe_level_subst
 val make_inverse_instance_subst : Instance.t -> universe_level_subst
 
-val abstract_universes : UContext.t -> universe_level_subst * AUContext.t
+val abstract_universes : UContext.t -> Instance.t * AUContext.t
 
-val abstract_cumulativity_info : CumulativityInfo.t -> universe_level_subst * ACumulativityInfo.t
+val abstract_cumulativity_info : CumulativityInfo.t -> Instance.t * ACumulativityInfo.t
 
 val make_abstract_instance : AUContext.t -> Instance.t
 
diff --git a/library/lib.ml b/library/lib.ml
index 16dd7fdd01..971089c171 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -419,7 +419,7 @@ type variable_info = Context.Named.Declaration.t * Decl_kinds.binding_kind
 type variable_context = variable_info list
 type abstr_info = {
   abstr_ctx : variable_context;
-  abstr_subst : Univ.universe_level_subst;
+  abstr_subst : Univ.Instance.t;
   abstr_uctx : Univ.AUContext.t;
 }
 type abstr_list = abstr_info Names.Cmap.t * abstr_info Names.Mindmap.t
@@ -511,7 +511,7 @@ let section_segment_of_mutual_inductive kn =
 
 let empty_segment = {
   abstr_ctx = [];
-  abstr_subst = Univ.LMap.empty;
+  abstr_subst = Univ.Instance.empty;
   abstr_uctx = Univ.AUContext.empty;
 }
 
@@ -672,13 +672,8 @@ let discharge_inductive (kn,i) =
 
 let discharge_abstract_universe_context { abstr_subst = subst; abstr_uctx = abs_ctx } auctx =
   let open Univ in
-  let len = LMap.cardinal subst in
-  let rec gen_subst i acc =
-    if i < 0 then acc
-    else
-      let acc = LMap.add (Level.var i) (Level.var (i + len)) acc in
-      gen_subst (pred i) acc
-  in
-  let subst = gen_subst (AUContext.size auctx - 1) subst in
+  let ainst = make_abstract_instance auctx in
+  let subst = Instance.append subst ainst in
+  let subst = make_instance_subst subst in
   let auctx = Univ.subst_univs_level_abstract_universe_context subst auctx in
   subst, AUContext.union abs_ctx auctx
diff --git a/library/lib.mli b/library/lib.mli
index 2f4d0d56ff..cf75d5f8cf 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -156,8 +156,8 @@ type variable_context = variable_info list
 type abstr_info = private {
   abstr_ctx : variable_context;
   (** Section variables of this prefix *)
-  abstr_subst : Univ.universe_level_subst;
-  (** Abstract substitution: named universes are mapped to De Bruijn indices *)
+  abstr_subst : Univ.Instance.t;
+  (** Actual names of the abstracted variables *)
   abstr_uctx : Univ.AUContext.t;
   (** Universe quantification, same length as the substitution *)
 }
diff --git a/vernac/record.ml b/vernac/record.ml
index d9dc16d96e..1e464eb8bf 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -531,6 +531,7 @@ let declare_class finite def cum ubinders univs id idbuild paramimpls params ari
     match univs with
     | Polymorphic_const_entry univs ->
       let usubst, auctx = Univ.abstract_universes univs in
+      let usubst = Univ.make_instance_subst usubst in
       let map c = Vars.subst_univs_level_constr usubst c in
       let fields = Context.Rel.map map fields in
       let ctx_context = on_snd (fun d -> Context.Rel.map map d) ctx_context in
-- 
cgit v1.2.3


From bad3f3b784d3de8851615b8f4b7afba734232d8e Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 13 Dec 2017 17:33:04 +0100
Subject: Moving some universe substitution code out of the kernel.

This code was not used at all inside the kernel, it was related to universe
unification that happens in the upper layer. It makes more sense to put it
somewhere upper.
---
 checker/univ.ml          |  8 -----
 checker/univ.mli         |  2 --
 engine/evd.ml            |  2 +-
 engine/uState.ml         |  2 +-
 engine/universes.ml      | 78 +++++++++++++++++++++++++++++++++++++++++++++---
 engine/universes.mli     |  5 ++++
 kernel/univ.ml           | 32 --------------------
 kernel/univ.mli          |  9 +++---
 kernel/vars.ml           | 43 --------------------------
 kernel/vars.mli          |  6 ----
 pretyping/unification.ml |  6 ++--
 tactics/ind_tables.ml    |  3 +-
 12 files changed, 89 insertions(+), 107 deletions(-)

diff --git a/checker/univ.ml b/checker/univ.ml
index 4f31318132..7d01657df7 100644
--- a/checker/univ.ml
+++ b/checker/univ.ml
@@ -881,14 +881,6 @@ type universe_level_subst = universe_level universe_map
 (** A full substitution might involve algebraic universes *)
 type universe_subst = universe universe_map
 
-let level_subst_of f = 
-  fun l -> 
-    try let u = f l in 
-	  match Universe.level u with
-	  | None -> l
-	  | Some l -> l
-    with Not_found -> l
-     
 module Instance : sig 
     type t = Level.t array
 
diff --git a/checker/univ.mli b/checker/univ.mli
index 0eadc6801f..21c94d9529 100644
--- a/checker/univ.mli
+++ b/checker/univ.mli
@@ -150,8 +150,6 @@ type universe_level_subst_fn = universe_level -> universe_level
 type universe_subst = universe universe_map
 type universe_level_subst = universe_level universe_map
 
-val level_subst_of : universe_subst_fn -> universe_level_subst_fn
-
 (** {6 Universe instances} *)
 
 module Instance :
diff --git a/engine/evd.ml b/engine/evd.ml
index e33c851f6e..0e94721589 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -855,7 +855,7 @@ let normalize_universe evd =
 
 let normalize_universe_instance evd l =
   let vars = ref (UState.subst evd.universes) in
-  let normalize = Univ.level_subst_of (Universes.normalize_univ_variable_opt_subst vars) in
+  let normalize = Universes.level_subst_of (Universes.normalize_univ_variable_opt_subst vars) in
     Univ.Instance.subst_fn normalize l
 
 let normalize_sort evars s =
diff --git a/engine/uState.ml b/engine/uState.ml
index 6131f4c033..6f2b3c4b26 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -516,7 +516,7 @@ let is_sort_variable uctx s =
   | _ -> None
 
 let subst_univs_context_with_def def usubst (ctx, cst) =
-  (Univ.LSet.diff ctx def, Univ.subst_univs_constraints usubst cst)
+  (Univ.LSet.diff ctx def, Universes.subst_univs_constraints usubst cst)
 
 let normalize_variables uctx =
   let normalized_variables, undef, def, subst = 
diff --git a/engine/universes.ml b/engine/universes.ml
index 30490ec56a..eaddf98a83 100644
--- a/engine/universes.ml
+++ b/engine/universes.ml
@@ -181,6 +181,30 @@ let enforce_eq_instances_univs strict x y c =
       (fun x y -> Constraints.add (Universe.make x, d, Universe.make y))
       ax ay c
 
+let enforce_univ_constraint (u,d,v) =
+  match d with
+  | Eq -> enforce_eq u v
+  | Le -> enforce_leq u v
+  | Lt -> enforce_leq (super u) v
+
+let subst_univs_level fn l =
+  try Some (fn l)
+  with Not_found -> None
+
+let subst_univs_constraint fn (u,d,v as c) cstrs =
+  let u' = subst_univs_level fn u in
+  let v' = subst_univs_level fn v in
+  match u', v' with
+  | None, None -> Constraint.add c cstrs
+  | Some u, None -> enforce_univ_constraint (u,d,Universe.make v) cstrs
+  | None, Some v -> enforce_univ_constraint (Universe.make u,d,v) cstrs
+  | Some u, Some v -> enforce_univ_constraint (u,d,v) cstrs
+
+let subst_univs_constraints subst csts =
+  Constraint.fold
+    (fun c cstrs -> subst_univs_constraint subst c cstrs)
+    csts Constraint.empty
+
 let subst_univs_universe_constraint fn (u,d,v) =
   let u' = subst_univs_universe fn u and v' = subst_univs_universe fn v in
     if Universe.equal u' v' then None
@@ -519,13 +543,60 @@ let choose_canonical ctx flexible algs s =
 	      let canon = LSet.choose algs in
 		canon, (global, rigid, LSet.remove canon flexible)
 
+let level_subst_of f =
+  fun l ->
+    try let u = f l in
+          match Universe.level u with
+          | None -> l
+          | Some l -> l
+    with Not_found -> l
+
+let subst_univs_fn_constr f c =
+  let changed = ref false in
+  let fu = Univ.subst_univs_universe f in
+  let fi = Univ.Instance.subst_fn (level_subst_of f) in
+  let rec aux t =
+    match kind t with
+    | Sort (Sorts.Type u) ->
+      let u' = fu u in
+        if u' == u then t else
+          (changed := true; mkSort (Sorts.sort_of_univ u'))
+    | Const (c, u) ->
+      let u' = fi u in
+        if u' == u then t
+        else (changed := true; mkConstU (c, u'))
+    | Ind (i, u) ->
+      let u' = fi u in
+        if u' == u then t
+        else (changed := true; mkIndU (i, u'))
+    | Construct (c, u) ->
+      let u' = fi u in
+        if u' == u then t
+        else (changed := true; mkConstructU (c, u'))
+    | _ -> map aux t
+  in
+  let c' = aux c in
+    if !changed then c' else c
+
+let subst_univs_constr subst c =
+  if Univ.is_empty_subst subst then c
+  else
+    let f = Univ.make_subst subst in
+      subst_univs_fn_constr f c
+
+let subst_univs_constr =
+  if Flags.profile then
+    let subst_univs_constr_key = CProfile.declare_profile "subst_univs_constr" in
+      CProfile.profile2 subst_univs_constr_key subst_univs_constr
+  else subst_univs_constr
+
 let subst_univs_fn_puniverses lsubst (c, u as cu) =
   let u' = Instance.subst_fn lsubst u in
     if u' == u then cu else (c, u')
 
 let nf_evars_and_universes_opt_subst f subst =
   let subst = fun l -> match LMap.find l subst with None -> raise Not_found | Some l' -> l' in
-  let lsubst = Univ.level_subst_of subst in
+  let lsubst = level_subst_of subst in
   let rec aux c =
     match kind c with
     | Evar (evk, args) ->
@@ -605,7 +676,7 @@ let normalize_opt_subst ctx =
   in !ectx
 
 type universe_opt_subst = Universe.t option universe_map
-	  
+
 let make_opt_subst s = 
   fun x -> 
     (match Univ.LMap.find x s with
@@ -614,8 +685,7 @@ let make_opt_subst s =
 
 let subst_opt_univs_constr s = 
   let f = make_opt_subst s in
-    Vars.subst_univs_fn_constr f
-
+  subst_univs_fn_constr f
 
 let normalize_univ_variables ctx = 
   let ctx = normalize_opt_subst ctx in
diff --git a/engine/universes.mli b/engine/universes.mli
index 1a98d969b4..130dcf8bb8 100644
--- a/engine/universes.mli
+++ b/engine/universes.mli
@@ -154,6 +154,11 @@ val extend_context : 'a in_universe_context_set -> ContextSet.t ->
 
 module UF : Unionfind.PartitionSig with type elt = Level.t
 
+val level_subst_of : universe_subst_fn -> universe_level_subst_fn
+val subst_univs_constraints : universe_subst_fn -> Constraint.t -> Constraint.t
+
+val subst_univs_constr : universe_subst -> constr -> constr
+
 type universe_opt_subst = Universe.t option universe_map
 
 val make_opt_subst : universe_opt_subst -> universe_subst_fn
diff --git a/kernel/univ.ml b/kernel/univ.ml
index fee431ff43..f72f6f26a9 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -686,12 +686,6 @@ let enforce_leq u v c =
 let enforce_leq_level u v c =
   if Level.equal u v then c else Constraint.add (u,Le,v) c
 
-let enforce_univ_constraint (u,d,v) =
-  match d with
-  | Eq -> enforce_eq u v
-  | Le -> enforce_leq u v
-  | Lt -> enforce_leq (super u) v
-
 (* Miscellaneous functions to remove or test local univ assumed to
    occur in a universe *)
 
@@ -718,14 +712,6 @@ type universe_level_subst = universe_level universe_map
 (** A full substitution might involve algebraic universes *)
 type universe_subst = universe universe_map
 
-let level_subst_of f = 
-  fun l -> 
-    try let u = f l in 
-	  match Universe.level u with
-	  | None -> l
-	  | Some l -> l
-    with Not_found -> l
-     
 module Instance : sig 
     type t = Level.t array
 
@@ -1128,24 +1114,6 @@ let subst_univs_universe fn ul =
 	List.fold_left (fun acc u -> Universe.merge_univs acc (Universe.tip u))
 	  substs nosubst
 
-let subst_univs_level fn l = 
-  try Some (fn l)
-  with Not_found -> None
-
-let subst_univs_constraint fn (u,d,v as c) cstrs =
-  let u' = subst_univs_level fn u in
-  let v' = subst_univs_level fn v in
-  match u', v' with
-  | None, None -> Constraint.add c cstrs
-  | Some u, None -> enforce_univ_constraint (u,d,make v) cstrs
-  | None, Some v -> enforce_univ_constraint (make u,d,v) cstrs
-  | Some u, Some v -> enforce_univ_constraint (u,d,v) cstrs
-
-let subst_univs_constraints subst csts =
-  Constraint.fold 
-    (fun c cstrs -> subst_univs_constraint subst c cstrs)
-    csts Constraint.empty 
-
 let make_instance_subst i = 
   let arr = Instance.to_array i in
     Array.fold_left_i (fun i acc l ->
diff --git a/kernel/univ.mli b/kernel/univ.mli
index 324167890a..63bef1b81b 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -238,8 +238,6 @@ type universe_level_subst_fn = Level.t -> Level.t
 type universe_subst = Universe.t universe_map
 type universe_level_subst = Level.t universe_map
 
-val level_subst_of : universe_subst_fn -> universe_level_subst_fn
-
 (** {6 Universe instances} *)
 
 module Instance :
@@ -461,18 +459,21 @@ val is_empty_subst : universe_subst -> bool
 val make_subst : universe_subst -> universe_subst_fn
 
 val subst_univs_universe : universe_subst_fn -> Universe.t -> Universe.t
-val subst_univs_constraints : universe_subst_fn -> Constraint.t -> Constraint.t
+(** Only user in the kernel is template polymorphism. Ideally we get rid of
+    this code if it goes away. *)
 
 (** Substitution of instances *)
 val subst_instance_instance : Instance.t -> Instance.t -> Instance.t
 val subst_instance_universe : Instance.t -> Universe.t -> Universe.t
 
 val make_instance_subst : Instance.t -> universe_level_subst
+(** Creates [u(0) ↦ 0; ...; u(n-1) ↦ n - 1] out of [u(0); ...; u(n - 1)] *)
+
 val make_inverse_instance_subst : Instance.t -> universe_level_subst
 
 val abstract_universes : UContext.t -> Instance.t * AUContext.t
-
 val abstract_cumulativity_info : CumulativityInfo.t -> Instance.t * ACumulativityInfo.t
+(** TODO: move universe abstraction out of the kernel *)
 
 val make_abstract_instance : AUContext.t -> Instance.t
 
diff --git a/kernel/vars.ml b/kernel/vars.ml
index eae917b5a2..b3b3eff628 100644
--- a/kernel/vars.ml
+++ b/kernel/vars.ml
@@ -235,49 +235,6 @@ let subst_vars subst c = substn_vars 1 subst c
 (** Universe substitutions *)
 open Constr
 
-let subst_univs_fn_puniverses fn =
-  let f = Univ.Instance.subst_fn fn in
-    fun ((c, u) as x) -> let u' = f u in if u' == u then x else (c, u')
-
-let subst_univs_fn_constr f c =
-  let changed = ref false in
-  let fu = Univ.subst_univs_universe f in
-  let fi = Univ.Instance.subst_fn (Univ.level_subst_of f) in
-  let rec aux t = 
-    match kind t with
-    | Sort (Sorts.Type u) -> 
-      let u' = fu u in
-	if u' == u then t else 
-	  (changed := true; mkSort (Sorts.sort_of_univ u'))
-    | Const (c, u) -> 
-      let u' = fi u in 
-	if u' == u then t
-	else (changed := true; mkConstU (c, u'))
-    | Ind (i, u) ->
-      let u' = fi u in 
-	if u' == u then t
-	else (changed := true; mkIndU (i, u'))
-    | Construct (c, u) ->
-      let u' = fi u in 
-	if u' == u then t
-	else (changed := true; mkConstructU (c, u'))
-    | _ -> map aux t
-  in 
-  let c' = aux c in
-    if !changed then c' else c
-
-let subst_univs_constr subst c =
-  if Univ.is_empty_subst subst then c
-  else 
-    let f = Univ.make_subst subst in
-      subst_univs_fn_constr f c
-
-let subst_univs_constr = 
-  if Flags.profile then
-    let subst_univs_constr_key = CProfile.declare_profile "subst_univs_constr" in
-      CProfile.profile2 subst_univs_constr_key subst_univs_constr
-  else subst_univs_constr
-
 let subst_univs_level_constr subst c =
   if Univ.is_empty_level_subst subst then c
   else 
diff --git a/kernel/vars.mli b/kernel/vars.mli
index 964de4e958..b74d25260f 100644
--- a/kernel/vars.mli
+++ b/kernel/vars.mli
@@ -129,12 +129,6 @@ val subst_var : Id.t -> constr -> constr
 
 open Univ
 
-val subst_univs_fn_constr : universe_subst_fn -> constr -> constr
-val subst_univs_fn_puniverses : universe_level_subst_fn -> 
-  'a puniverses -> 'a puniverses
-
-val subst_univs_constr : universe_subst -> constr -> constr
-
 (** Level substitutions for polymorphism. *)
 
 val subst_univs_level_constr : universe_level_subst -> constr -> constr
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index b41fb4e4dd..8df8f84742 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-module CVars = Vars
-
 open CErrors
 open Pp
 open Util
@@ -1527,7 +1525,7 @@ let indirectly_dependent sigma c d decls =
 let finish_evar_resolution ?(flags=Pretyping.all_and_fail_flags) env current_sigma (pending,c) =
   let sigma = Pretyping.solve_remaining_evars flags env current_sigma pending in
   let sigma, subst = nf_univ_variables sigma in
-  (sigma, EConstr.of_constr (CVars.subst_univs_constr subst (EConstr.Unsafe.to_constr (nf_evar sigma c))))
+  (sigma, EConstr.of_constr (Universes.subst_univs_constr subst (EConstr.Unsafe.to_constr (nf_evar sigma c))))
 
 let default_matching_core_flags sigma =
   let ts = Names.full_transparent_state in {
@@ -1617,7 +1615,7 @@ let make_pattern_test from_prefix_of_ind is_correct_type env sigma (pending,c) =
   | Some (sigma,_,l) ->
      let c = applist (nf_evar sigma (local_strong whd_meta sigma c), l) in
      let univs, subst = nf_univ_variables sigma in
-     Some (sigma,EConstr.of_constr (CVars.subst_univs_constr subst (EConstr.Unsafe.to_constr c))))
+     Some (sigma,EConstr.of_constr (Universes.subst_univs_constr subst (EConstr.Unsafe.to_constr c))))
 
 let make_eq_test env evd c =
   let out cstr =
diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml
index e1bf32f3ce..bc2fea2bd5 100644
--- a/tactics/ind_tables.ml
+++ b/tactics/ind_tables.ml
@@ -121,8 +121,7 @@ let define internal id c p univs =
   let fd = declare_constant ~internal in
   let id = compute_name internal id in
   let ctx = Evd.normalize_evar_universe_context univs in
-  let c = Vars.subst_univs_fn_constr 
-    (Universes.make_opt_subst (Evd.evar_universe_context_subst ctx)) c in
+  let c = Universes.subst_opt_univs_constr (Evd.evar_universe_context_subst ctx) c in
   let univs =
     if p then Polymorphic_const_entry (UState.context ctx)
     else Monomorphic_const_entry (UState.context_set ctx)
-- 
cgit v1.2.3


From 4131f060ac42f121685817fcc9546c3899c09ab7 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 31 Dec 2017 21:05:16 +0100
Subject: Add a comment about universe lifting in sections in the kernel.

---
 kernel/cooking.ml | 11 +++++++++++
 1 file changed, 11 insertions(+)

diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index 1f407fc298..23a578d993 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -184,6 +184,17 @@ let lift_univs cb subst auctx0 =
     assert (AUContext.is_empty auctx0);
     subst, (Monomorphic_const ctx)
   | Polymorphic_const auctx ->
+    (** Given a named instance [subst := u₀ ... uₙ₋₁] together with an abstract
+        context [auctx0 := 0 ... n - 1 |= C{0, ..., n - 1}] of the same length,
+        and another abstract context relative to the former context
+        [auctx := 0 ... m - 1 |= C'{u₀, ..., uₙ₋₁, 0, ..., m - 1}],
+        construct the lifted abstract universe context
+        [0 ... n - 1 n ... n + m - 1 |=
+          C{0, ... n - 1} ∪
+          C'{0, ..., n - 1, n, ..., n + m - 1} ]
+        together with the instance
+        [u₀ ... uₙ₋₁ Var(0) ... Var (m - 1)].
+    *)
     if (Univ.Instance.is_empty subst) then
       (** Still need to take the union for the constraints between globals *)
       subst, (Polymorphic_const (AUContext.union auctx0 auctx))
-- 
cgit v1.2.3