diff options
Diffstat (limited to 'kernel/inductive.ml')
| -rw-r--r-- | kernel/inductive.ml | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 2c0865348e..ce12d65614 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -331,13 +331,16 @@ let check_allowed_sort ksort specif = raise (LocalArity (Some(elim_sort specif, ksort,s,error_elim_explain ksort s))) let check_correct_arity env c pj ind specif params = + (* We use l2r:true for compat with old versions which used CONV + instead of CUMUL called with arguments flipped. It is relevant + for performance eg in bedrock / Kami. *) let arsign,_ = get_instantiated_arity ind specif params in let rec srec env ar pt = let pt' = whd_all env pt in match ar, kind pt' with | (LocalAssum (_,a1))::ar', Prod (na1,a1',t) -> let () = - try conv_leq env a1 a1' + try conv_leq ~l2r:true env a1 a1' with NotConvertible -> raise (LocalArity None) in srec (push_rel (LocalAssum (na1,a1)) env) ar' t (* The last Prod domain is the type of the scrutinee *) @@ -351,7 +354,7 @@ let check_correct_arity env c pj ind specif params = let () = (* This ensures that the type of the scrutinee is <= the inductive type declared in the predicate. *) - try conv_leq env dep_ind a1' + try conv_leq ~l2r:true env dep_ind a1' with NotConvertible -> raise (LocalArity None) in let () = check_allowed_sort ksort specif in |