Merge PR #870: Prepare De Bruijn universe abstractions, Episode I: Kernel

5 files changed, 16 insertions, 20 deletions

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index b5d195873..87f29ba49 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -353,9 +353,8 @@ let exact_ise_stack2 env evd f sk1 sk2 =
 let check_leq_inductives evd cumi u u' =
   let u = EConstr.EInstance.kind evd u in
   let u' = EConstr.EInstance.kind evd u' in
-  let length_ind_instance = 
-    Univ.Instance.length
-      (Univ.AUContext.instance (Univ.ACumulativityInfo.univ_context cumi))
+  let length_ind_instance =
+    Univ.AUContext.size (Univ.ACumulativityInfo.univ_context cumi)
   in
   let ind_sbcst =  Univ.ACumulativityInfo.subtyp_context cumi in
   if not ((length_ind_instance = Univ.Instance.length u) &&
@@ -364,9 +363,7 @@ let check_leq_inductives evd cumi u u' =
   else
     begin
      let comp_subst = (Univ.Instance.append u u') in
-     let comp_cst = 
-       Univ.UContext.constraints (Univ.subst_instance_context comp_subst ind_sbcst)
-     in
+     let comp_cst =  Univ.AUContext.instantiate comp_subst ind_sbcst in
      Evd.add_constraints evd comp_cst
     end
 
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 4131f9a61..c498089ca 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -203,7 +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.UContext.instance ctx in
+  let u = Univ.AUContext.instance ctx in
+  let ctx = Univ.UContext.make (u, Univ.AUContext.instantiate u 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
@@ -301,7 +302,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 = Environ.constant_instance env sp in
+  let u = Univ.AUContext.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/reductionops.ml b/pretyping/reductionops.ml
index cc1709f1c..21ed8e0a2 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -1362,25 +1362,23 @@ let sigma_compare_instances ~flex i0 i1 sigma =
 	raise Reduction.NotConvertible
 
 let sigma_check_inductive_instances cv_pb uinfind u u' sigma =
-  let ind_instance = 
-    Univ.AUContext.instance (Univ.ACumulativityInfo.univ_context uinfind) 
+  let len_instance =
+    Univ.AUContext.size (Univ.ACumulativityInfo.univ_context uinfind)
   in
   let ind_sbctx =  Univ.ACumulativityInfo.subtyp_context uinfind  in
-  if not ((Univ.Instance.length ind_instance = Univ.Instance.length u) &&
-          (Univ.Instance.length ind_instance = Univ.Instance.length u')) then
+  if not ((len_instance = Univ.Instance.length u) &&
+          (len_instance = Univ.Instance.length u')) then
      anomaly (Pp.str "Invalid inductive subtyping encountered!")
   else
     let comp_cst =
       let comp_subst = (Univ.Instance.append u u') in
-      Univ.UContext.constraints (Univ.subst_instance_context comp_subst ind_sbctx)
+      Univ.AUContext.instantiate comp_subst ind_sbctx
     in
     let comp_cst =
       match cv_pb with
         Reduction.CONV -> 
         let comp_subst = (Univ.Instance.append u' u) in
-        let comp_cst' = 
-          Univ.UContext.constraints(Univ.subst_instance_context comp_subst ind_sbctx)
-        in
+        let comp_cst' = Univ.AUContext.instantiate comp_subst ind_sbctx in
         Univ.Constraint.union comp_cst comp_cst'
       | Reduction.CUMUL -> comp_cst
     in
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 201f79c39..bae831b63 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -117,10 +117,10 @@ let typeclass_univ_instance (cl,u') =
       match cl.cl_impl with
       | ConstRef c -> 
         let cb = Global.lookup_constant c in
-        Declareops.constant_polymorphic_instance cb
+        Univ.AUContext.instance (Declareops.constant_polymorphic_context cb)
       | IndRef c ->
          let mib,oib = Global.lookup_inductive c in
-         Declareops.inductive_polymorphic_instance mib
+         Univ.AUContext.instance (Declareops.inductive_polymorphic_context mib)
       | _ -> Univ.Instance.empty
     in Array.fold_left2 (fun subst u u' -> Univ.LMap.add u u' subst) 
       Univ.LMap.empty (Univ.Instance.to_array u) (Univ.Instance.to_array u')
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index b3eaa3cb9..66cc42cb6 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -174,7 +174,7 @@ and nf_whd env sigma whd typ =
   | Vatom_stk(Aind ((mi,i) as ind), stk) ->
      let mib = Environ.lookup_mind mi env in
      let nb_univs =
-       Univ.Instance.length (Declareops.inductive_polymorphic_instance mib)
+       Univ.AUContext.size (Declareops.inductive_polymorphic_context mib)
      in
      let mk u =
        let pind = (ind, u) in (mkIndU pind, type_of_ind env pind)
@@ -203,7 +203,7 @@ and constr_type_of_idkey env sigma (idkey : Vars.id_key) stk =
   | ConstKey cst ->
      let cbody = Environ.lookup_constant cst env in
      let nb_univs =
-       Univ.Instance.length (Declareops.constant_polymorphic_instance cbody)
+       Univ.AUContext.size (Declareops.constant_polymorphic_context cbody)
      in
      let mk u =
        let pcst = (cst, u) in (mkConstU pcst, Typeops.type_of_constant_in env pcst)