From c8b4fe261c80f5cb8b9bf998495996c469783ba6 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 12 Sep 2006 17:52:57 +0000
Subject: [PATCH] Possible bug fixed (similar to the previous one, but in
 another similar function).

---
 .../cic_proof_checking/cicTypeChecker.ml      | 26 +++++++++++++------
 1 file changed, 18 insertions(+), 8 deletions(-)

diff --git a/components/cic_proof_checking/cicTypeChecker.ml b/components/cic_proof_checking/cicTypeChecker.ml
index 81b33b0d1..7e2715d0a 100644
--- a/components/cic_proof_checking/cicTypeChecker.ml
+++ b/components/cic_proof_checking/cicTypeChecker.ml
@@ -772,7 +772,7 @@ and check_is_really_smaller_arg ~subst context n nn kl x safes te =
    | C.MutCase (uri,i,outtype,term,pl) ->
       (match term with
           C.Rel m when List.mem m safes || m = x ->
-           let (tys,len,isinductive,paramsno,cl) =
+           let (lefts_and_tys,len,isinductive,paramsno,cl) =
 	    let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
             match o with
                C.InductiveDefinition (tl,_,paramsno,_) ->
@@ -784,9 +784,14 @@ and check_is_really_smaller_arg ~subst context n nn kl x safes te =
                   let cl' =
                    List.map
                     (fun (id,ty) ->
-                      (id, snd (split_prods ~subst tys paramsno ty))) cl
+                      (id, snd (split_prods ~subst tys paramsno ty))) cl in
+                  let lefts =
+                   match tl with
+                      [] -> assert false
+                    | (_,_,ty,_)::_ ->
+                       fst (split_prods ~subst [] paramsno ty)
                   in
-                   (tys,List.length tl,isinductive,paramsno,cl')
+                   (tys@lefts,List.length tl,isinductive,paramsno,cl')
              | _ ->
                 raise (TypeCheckerFailure
                   (lazy ("Unknown mutual inductive definition:" ^
@@ -809,7 +814,7 @@ and check_is_really_smaller_arg ~subst context n nn kl x safes te =
                (fun (p,(_,c)) i ->
                  let rl' =
                   let debrujinedte = debrujin_constructor uri len c in
-                   recursive_args tys 0 len debrujinedte
+                   recursive_args lefts_and_tys 0 len debrujinedte
                  in
                   let (e,safes',n',nn',x',context') =
                    get_new_safes ~subst context p c rl' safes n nn x
@@ -818,7 +823,7 @@ and check_is_really_smaller_arg ~subst context n nn kl x safes te =
                    check_is_really_smaller_arg ~subst context' n' nn' kl x' safes' e
                ) pl_and_cl true
         | C.Appl ((C.Rel m)::tl) when List.mem m safes || m = x ->
-           let (tys,len,isinductive,paramsno,cl) =
+           let (lefts_and_tys,len,isinductive,paramsno,cl) =
             let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
             match o with
                C.InductiveDefinition (tl,_,paramsno,_) ->
@@ -830,9 +835,14 @@ and check_is_really_smaller_arg ~subst context n nn kl x safes te =
                   let cl' =
                    List.map
                     (fun (id,ty) ->
-                      (id, snd (split_prods ~subst tys paramsno ty))) cl
+                      (id, snd (split_prods ~subst tys paramsno ty))) cl in
+                  let lefts =
+                   match tl with
+                      [] -> assert false
+                    | (_,_,ty,_)::_ ->
+                       fst (split_prods ~subst [] paramsno ty)
                   in
-                   (tys,List.length tl,isinductive,paramsno,cl')
+                   (tys@lefts,List.length tl,isinductive,paramsno,cl')
              | _ ->
                 raise (TypeCheckerFailure
                   (lazy ("Unknown mutual inductive definition:" ^
@@ -857,7 +867,7 @@ and check_is_really_smaller_arg ~subst context n nn kl x safes te =
                (fun (p,(_,c)) i ->
                  let rl' =
                   let debrujinedte = debrujin_constructor uri len c in
-                   recursive_args tys 0 len debrujinedte
+                   recursive_args lefts_and_tys 0 len debrujinedte
                  in
                   let (e, safes',n',nn',x',context') =
                    get_new_safes ~subst context p c rl' safes n nn x
-- 
2.39.2