diff options
Diffstat (limited to 'checker/reduction.ml')
| -rw-r--r-- | checker/reduction.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/checker/reduction.ml b/checker/reduction.ml index 93b8b907c..0b605820d 100644 --- a/checker/reduction.ml +++ b/checker/reduction.ml @@ -157,11 +157,11 @@ let compare_stacks f fmind lft1 stk1 lft2 stk2 = else raise NotConvertible let convert_inductive_instances cv_pb cumi u u' univs = - let ind_instance = - Univ.AUContext.instance (Univ.ACumulativityInfo.univ_context cumi) in + let len_instance = + Univ.AUContext.size (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 ((len_instance = Univ.Instance.length u) && + (len_instance = Univ.Instance.length u')) then anomaly (Pp.str "Invalid inductive subtyping encountered!") else let comp_cst = |