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.

2 files changed, 7 insertions, 12 deletions

diff --git a/library/lib.ml b/library/lib.ml
index 16dd7fdd0..971089c17 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 2f4d0d56f..cf75d5f8c 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 *)
 }