From 36e2df30d23d56f0a80adcd3ed5c04d64117af74 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Tue, 1 Dec 2020 08:57:54 +0100
Subject: Use ~l2r:true to restore previous order of unfolding when typing
 predicates of cases.

---
 kernel/inductive.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'kernel/inductive.ml')

diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 2c0865348e..83e31a1881 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -337,7 +337,7 @@ let check_correct_arity env c pj ind specif params =
     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 +351,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
-- 
cgit v1.2.3