some fixes for guardness conditions

diff --git a/helm/software/components/cic_proof_checking/cicTypeChecker.ml b/helm/software/components/cic_proof_checking/cicTypeChecker.ml
index 787a0cb3c02e6c8549deb29a4793420c3b591055..5f1c933f2f0e295e03904c6ca05348012f09dae8 100644 (file)
--- a/helm/software/components/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/software/components/cic_proof_checking/cicTypeChecker.ml
@@ -748,9 +748,8 @@ and check_is_really_smaller_arg ~subst context n nn kl x safes te =
    delta only on-demand when it fails without *)
  match CicReduction.whd ~subst context te with
      C.Rel m when List.mem m safes -> true
-   | C.Rel _ -> false
-   | C.Appl (he::_) ->
-      check_is_really_smaller_arg ~subst context n nn kl x safes he
+   | C.Rel _ 
+   | C.Appl _
    | C.MutConstruct _
    | C.Const _
    | C.Var _ -> false
@@ -791,27 +790,19 @@ and check_is_really_smaller_arg ~subst context n nn kl x safes te =
                  i && check_is_really_smaller_arg ~subst context n nn kl x safes p)
                pl true
             else
-             let pl_and_cl =
-              try
-               List.combine pl cl
-              with
-               Invalid_argument _ ->
-                raise (TypeCheckerFailure (lazy "not enough patterns"))
-             in
-              (*CSC: supponiamo come prima che nessun controllo sia necessario*)
-              (*CSC: sugli argomenti di una applicazione                      *)
-              List.fold_right
-               (fun (p,(_,c)) i ->
+              List.for_all2
+               (fun p (_,c) ->
                  let rl' =
                   let debrujinedte = debrujin_constructor uri len c in
-                   recursive_args lefts_and_tys 0 len debrujinedte
+                   recursive_args lefts_and_tys paramsno 
+                     (len+paramsno) debrujinedte
                  in
                   let (e, safes',n',nn',x',context') =
                    get_new_safes ~subst context p c rl' safes n nn x
                   in
-                   i &&
-                   check_is_really_smaller_arg ~subst context' n' nn' kl x' safes' e
-               ) pl_and_cl true
+                  check_is_really_smaller_arg 
+                    ~subst context' n' nn' kl x' safes' e
+               ) pl cl
         | _ ->
           List.fold_right
            (fun p i ->
@@ -940,7 +931,8 @@ and guarded_by_destructors ~subst context n nn kl x safes t =
               List.fold_right
                (fun (p,(name,c,brujinedc)) i ->
                    i &&
-                 let rl' = recursive_args lefts_and_tys 0 len brujinedc in
+                 let rl' = recursive_args 
+                   lefts_and_tys paramsno (len+paramsno) brujinedc in
                   let (e,safes',n',nn',x',context') =
                    get_new_safes ~subst context p c rl' safes n nn x
                   in
@@ -998,7 +990,8 @@ and guarded_by_destructors ~subst context n nn kl x safes t =
                (fun (p,(_,c)) i ->
                  let rl' =
                   let debrujinedte = debrujin_constructor uri len c in
-                   recursive_args lefts_and_tys 0 len debrujinedte
+                   recursive_args lefts_and_tys paramsno 
+                     (len+paramsno) debrujinedte
                  in
                   let (e, safes',n',nn',x',context') =
                    get_new_safes ~subst context p c rl' safes n nn x