From baaa28f921e8ed2045acb14da94f2c8e1701fa1f Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 1 Dec 2020 11:53:36 +0100
Subject: Added comment about l2r in check_correct_arity

---
 kernel/inductive.ml | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'kernel')

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
-- 
cgit v1.2.3