From a9f0fd89cf3bb4b728eb451572a96f8599211380 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 30 Jan 2019 14:39:28 +0100
Subject: Separate variance and universe fields in inductives.

I think the usage looks cleaner this way.
---
 kernel/reduction.ml | 22 +++++++---------------
 1 file changed, 7 insertions(+), 15 deletions(-)

(limited to 'kernel/reduction.ml')

diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 61051c001d..b583d33e29 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -244,18 +244,14 @@ let inductive_cumulativity_arguments (mind,ind) =
   mind.Declarations.mind_packets.(ind).Declarations.mind_nrealargs
 
 let convert_inductives_gen cmp_instances cmp_cumul cv_pb (mind,ind) nargs u1 u2 s =
-  match mind.Declarations.mind_universes with
-  | Declarations.Monomorphic_ind _ ->
-    assert (Univ.Instance.length u1 = 0 && Univ.Instance.length u2 = 0);
-    s
-  | Declarations.Polymorphic_ind _ ->
-    cmp_instances u1 u2 s
-  | Declarations.Cumulative_ind cumi ->
+  match mind.Declarations.mind_variance with
+  | None -> cmp_instances u1 u2 s
+  | Some variances ->
     let num_param_arity = inductive_cumulativity_arguments (mind,ind) in
     if not (Int.equal num_param_arity nargs) then
       cmp_instances u1 u2 s
     else
-      cmp_cumul cv_pb (Univ.ACumulativityInfo.variance cumi) u1 u2 s
+      cmp_cumul cv_pb variances u1 u2 s
 
 let convert_inductives cv_pb ind nargs u1 u2 (s, check) =
   convert_inductives_gen (check.compare_instances ~flex:false) check.compare_cumul_instances
@@ -266,13 +262,9 @@ let constructor_cumulativity_arguments (mind, ind, ctor) =
   mind.Declarations.mind_packets.(ind).Declarations.mind_consnrealargs.(ctor - 1)
 
 let convert_constructors_gen cmp_instances cmp_cumul (mind, ind, cns) nargs u1 u2 s =
-  match mind.Declarations.mind_universes with
-  | Declarations.Monomorphic_ind _ ->
-    assert (Univ.Instance.length u1 = 0 && Univ.Instance.length u2 = 0);
-    s
-  | Declarations.Polymorphic_ind _ ->
-    cmp_instances u1 u2 s
-  | Declarations.Cumulative_ind _cumi ->
+  match mind.Declarations.mind_variance with
+  | None -> cmp_instances u1 u2 s
+  | Some _ ->
     let num_cnstr_args = constructor_cumulativity_arguments (mind,ind,cns) in
     if not (Int.equal num_cnstr_args nargs) then
       cmp_instances u1 u2 s
-- 
cgit v1.2.3