From 0d884e0852ae388becc5b74c6a8cb30088f7b79b Mon Sep 17 00:00:00 2001
From: Amin Timany <amintimany@gmail.com>
Date: Sat, 8 Apr 2017 16:10:19 +0200
Subject: Fix cum/conv for inductive types

Fall back to the equating levels in case inductive is not fully applied
instead of failing.
---
 kernel/reduction.ml | 24 ++++++++++++++----------
 1 file changed, 14 insertions(+), 10 deletions(-)

(limited to 'kernel/reduction.ml')

diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 0d2399e02..c8fad60eb 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -492,24 +492,28 @@ and eqappr env cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
         if eq_ind ind1 ind2
 	then
         begin
+          let fall_back () =
+            let cuniv = convert_instances ~flex:false u1 u2 cuniv in
+            convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv
+          in
           let mind = Environ.lookup_mind (fst ind1) env in
           if mind.Declarations.mind_polymorphic then
           begin
             let num_param_arity =
               Context.Rel.length (mind.Declarations.mind_packets.(snd ind1).Declarations.mind_arity_ctxt)
             in
-            (if not (num_param_arity = CClosure.stack_args_size v1 && num_param_arity = CClosure.stack_args_size v2) then
-               raise NotConvertible else ());
-            let uinfind = mind.Declarations.mind_universes in
-	    let cuniv = compare_leq_inductives ~flex:false uinfind u1 u2 cuniv in
-            let cuniv = if cv_pb = CONV then compare_leq_inductives ~flex:false uinfind u2 u1 cuniv else cuniv in
-            convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv
+            if not (num_param_arity = CClosure.stack_args_size v1 && num_param_arity = CClosure.stack_args_size v2) then
+              fall_back ()
+            else
+            begin
+              let uinfind = mind.Declarations.mind_universes in
+              let cuniv = compare_leq_inductives ~flex:false uinfind u1 u2 cuniv in
+              let cuniv = if cv_pb = CONV then compare_leq_inductives ~flex:false uinfind u2 u1 cuniv else cuniv in
+              convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv
+            end
           end
           else
-          begin
-            let cuniv = convert_instances ~flex:false u1 u2 cuniv in
-            convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv
-          end
+            fall_back ()
         end
         else raise NotConvertible
 
-- 
cgit v1.2.3