X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_proof_checking%2FcicTypeChecker.ml;h=2855367002ef063677589e455b143d5727453ffa;hb=c59d5065faea77ce41431e273a3331f4d152fbfa;hp=ab43c3732ee6b1b572bfb66ed486ecd8439e7838;hpb=442c8011ba8aca1a0f37226bfe3033a220bb71e3;p=helm.git

diff --git a/helm/software/components/cic_proof_checking/cicTypeChecker.ml b/helm/software/components/cic_proof_checking/cicTypeChecker.ml
index ab43c3732..285536700 100644
--- a/helm/software/components/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/software/components/cic_proof_checking/cicTypeChecker.ml
@@ -391,13 +391,8 @@ and weakly_positive context n nn uri te =
 *)
      C.Appl ((C.MutInd (uri',_,_))::tl) when UriManager.eq uri' uri -> true
    | C.MutInd (uri',0,_) when UriManager.eq uri' uri -> true
-   | C.Prod (C.Anonymous,source,dest) ->
-      strictly_positive context n nn
-       (subst_inductive_type_with_dummy_mutind source) &&
-       weakly_positive ((Some (C.Anonymous,(C.Decl source)))::context)
-        (n + 1) (nn + 1) uri dest
    | C.Prod (name,source,dest) when
-      does_not_occur ((Some (name,(C.Decl source)))::context) 0 n dest ->
+      does_not_occur ((Some (name,(C.Decl source)))::context) 0 1 dest ->
        (* dummy abstraction, so we behave as in the anonimous case *)
        strictly_positive context n nn
         (subst_inductive_type_with_dummy_mutind source) &&
@@ -437,7 +432,9 @@ and strictly_positive context n nn te =
        strictly_positive ((Some (name,(C.Decl so)))::context) (n+1) (nn+1) ta
    | C.Appl ((C.Rel m)::tl) when m > n && m <= nn ->
       List.fold_right (fun x i -> i && does_not_occur context n nn x) tl true
-   | C.Appl ((C.MutInd (uri,i,exp_named_subst))::tl) -> 
+   | C.Appl ((C.MutInd (uri,i,exp_named_subst))::_) 
+   | (C.MutInd (uri,i,exp_named_subst)) as t -> 
+      let tl = match t with C.Appl (_::tl) -> tl | _ -> [] in
       let (ok,paramsno,ity,cl,name) =
 	let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
 	  match o with
@@ -508,14 +505,8 @@ and are_all_occurrences_positive context uri indparamsno i n nn te =
         raise (TypeCheckerFailure
          (lazy ("Non-positive occurence in mutual inductive definition(s) [3]"^
           UriManager.string_of_uri uri)))
-   | C.Prod (C.Anonymous,source,dest) ->
-       let b = strictly_positive context n nn source in
-       b &&
-       are_all_occurrences_positive
-        ((Some (C.Anonymous,(C.Decl source)))::context) uri indparamsno
-        (i+1) (n + 1) (nn + 1) dest
    | C.Prod (name,source,dest) when
-      does_not_occur ((Some (name,(C.Decl source)))::context) 0 n dest ->
+      does_not_occur ((Some (name,(C.Decl source)))::context) 0 1 dest ->
       (* dummy abstraction, so we behave as in the anonimous case *)
       strictly_positive context n nn source &&
        are_all_occurrences_positive
@@ -2003,7 +1994,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
@@ -2029,7 +2020,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