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 /engine/eConstr.ml | |
| parent | a49077ef67b8e70696ecacc311fc3070d1b7b461 (diff) | |
Separate variance and universe fields in inductives.
I think the usage looks cleaner this way.
Diffstat (limited to 'engine/eConstr.ml')
| -rw-r--r-- | engine/eConstr.ml | 20 |
1 files changed, 6 insertions, 14 deletions
diff --git a/engine/eConstr.ml b/engine/eConstr.ml index 8493119ee5..8756ebfdf2 100644 --- a/engine/eConstr.ml +++ b/engine/eConstr.ml @@ -405,25 +405,17 @@ let compare_cumulative_instances cv_pb nargs_ok variances u u' cstrs = let cmp_inductives cv_pb (mind,ind as spec) nargs u1 u2 cstrs = let open UnivProblem in - match mind.Declarations.mind_universes with - | Declarations.Monomorphic_ind _ -> - assert (Univ.Instance.length u1 = 0 && Univ.Instance.length u2 = 0); - cstrs - | Declarations.Polymorphic_ind _ -> - enforce_eq_instances_univs false u1 u2 cstrs - | Declarations.Cumulative_ind cumi -> + match mind.Declarations.mind_variance with + | None -> enforce_eq_instances_univs false u1 u2 cstrs + | Some variances -> let num_param_arity = Reduction.inductive_cumulativity_arguments spec in - let variances = Univ.ACumulativityInfo.variance cumi in compare_cumulative_instances cv_pb (Int.equal num_param_arity nargs) variances u1 u2 cstrs let cmp_constructors (mind, ind, cns as spec) nargs u1 u2 cstrs = let open UnivProblem in - match mind.Declarations.mind_universes with - | Declarations.Monomorphic_ind _ -> - cstrs - | Declarations.Polymorphic_ind _ -> - enforce_eq_instances_univs false u1 u2 cstrs - | Declarations.Cumulative_ind cumi -> + match mind.Declarations.mind_variance with + | None -> enforce_eq_instances_univs false u1 u2 cstrs + | Some _ -> let num_cnstr_args = Reduction.constructor_cumulativity_arguments spec in if not (Int.equal num_cnstr_args nargs) then enforce_eq_instances_univs false u1 u2 cstrs |