diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-03-09 13:20:54 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-03-09 16:30:12 +0100 |
| commit | 65cba7c6cb1016df13e948452f1e3cb58edcb996 (patch) | |
| tree | e70a8f42e040b0382db09e71c8a93c3682a683aa /engine | |
| parent | af5eded304b74fa0fccb35a7dc284c46a96ba5cc (diff) | |
Adjust EConstr.cmp_constructors for relaxed constructor cumulativity
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/eConstr.ml | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/engine/eConstr.ml b/engine/eConstr.ml index 3ee072214..bd47a04f1 100644 --- a/engine/eConstr.ml +++ b/engine/eConstr.ml @@ -613,8 +613,11 @@ let cmp_constructors (mind, ind, cns as spec) nargs u1 u2 cstrs = enforce_eq_instances_univs false u1 u2 cstrs | Declarations.Cumulative_ind cumi -> let num_cnstr_args = Reduction.constructor_cumulativity_arguments spec in - let variances = Univ.ACumulativityInfo.variance cumi in - compare_cumulative_instances Reduction.CONV (Int.equal num_cnstr_args nargs) variances u1 u2 cstrs + if not (Int.equal num_cnstr_args nargs) + then enforce_eq_instances_univs false u1 u2 cstrs + else + Array.fold_left2 (fun cstrs u1 u2 -> Universes.(Constraints.add (UWeak (u1,u2)) cstrs)) + cstrs (Univ.Instance.to_array u1) (Univ.Instance.to_array u2) let eq_universes env sigma cstrs cv_pb ref nargs l l' = if Univ.Instance.is_empty l then (assert (Univ.Instance.is_empty l'); true) |