Added comment about l2r in check_correct_arity

1 files changed, 3 insertions, 0 deletions

diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 83e31a1881..ce12d65614 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -331,6 +331,9 @@ 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