Bug fixed in the guarded_by_descructors function: in some cases the context

was missing the left arguments! This is the first bug found in the kernel
after quite a long time.

diff --git a/helm/software/components/cic_proof_checking/cicTypeChecker.ml b/helm/software/components/cic_proof_checking/cicTypeChecker.ml
index c0e90a5c6a20157284bf9de115611da4bef94bf6..81b33b0d198f7b6c958c9055c1dbedee84d7f29f 100644 (file)
--- a/helm/software/components/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/software/components/cic_proof_checking/cicTypeChecker.ml
@@ -952,7 +952,7 @@ and guarded_by_destructors ~subst context n nn kl x safes =
    | C.MutCase (uri,i,outtype,term,pl) ->
       (match CicReduction.whd ~subst context 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,_) ->
@@ -968,9 +968,14 @@ and guarded_by_destructors ~subst context n nn kl x safes =
                       let debrujinedty = debrujin_constructor uri len ty in
                        (id, snd (split_prods ~subst tys paramsno ty),
                         snd (split_prods ~subst tys paramsno debrujinedty)
-                       )) cl
+                       )) cl in
+                   let lefts =
+                    match tl with
+                       [] -> assert false
+                     | (_,_,ty,_)::_ ->
+                        fst (split_prods ~subst [] paramsno ty)
                    in
-                    (tys,len,isinductive,paramsno,cl')
+                    (tys@lefts,len,isinductive,paramsno,cl')
              | _ ->
                 raise (TypeCheckerFailure
                   (lazy ("Unknown mutual inductive definition:" ^
@@ -996,7 +1001,7 @@ and guarded_by_destructors ~subst context n nn kl x safes =
               (*CSC: manca ??? il controllo sul tipo di term? *)
               List.fold_right
                (fun (p,(_,c,brujinedc)) i ->
-                 let rl' = recursive_args tys 0 len brujinedc in
+                 let rl' = recursive_args lefts_and_tys 0 len brujinedc in
                   let (e,safes',n',nn',x',context') =
                    get_new_safes ~subst context p c rl' safes n nn x
                   in
@@ -1004,7 +1009,7 @@ and guarded_by_destructors ~subst context n nn kl x safes =
                    guarded_by_destructors ~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,_) ->
@@ -1016,9 +1021,14 @@ and guarded_by_destructors ~subst context n nn kl x safes =
                   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:" ^
@@ -1050,7 +1060,7 @@ and guarded_by_destructors ~subst context n nn kl x safes =
                (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