Clean up universes of constants and inductives

1 files changed, 39 insertions, 36 deletions

diff --git a/checker/reduction.ml b/checker/reduction.ml
index 70c0bdad0..5010920bc 100644
--- a/checker/reduction.ml
+++ b/checker/reduction.ml
@@ -156,22 +156,27 @@ let compare_stacks f fmind lft1 stk1 lft2 stk2 =
     cmp_rec (pure_stack lft1 stk1) (pure_stack lft2 stk2)
   else raise NotConvertible
 
-let convert_inductive_instances cv_pb uinfind u u' univs =
-  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 convert_inductive_instances cv_pb cumi u u' univs =
+  let ind_instance =
+      Univ.AUContext.instance (Univ.ACumulativityInfo.univ_context cumi) in
+  let ind_subtypctx =  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!")
+    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_subtypctx)
     in
     let comp_cst =
       match cv_pb with
         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' =
+          let comp_subst = (Univ.Instance.append u' u) in
+          Univ.UContext.constraints
+            (Univ.subst_instance_context comp_subst ind_subtypctx)
+        in
         Univ.Constraint.union comp_cst comp_cst'
       | CUMUL -> comp_cst
     in
@@ -179,28 +184,32 @@ let convert_inductive_instances cv_pb uinfind u u' univs =
 
 let convert_inductives
     cv_pb (mind, ind) u1 sv1 u2 sv2 univs =
-  let num_param_arity =
-    mind.mind_nparams + mind.mind_packets.(ind).mind_nrealargs
-  in
-  if not (num_param_arity = sv1 && num_param_arity = sv2) then
-    convert_universes univs u1 u2
-  else
-    let uinfind = mind.mind_universes in
-    convert_inductive_instances cv_pb uinfind u1 u2 univs
+  match mind.mind_universes with
+  | Monomorphic_ind _ | Polymorphic_ind _ -> convert_universes univs u1 u2
+  | Cumulative_ind cumi ->
+    let num_param_arity =
+      mind.mind_nparams + mind.mind_packets.(ind).mind_nrealargs
+    in
+    if not (num_param_arity = sv1 && num_param_arity = sv2) then
+      convert_universes univs u1 u2
+    else
+      convert_inductive_instances cv_pb cumi u1 u2 univs
 
 let convert_constructors
     (mind, ind, cns) u1 sv1 u2 sv2 univs =
-  let num_cnstr_args =
-    let nparamsctxt =
-      mind.mind_nparams + mind.mind_packets.(ind).mind_nrealargs
+  match mind.mind_universes with
+  | Monomorphic_ind _ | Polymorphic_ind _ -> convert_universes univs u1 u2
+  | Cumulative_ind cumi ->
+    let num_cnstr_args =
+      let nparamsctxt =
+        mind.mind_nparams + mind.mind_packets.(ind).mind_nrealargs
+      in
+      nparamsctxt + mind.mind_packets.(ind).mind_consnrealargs.(cns - 1)
     in
-    nparamsctxt + mind.mind_packets.(ind).mind_consnrealargs.(cns - 1)
-  in
-  if not (num_cnstr_args = sv1 && num_cnstr_args = sv2) then
-    convert_universes univs u1 u2
-  else
-    let uinfind = mind.mind_universes in
-    convert_inductive_instances CONV uinfind u1 u2 univs
+    if not (num_cnstr_args = sv1 && num_cnstr_args = sv2) then
+      convert_universes univs u1 u2
+    else
+      convert_inductive_instances CONV cumi u1 u2 univs
 
 (* Convertibility of sorts *)
 
@@ -424,11 +433,8 @@ and eqappr univ cv_pb infos (lft1,st1) (lft2,st2) =
       if mind_equiv_infos infos ind1 ind2 then
         let mind = Environ.lookup_mind (fst ind1) (infos_env infos) in
         let () =
-          if mind.mind_polymorphic && mind.mind_cumulative then
-              convert_inductives cv_pb (mind, snd ind1) u1 (stack_args_size v1)
-                u2 (stack_args_size v2) univ
-          else
-            convert_universes univ u1 u2
+          convert_inductives cv_pb (mind, snd ind1) u1 (stack_args_size v1)
+            u2 (stack_args_size v2) univ
         in
         convert_stacks univ infos lft1 lft2 v1 v2
       else raise NotConvertible
@@ -437,12 +443,9 @@ and eqappr univ cv_pb infos (lft1,st1) (lft2,st2) =
       if Int.equal j1 j2 && mind_equiv_infos infos ind1 ind2 then
         let mind = Environ.lookup_mind (fst ind1) (infos_env infos) in
         let () =
-          if mind.mind_polymorphic && mind.mind_cumulative then
-            convert_constructors
-              (mind, snd ind1, j1) u1 (stack_args_size v1)
-              u2 (stack_args_size v2) univ
-          else
-            convert_universes univ u1 u2
+          convert_constructors
+            (mind, snd ind1, j1) u1 (stack_args_size v1)
+            u2 (stack_args_size v2) univ
         in
         convert_stacks univ infos lft1 lft2 v1 v2
       else raise NotConvertible