X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Fcic_proof_checking%2FcicTypeChecker.ml;h=d34c829199e506cf1925c46402104b9e43295a20;hb=233836d11a41951f0197523c75a317d1070d7c6e;hp=ad00c0eeb614bfc2ce958c9818386041a9fc084d;hpb=04d8e2282a3536a9b822a8dbfcbdb4e3a949f04d;p=helm.git

diff --git a/helm/software/components/cic_proof_checking/cicTypeChecker.ml b/helm/software/components/cic_proof_checking/cicTypeChecker.ml
index ad00c0eeb..d34c82919 100644
--- a/helm/software/components/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/software/components/cic_proof_checking/cicTypeChecker.ml
@@ -801,7 +801,7 @@ and check_is_really_smaller_arg ~subst context n nn kl x safes te =
                     | (_,_,ty,_)::_ ->
                        fst (split_prods ~subst [] paramsno ty)
                   in
-                   (tys@lefts,List.length tl,isinductive,paramsno,cl')
+                   (lefts@tys,List.length tl,isinductive,paramsno,cl')
              | _ ->
                 raise (TypeCheckerFailure
                   (lazy ("Unknown mutual inductive definition:" ^
@@ -852,7 +852,7 @@ and check_is_really_smaller_arg ~subst context n nn kl x safes te =
                     | (_,_,ty,_)::_ ->
                        fst (split_prods ~subst [] paramsno ty)
                   in
-                   (tys@lefts,List.length tl,isinductive,paramsno,cl')
+                   (lefts@tys,List.length tl,isinductive,paramsno,cl')
              | _ ->
                 raise (TypeCheckerFailure
                   (lazy ("Unknown mutual inductive definition:" ^
@@ -934,10 +934,10 @@ and guarded_by_destructors ~subst context n nn kl x safes =
   function
      C.Rel m when m > n && m <= nn -> false
    | C.Rel m ->
-      (match List.nth context (n-1) with
+      (match List.nth context (m-1) with
           Some (_,C.Decl _) -> true
         | Some (_,C.Def (bo,_)) ->
-           guarded_by_destructors ~subst context m nn kl x safes
+           guarded_by_destructors ~subst context n nn kl x safes
             (CicSubstitution.lift m bo)
         | None -> raise (TypeCheckerFailure (lazy "Reference to deleted hypothesis"))
       )
@@ -1006,7 +1006,7 @@ and guarded_by_destructors ~subst context n nn kl x safes =
                      | (_,_,ty,_)::_ ->
                         fst (split_prods ~subst [] paramsno ty)
                    in
-                    (tys@lefts,len,isinductive,paramsno,cl')
+                    (lefts@tys,len,isinductive,paramsno,cl')
              | _ ->
                 raise (TypeCheckerFailure
                   (lazy ("Unknown mutual inductive definition:" ^
@@ -1059,7 +1059,7 @@ and guarded_by_destructors ~subst context n nn kl x safes =
                     | (_,_,ty,_)::_ ->
                        fst (split_prods ~subst [] paramsno ty)
                   in
-                   (tys@lefts,List.length tl,isinductive,paramsno,cl')
+                   (lefts@tys,List.length tl,isinductive,paramsno,cl')
              | _ ->
                 raise (TypeCheckerFailure
                   (lazy ("Unknown mutual inductive definition:" ^
@@ -1647,6 +1647,7 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph =
    | C.LetIn (n,s,ty,t) ->
       (* only to check if s is well-typed *)
       let ty',ugraph1 = type_of_aux ~logger context s ugraph in
+      let _,ugraph1 = type_of_aux ~logger context ty ugraph1 in
       let b,ugraph1 =
        R.are_convertible ~subst ~metasenv context ty ty' ugraph1
       in 
@@ -2002,7 +2003,7 @@ end;
        let (_,ty,_) = List.nth fl i in
 	 ty,ugraph2
 
- and check_exp_named_subst ~logger ~subst context ugraph =
+ and check_exp_named_subst ~logger ~subst context =
    let rec check_exp_named_subst_aux ~logger esubsts l ugraph =
      match l with
 	 [] -> ugraph
@@ -2028,7 +2029,7 @@ end;
 		 raise (TypeCheckerFailure (lazy "Wrong Explicit Named Substitution"))
                end
    in
-     check_exp_named_subst_aux ~logger [] ugraph 
+     check_exp_named_subst_aux ~logger []
        
  and sort_of_prod ~subst context (name,s) (t1, t2) ugraph =
   let module C = Cic in