Getting rid of AUContext abstraction breakers in Recordops.

4 files changed, 12 insertions, 8 deletions

diff --git a/API/API.mli b/API/API.mli
index 9f7a6ded8..a661b34c5 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -84,6 +84,11 @@ sig
     val empty : t
   end
 
+  module AUContext :
+  sig
+    type t = Univ.AUContext.t
+  end
+
   type universe_context = UContext.t
   [@@ocaml.deprecated "alias of API.Univ.UContext.t"]
 
@@ -2884,7 +2889,7 @@ sig
                   | Default_cs
   type obj_typ = Recordops.obj_typ = {
         o_DEF : Term.constr;
-        o_CTX : Univ.ContextSet.t;
+        o_CTX : Univ.AUContext.t;
         o_INJ : int option;      (** position of trivial argument *)
         o_TABS : Term.constr list;    (** ordered *)
         o_TPARAMS : Term.constr list; (** ordered *)
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 87f29ba49..cb76df4e8 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -205,7 +205,8 @@ let check_conv_record env sigma (t1,sk1) (t2,sk2) =
       else match (Stack.strip_n_app (l_us-1) sk2_effective) with
       | None -> raise Not_found
       | Some (l',el,s') -> (l'@Stack.append_app [|el|] Stack.empty,s') in
-  let subst, ctx' = Universes.fresh_universe_context_set_instance ctx in
+  let u, ctx' = Universes.fresh_instance_from ctx None in
+  let subst = Univ.make_inverse_instance_subst u in
   let c = EConstr.of_constr c in
   let c' = subst_univs_level_constr subst c in
   let t' = EConstr.of_constr t' in
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index c498089ca..a23579609 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -134,7 +134,7 @@ let find_projection = function
 
 type obj_typ = {
   o_DEF : constr;
-  o_CTX : Univ.ContextSet.t;
+  o_CTX : Univ.AUContext.t;
   o_INJ : int option;      (* position of trivial argument if any *)
   o_TABS : constr list;    (* ordered *)
   o_TPARAMS : constr list; (* ordered *)
@@ -203,10 +203,8 @@ let warn_projection_no_head_constant =
 let compute_canonical_projections warn (con,ind) =
   let env = Global.env () in
   let ctx = Environ.constant_context env con in
-  let u = Univ.AUContext.instance ctx in
-  let ctx = Univ.UContext.make (u, Univ.AUContext.instantiate u ctx) in
+  let u = Univ.make_abstract_instance ctx in
   let v = (mkConstU (con,u)) in
-  let ctx = Univ.ContextSet.of_context ctx in
   let c = Environ.constant_value_in env (con,u) in
   let sign,t = Reductionops.splay_lam env Evd.empty (EConstr.of_constr c) in
   let t = EConstr.Unsafe.to_constr t in
@@ -302,7 +300,7 @@ let error_not_structure ref =
 let check_and_decompose_canonical_structure ref =
   let sp = match ref with ConstRef sp -> sp | _ -> error_not_structure ref in
   let env = Global.env () in
-  let u = Univ.AUContext.instance (Environ.constant_context env sp) in
+  let u = Univ.make_abstract_instance (Environ.constant_context env sp) in
   let vc = match Environ.constant_opt_value_in env (sp, u) with
     | Some vc -> vc
     | None -> error_not_structure ref in
diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli
index 27d1650af..de09edcdc 100644
--- a/pretyping/recordops.mli
+++ b/pretyping/recordops.mli
@@ -57,7 +57,7 @@ type cs_pattern =
 
 type obj_typ = {
   o_DEF : constr;
-  o_CTX : Univ.ContextSet.t;
+  o_CTX : Univ.AUContext.t;
   o_INJ : int option;      (** position of trivial argument *)
   o_TABS : constr list;    (** ordered *)
   o_TPARAMS : constr list; (** ordered *)