Merge PR #13531: [kernel]Use ~l2r:true to restore previous order of unfolding

Reviewed-by: SkySkimmer
Ack-by: ppedrot

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