diff options
| author |  Amin Timany <amintimany@gmail.com> | 2017-06-15 16:50:05 +0200 |
|---|---|---|
| committer |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-06-16 04:52:11 +0200 |
| commit | 15b1856edd593b39d63d23584a4f5acec0eeb592 (patch) | |
| tree | 4233f58e213573b48bfd2692af758b30f385db7c /kernel/reduction.ml | |
| parent | a4969591f391d857a9efd038338e1a80fc68950b (diff) | |
Fix a bug in cumulativity
Diffstat (limited to 'kernel/reduction.ml')
| -rw-r--r-- | kernel/reduction.ml | 20 |
1 files changed, 11 insertions, 9 deletions
diff --git a/kernel/reduction.ml b/kernel/reduction.ml index a9e2ce78c..605e9f314 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -679,12 +679,13 @@ let infer_check_conv_constructors infer_check_inductive_instances CONV cumi u1 u2 univs let check_inductive_instances cv_pb cumi u u' univs = - let ind_instance = - Univ.AUContext.instance (Univ.ACumulativityInfo.univ_context cumi) + let length_ind_instance = + Univ.Instance.length + (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 + if not ((length_ind_instance = Univ.Instance.length u) && + (length_ind_instance = Univ.Instance.length u')) then anomaly (Pp.str "Invalid inductive subtyping encountered!") else let comp_cst = @@ -765,13 +766,14 @@ let infer_convert_instances ~flex u u' (univs,cstrs) = in (univs, cstrs') let infer_inductive_instances cv_pb cumi u u' (univs, cstrs) = - let ind_instance = - Univ.AUContext.instance (Univ.ACumulativityInfo.subtyp_context cumi) + let length_ind_instance = + Univ.Instance.length + (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!") + if not ((length_ind_instance = Univ.Instance.length u) && + (length_ind_instance = Univ.Instance.length u')) then + anomaly (Pp.str "Invalid inductive subtyping encountered!") else let comp_cst = let comp_subst = (Univ.Instance.append u u') in |