Clean up universes of constants and inductives

7 files changed, 112 insertions, 86 deletions

diff --git a/pretyping/arguments_renaming.ml b/pretyping/arguments_renaming.ml
index 1bd03491a..c7b37aba5 100644
--- a/pretyping/arguments_renaming.ml
+++ b/pretyping/arguments_renaming.ml
@@ -43,7 +43,7 @@ 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.UContext.empty
+  | _ -> [], Univ.LMap.empty, Univ.AUContext.empty
 
 let discharge_rename_args = function
   | _, (ReqGlobal (c, names), _ as req) ->
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index be2fd8129..b15dde5d7 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -350,18 +350,22 @@ let exact_ise_stack2 env evd f sk1 sk2 =
     ise_stack2 evd (List.rev sk1) (List.rev sk2)
   else UnifFailure (evd, (* Dummy *) NotSameHead)
 
-let check_leq_inductives evd uinfind u u' =
+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 ind_instance = Univ.UContext.instance (Univ.UInfoInd.univ_context uinfind) in
-  let ind_sbcst = Univ.UContext.constraints (Univ.UInfoInd.subtyp_context uinfind) in
+  let ind_instance = 
+    Univ.AUContext.instance (Univ.ACumulativityInfo.univ_context cumi) 
+  in
+  let ind_sbcst =  Univ.ACumulativityInfo.subtyp_context cumi in
   if not ((Univ.Instance.length ind_instance = Univ.Instance.length u) &&
           (Univ.Instance.length ind_instance = Univ.Instance.length u')) then
      anomaly (Pp.str "Invalid inductive subtyping encountered!")
   else
     begin
      let comp_subst = (Univ.Instance.append u u') in
-     let comp_cst = Univ.subst_instance_constraints comp_subst ind_sbcst in
+     let comp_cst = 
+       Univ.UContext.constraints (Univ.subst_instance_context comp_subst ind_sbcst)
+     in
      Evd.add_constraints evd comp_cst
     end
 
@@ -491,23 +495,24 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
           let nparamsaplied' = Stack.args_size sk' in
           begin
             let mind = Environ.lookup_mind (fst ind) env in
-            if mind.Declarations.mind_polymorphic then
+            match mind.Declarations.mind_universes with
+            | Declarations.Monomorphic_ind _ | Declarations.Polymorphic_ind _ ->
+              UnifFailure (evd, NotSameHead)
+            | Declarations.Cumulative_ind cumi ->
               begin
                 let num_param_arity =
-                  (* Context.Rel.length (mind.Declarations.mind_packets.(snd ind).Declarations.mind_arity_ctxt) *)
-                  mind.Declarations.mind_nparams + mind.Declarations.mind_packets.(snd ind).Declarations.mind_nrealargs
+                  mind.Declarations.mind_nparams + 
+                  mind.Declarations.mind_packets.(snd ind).Declarations.mind_nrealargs
                 in
-                if not (num_param_arity = nparamsaplied && num_param_arity = nparamsaplied') then
+                if not (num_param_arity = nparamsaplied
+                        && num_param_arity = nparamsaplied') then
                   UnifFailure (evd, NotSameHead)
                 else
                   begin
-                    let uinfind = mind.Declarations.mind_universes in
-                    let evd' = check_leq_inductives evd uinfind u u' in
-                    Success (check_leq_inductives evd' uinfind u' u)
+                    let evd' = check_leq_inductives evd cumi u u' in
+                    Success (check_leq_inductives evd' cumi u' u)
                   end
               end
-            else
-              UnifFailure (evd, NotSameHead)
           end
         in
         first_try_strict_check (Names.eq_ind ind ind') u u' check_subtyping_constraints
@@ -518,26 +523,29 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
           let nparamsaplied = Stack.args_size sk in
           let nparamsaplied' = Stack.args_size sk' in
           let mind = Environ.lookup_mind (fst ind) env in
-          if mind.Declarations.mind_polymorphic then
+          match mind.Declarations.mind_universes with
+          | Declarations.Monomorphic_ind _ | Declarations.Polymorphic_ind _ ->
+            UnifFailure (evd, NotSameHead)
+          | Declarations.Cumulative_ind cumi ->
             begin
               let num_cnstr_args =
                 let nparamsctxt =
-                  (* Context.Rel.length mind.Declarations.mind_params_ctxt *)
-                  mind.Declarations.mind_nparams + mind.Declarations.mind_packets.(snd ind).Declarations.mind_nrealargs
+                  mind.Declarations.mind_nparams + 
+                  mind.Declarations.mind_packets.(snd ind).Declarations.mind_nrealargs
                 in
-                nparamsctxt + mind.Declarations.mind_packets.(snd ind).Declarations.mind_consnrealargs.(j - 1)
+                nparamsctxt + 
+                mind.Declarations.mind_packets.(snd ind).
+                  Declarations.mind_consnrealargs.(j - 1)
               in
-              if not (num_cnstr_args = nparamsaplied && num_cnstr_args = nparamsaplied') then
+              if not (num_cnstr_args = nparamsaplied 
+                      && num_cnstr_args = nparamsaplied') then
                 UnifFailure (evd, NotSameHead)
               else
                 begin
-                  let uinfind = mind.Declarations.mind_universes in
-                  let evd' = check_leq_inductives evd uinfind u u' in
-                  Success (check_leq_inductives evd' uinfind u' u)
+                  let evd' = check_leq_inductives evd cumi u u' in
+                  Success (check_leq_inductives evd' cumi u' u)
                 end
             end
-          else
-            UnifFailure (evd, NotSameHead)
         in
         first_try_strict_check (Names.eq_constructor cons cons') u u' check_subtyping_constraints
       | _, _ -> anomaly (Pp.str "")
@@ -546,7 +554,6 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
                 try compare_heads i
                 with Univ.UniverseInconsistency p -> UnifFailure (i, UnifUnivInconsistency p));
                  (fun i -> exact_ise_stack2 env i (evar_conv_x ts) sk sk')]
-(* >>>>>>> Make unification use subtyping info of inductives *)
   in
   let flex_maybeflex on_left ev ((termF,skF as apprF),cstsF) ((termM, skM as apprM),cstsM) vM =
     let switch f a b = if on_left then f a b else f b a in
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 1ef4a9f5e..2ae7c0f80 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -696,39 +696,52 @@ let infer_inductive_subtyping_arity_constructor
 let infer_inductive_subtyping env evd mind_ent =
   let { Entries.mind_entry_params = params;
         Entries.mind_entry_inds = entries;
-        Entries.mind_entry_polymorphic = poly;
-        Entries.mind_entry_cumulative = cum;
-        Entries.mind_entry_universes = ground_uinfind;
+        Entries.mind_entry_universes = ground_univs;
       } = mind_ent
   in
   let uinfind =
-    if poly && cum then
-    begin
-      let uctx = Univ.UInfoInd.univ_context ground_uinfind in
-      let sbsubst = Univ.UInfoInd.subtyping_susbst ground_uinfind in
-      let dosubst = subst_univs_level_constr sbsubst in
-      let instance_other = Univ.subst_univs_level_instance sbsubst (Univ.UContext.instance uctx) in
-      let constraints_other = Univ.subst_univs_level_constraints sbsubst (Univ.UContext.constraints uctx) in
-      let uctx_other = Univ.UContext.make (instance_other, constraints_other) in
-      let env = Environ.push_context uctx env in
-      let env = Environ.push_context uctx_other env in
-      let evd = Evd.merge_universe_context evd (UState.of_context_set (Univ.ContextSet.of_context uctx_other)) in
-      let (_, _, subtyp_constraints) =
-        List.fold_left
-          (fun ctxs indentry ->
-             let _, params = Typeops.infer_local_decls env params in
-             let ctxs' = infer_inductive_subtyping_arity_constructor
-                 ctxs dosubst indentry.Entries.mind_entry_arity true params
-             in
-             List.fold_left
-               (fun ctxs cons ->
-                  infer_inductive_subtyping_arity_constructor ctxs dosubst cons false params)
-               ctxs' indentry.Entries.mind_entry_lc
-          ) (env, evd, Univ.Constraint.empty) entries
-      in Univ.UInfoInd.make (Univ.UInfoInd.univ_context ground_uinfind,
-           Univ.UContext.make
-             (Univ.UContext.instance (Univ.UInfoInd.subtyp_context ground_uinfind),
-               subtyp_constraints))
-    end
-    else ground_uinfind
+    match ground_univs with
+    | Entries.Monomorphic_ind_entry _
+    | Entries.Polymorphic_ind_entry _ -> ground_univs
+    | Entries.Cumulative_ind_entry cumi -> 
+      begin
+        let uctx = Univ.CumulativityInfo.univ_context cumi in
+        let sbsubst = Univ.CumulativityInfo.subtyping_susbst cumi in
+        let dosubst = subst_univs_level_constr sbsubst in
+        let instance_other = 
+          Univ.subst_univs_level_instance sbsubst (Univ.UContext.instance uctx) 
+        in
+        let constraints_other = 
+          Univ.subst_univs_level_constraints
+            sbsubst (Univ.UContext.constraints uctx) 
+        in
+        let uctx_other = Univ.UContext.make (instance_other, constraints_other) in
+        let env = Environ.push_context uctx env in
+        let env = Environ.push_context uctx_other env in
+        let evd = 
+          Evd.merge_universe_context
+            evd (UState.of_context_set (Univ.ContextSet.of_context uctx_other)) 
+        in
+        let (_, _, subtyp_constraints) =
+          List.fold_left
+            (fun ctxs indentry ->
+               let _, params = Typeops.infer_local_decls env params in
+               let ctxs' = infer_inductive_subtyping_arity_constructor
+                   ctxs dosubst indentry.Entries.mind_entry_arity true params
+               in
+               List.fold_left
+                 (fun ctxs cons ->
+                    infer_inductive_subtyping_arity_constructor
+                      ctxs dosubst cons false params
+                 )
+                 ctxs' indentry.Entries.mind_entry_lc
+            ) (env, evd, Univ.Constraint.empty) entries
+        in 
+        Entries.Cumulative_ind_entry
+          (Univ.CumulativityInfo.make 
+             (Univ.CumulativityInfo.univ_context cumi,
+              Univ.UContext.make
+                (Univ.UContext.instance (Univ.CumulativityInfo.subtyp_context cumi),
+                 subtyp_constraints)))
+      end
   in {mind_ent with Entries.mind_entry_universes = uinfind;}
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index bc9e3a1f4..283a1dcd1 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -197,7 +197,7 @@ let warn_projection_no_head_constant =
 (* Intended to always succeed *)
 let compute_canonical_projections warn (con,ind) =
   let env = Global.env () in
-  let ctx = Univ.instantiate_univ_context (Environ.constant_context env con) in
+  let ctx = Environ.constant_context env con in
   let u = Univ.UContext.instance ctx in
   let v = (mkConstU (con,u)) in
   let ctx = Univ.ContextSet.of_context ctx in
@@ -298,8 +298,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 ctx = Environ.constant_context env sp in
-  let u = Univ.UContext.instance ctx in
+  let u = Environ.constant_instance 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 2040acba7..123c61016 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -1362,21 +1362,25 @@ 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.UContext.instance (Univ.UInfoInd.univ_context uinfind) in
-  let ind_sbcst = Univ.UContext.constraints (Univ.UInfoInd.subtyp_context uinfind) in
+  let ind_instance = 
+    Univ.AUContext.instance (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
      anomaly (Pp.str "Invalid inductive subtyping encountered!")
   else
     let comp_cst =
       let comp_subst = (Univ.Instance.append u u') in
-      Univ.subst_instance_constraints comp_subst ind_sbcst
+      Univ.UContext.constraints (Univ.subst_instance_context 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.subst_instance_constraints comp_subst ind_sbcst) in
+        let comp_cst' = 
+          Univ.UContext.constraints(Univ.subst_instance_context comp_subst ind_sbctx)
+        in
         Univ.Constraint.union comp_cst comp_cst'
       | Reduction.CUMUL -> comp_cst
     in
@@ -1389,34 +1393,43 @@ let sigma_conv_inductives
     cv_pb (mind, ind) u1 sv1 u2 sv2 sigma =
   try sigma_compare_instances ~flex:false u1 u2 sigma with
     Reduction.NotConvertible ->
-    if mind.Declarations.mind_polymorphic then
+    match mind.Declarations.mind_universes with
+    | Declarations.Monomorphic_ind _ ->
+      raise Reduction.NotConvertible
+    | Declarations.Polymorphic_ind _ ->
+      raise Reduction.NotConvertible
+    | Declarations.Cumulative_ind cumi ->
       let num_param_arity =
-        mind.Declarations.mind_nparams + mind.Declarations.mind_packets.(ind).Declarations.mind_nrealargs
+        mind.Declarations.mind_nparams + 
+        mind.Declarations.mind_packets.(ind).Declarations.mind_nrealargs
       in
       if not (num_param_arity = sv1 && num_param_arity = sv2) then
         raise Reduction.NotConvertible
       else
-        let uinfind = mind.Declarations.mind_universes in
-        sigma_check_inductive_instances cv_pb uinfind u1 u2 sigma
-    else raise Reduction.NotConvertible
+        sigma_check_inductive_instances cv_pb cumi u1 u2 sigma 
 
 let sigma_conv_constructors
     (mind, ind, cns) u1 sv1 u2 sv2 sigma =
   try sigma_compare_instances ~flex:false u1 u2 sigma with
     Reduction.NotConvertible ->
-    if mind.Declarations.mind_polymorphic then
+    match mind.Declarations.mind_universes with
+    | Declarations.Monomorphic_ind _ ->
+      raise Reduction.NotConvertible
+    | Declarations.Polymorphic_ind _ ->
+      raise Reduction.NotConvertible
+    | Declarations.Cumulative_ind cumi ->
       let num_cnstr_args =
         let nparamsctxt =
-          mind.Declarations.mind_nparams + mind.Declarations.mind_packets.(ind).Declarations.mind_nrealargs
-          (* Context.Rel.length mind.Declarations.mind_params_ctxt *) in
-        nparamsctxt + mind.Declarations.mind_packets.(ind).Declarations.mind_consnrealargs.(cns - 1)
+          mind.Declarations.mind_nparams + 
+          mind.Declarations.mind_packets.(ind).Declarations.mind_nrealargs
+        in
+        nparamsctxt + 
+        mind.Declarations.mind_packets.(ind).Declarations.mind_consnrealargs.(cns - 1)
       in
       if not (num_cnstr_args = sv1 && num_cnstr_args = sv2) then
         raise Reduction.NotConvertible
       else
-        let uinfind = mind.Declarations.mind_universes in
-        sigma_check_inductive_instances Reduction.CONV uinfind u1 u2 sigma
-    else raise Reduction.NotConvertible
+        sigma_check_inductive_instances Reduction.CONV cumi u1 u2 sigma
 
 let sigma_univ_state = 
   { Reduction.compare = sigma_compare_sorts;
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 152ccb079..f883e647b 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -111,20 +111,16 @@ let new_instance cl info glob poly impl =
 let classes : typeclasses ref = Summary.ref Refmap.empty ~name:"classes"
 let instances : instances ref = Summary.ref Refmap.empty ~name:"instances"
 
-open Declarations
-
 let typeclass_univ_instance (cl,u') =
   let subst = 
     let u = 
       match cl.cl_impl with
       | ConstRef c -> 
         let cb = Global.lookup_constant c in
-	  if cb.const_polymorphic then Univ.UContext.instance cb.const_universes
-	  else Univ.Instance.empty
+        Declareops.constant_polymorphic_instance cb
       | IndRef c ->
          let mib,oib = Global.lookup_inductive c in
-	  if mib.mind_polymorphic then Univ.UContext.instance (Univ.UInfoInd.univ_context mib.mind_universes)
-	  else Univ.Instance.empty
+         Declareops.inductive_polymorphic_instance 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 074b7373c..9e151fea2 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -174,8 +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 =
-       if mib.mind_polymorphic then Univ.UContext.size (Univ.UInfoInd.univ_context mib.mind_universes)
-       else 0
+       Univ.Instance.length (Declareops.inductive_polymorphic_instance mib)
      in
      let mk u =
        let pind = (ind, u) in (mkIndU pind, type_of_ind env pind)
@@ -204,8 +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 =
-       if cbody.const_polymorphic then Univ.UContext.size cbody.const_universes
-       else 0
+       Univ.Instance.length (Declareops.constant_polymorphic_instance cbody)
      in
      let mk u =
        let pcst = (cst, u) in (mkConstU pcst, Typeops.type_of_constant_in env pcst)