diff options
| author | Gaëtan Gilbert | 2019-01-30 14:39:28 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-02-17 15:44:30 +0100 |
| commit | a9f0fd89cf3bb4b728eb451572a96f8599211380 (patch) | |
| tree | 577b7330af67793041cfaba8414005f93fc49c88 /kernel/reduction.ml | |
| parent | a49077ef67b8e70696ecacc311fc3070d1b7b461 (diff) | |
Separate variance and universe fields in inductives.
I think the usage looks cleaner this way.
Diffstat (limited to 'kernel/reduction.ml')
| -rw-r--r-- | kernel/reduction.ml | 22 |
1 files changed, 7 insertions, 15 deletions
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 |