X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FnCicTypeChecker.ml;h=c68982ff7dddea804aba27eeb53b8f478d62cfdf;hb=341a777b344e7adb1e989dda3fdd643a3d9fb5f5;hp=5daea200c976f366fa55cc0e366adcb23bcd160b;hpb=a3b43762ca9cfb746933dcd991bfc363b5fdd9b7;p=helm.git

diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml
index 5daea200c..c68982ff7 100644
--- a/helm/software/components/ng_kernel/nCicTypeChecker.ml
+++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml
@@ -138,8 +138,6 @@ let sort_of_prod ~metasenv ~subst context (name,s) (t1, t2) =
          (PP.ppterm ~subst ~metasenv ~context t2))))
 ;;
 
-(* REMINDER: eat_prods was here *)
-
 (* instantiate_parameters ps (x1:T1)...(xn:Tn)C                             *)
 (* returns ((x_|ps|:T_|ps|)...(xn:Tn)C){ps_1 / x1 ; ... ; ps_|ps| / x_|ps|} *)
 let rec instantiate_parameters params c =
@@ -226,50 +224,73 @@ let rec eat_or_subst_lambdas
   | (_, te, _, _) -> te, k
 ;;
 
+let check_homogeneous_call ~subst context indparamsno n uri reduct tl =
+ let last =
+  List.fold_left
+   (fun k x ->
+     if k = 0 then 0
+     else
+      match R.whd context x with
+      | C.Rel m when m = n - (indparamsno - k) -> k - 1
+      | _ -> raise (TypeCheckerFailure (lazy 
+         ("Argument "^string_of_int (indparamsno - k + 1) ^ " (of " ^
+         string_of_int indparamsno ^ " fixed) is not homogeneous in "^
+         "appl:\n"^ PP.ppterm ~context ~subst ~metasenv:[] reduct))))
+   indparamsno tl
+ in
+  if last <> 0 then
+   raise (TypeCheckerFailure
+    (lazy ("Non-positive occurence in mutual inductive definition(s) [2]"^
+     NUri.string_of_uri uri)))
+;;
 
-(*CSC l'indice x dei tipi induttivi e' t.c. n < x <= nn *)
-(*CSC questa funzione e' simile alla are_all_occurrences_positive, ma fa *)
-(*CSC dei controlli leggermente diversi. Viene invocata solamente dalla  *)
-(*CSC strictly_positive                                                  *)
-(*CSC definizione (giusta???) tratta dalla mail di Hugo ;-)              *)
-let rec weakly_positive ~subst context n nn uri te =
-(*CSC: Che schifo! Bisogna capire meglio e trovare una soluzione ragionevole!*)
+(* Inductive types being checked for positivity have *)
+(* indexes x s.t. n < x <= nn.                       *)
+let rec weakly_positive ~subst context n nn uri indparamsno posuri te =
+  (*CSC: Not very nice. *)
   let dummy = C.Sort C.Prop in
-  (*CSC: mettere in cicSubstitution *)
+  (*CSC: to be moved in cicSubstitution? *)
   let rec subst_inductive_type_with_dummy _ = function
     | C.Const (Ref.Ref (uri',Ref.Ind (true,0,_))) when NUri.eq uri' uri -> dummy
-    | C.Appl ((C.Const (Ref.Ref (uri',Ref.Ind (true,0,_))))::_) 
-        when NUri.eq uri' uri -> dummy
+    | C.Appl ((C.Const (Ref.Ref (uri',Ref.Ind (true,0,lno))))::tl) 
+        when NUri.eq uri' uri -> 
+          let _, rargs = HExtlib.split_nth lno tl in
+          if rargs = [] then dummy else C.Appl (dummy :: rargs)
     | t -> U.map (fun _ x->x) () subst_inductive_type_with_dummy t
   in
-  match R.whd context te with
-   | C.Const (Ref.Ref (uri',Ref.Ind _))
-   | C.Appl ((C.Const (Ref.Ref (uri',Ref.Ind _)))::_) 
-      when NUri.eq uri' uri -> true
-   | C.Prod (name,source,dest) when
-      does_not_occur ~subst ((name,C.Decl source)::context) 0 1 dest ->
-       (* dummy abstraction, so we behave as in the anonimous case *)
-       strictly_positive ~subst context n nn
-        (subst_inductive_type_with_dummy () source) &&
-       weakly_positive ~subst ((name,C.Decl source)::context)
-        (n + 1) (nn + 1) uri dest
-   | C.Prod (name,source,dest) ->
-       does_not_occur ~subst context n nn
-        (subst_inductive_type_with_dummy () source)&&
-       weakly_positive ~subst ((name,C.Decl source)::context)
-        (n + 1) (nn + 1) uri dest
-   | _ ->
-     raise (TypeCheckerFailure (lazy "Malformed inductive constructor type"))
+  (* this function has the same semantics of are_all_occurrences_positive
+     but the i-th context entry role is played by dummy and some checks
+     are skipped because we already know that are_all_occurrences_positive
+     of uri in te. *)
+  let rec aux context n nn te =
+    match R.whd context te with
+     | t when t = dummy -> true
+     | C.Appl (te::rargs) when te = dummy ->
+        List.for_all (does_not_occur ~subst context n nn) rargs
+     | C.Prod (name,source,dest) when
+        does_not_occur ~subst ((name,C.Decl source)::context) 0 1 dest ->
+         (* dummy abstraction, so we behave as in the anonimous case *)
+         strictly_positive ~subst context n nn indparamsno posuri source &&
+         aux ((name,C.Decl source)::context) (n + 1) (nn + 1) dest
+     | C.Prod (name,source,dest) ->
+         does_not_occur ~subst context n nn source &&
+         aux ((name,C.Decl source)::context) (n + 1) (nn + 1) dest
+     | _ ->
+       raise (TypeCheckerFailure (lazy "Malformed inductive constructor type"))
+   in
+     aux context n nn (subst_inductive_type_with_dummy () te)
 
-and strictly_positive ~subst context n nn te =
+and strictly_positive ~subst context n nn indparamsno posuri te =
   match R.whd context te with
    | t when does_not_occur ~subst context n nn t -> true
-   | C.Rel _ -> true
+   | C.Rel _ when indparamsno = 0 -> true
+   | C.Appl ((C.Rel m)::tl) as reduct when m > n && m <= nn ->
+      check_homogeneous_call ~subst context indparamsno n posuri reduct tl;
+      List.for_all (does_not_occur ~subst context n nn) tl
    | C.Prod (name,so,ta) ->
       does_not_occur ~subst context n nn so &&
-       strictly_positive ~subst ((name,C.Decl so)::context) (n+1) (nn+1) ta
-   | C.Appl ((C.Rel m)::tl) when m > n && m <= nn ->
-      List.for_all (does_not_occur ~subst context n nn) tl
+       strictly_positive ~subst ((name,C.Decl so)::context) (n+1) (nn+1)
+        indparamsno posuri ta
    | C.Appl (C.Const (Ref.Ref (uri,Ref.Ind _) as r)::tl) -> 
       let _,paramsno,tyl,_,i = E.get_checked_indtys r in
       let _,name,ity,cl = List.nth tyl i in
@@ -282,32 +303,16 @@ and strictly_positive ~subst context n nn te =
       ok &&
       List.for_all (does_not_occur ~subst context n nn) arguments &&
       List.for_all 
-       (weakly_positive ~subst ((name,C.Decl ity)::context) (n+1) (nn+1) uri) cl
+       (weakly_positive ~subst ((name,C.Decl ity)::context) (n+1) (nn+1)
+         uri indparamsno posuri) cl
    | _ -> false
        
 (* the inductive type indexes are s.t. n < x <= nn *)
 and are_all_occurrences_positive ~subst context uri indparamsno i n nn te =
   match R.whd context te with
   |  C.Appl ((C.Rel m)::tl) as reduct when m = i ->
-      let last =
-       List.fold_left
-        (fun k x ->
-          if k = 0 then 0
-          else
-           match R.whd context x with
-           | C.Rel m when m = n - (indparamsno - k) -> k - 1
-           | _ -> raise (TypeCheckerFailure (lazy 
-              ("Argument "^string_of_int (indparamsno - k + 1) ^ " (of " ^
-              string_of_int indparamsno ^ " fixed) is not homogeneous in "^
-              "appl:\n"^ PP.ppterm ~context ~subst ~metasenv:[] reduct))))
-        indparamsno tl
-      in
-       if last = 0 then
-        List.for_all (does_not_occur ~subst context n nn) tl
-       else
-        raise (TypeCheckerFailure
-         (lazy ("Non-positive occurence in mutual inductive definition(s) [2]"^
-          NUri.string_of_uri uri)))
+      check_homogeneous_call ~subst context indparamsno n uri reduct tl;
+      List.for_all (does_not_occur ~subst context n nn) tl
   | C.Rel m when m = i ->
       if indparamsno = 0 then
        true
@@ -315,9 +320,9 @@ and are_all_occurrences_positive ~subst context uri indparamsno i n nn te =
         raise (TypeCheckerFailure
          (lazy ("Non-positive occurence in mutual inductive definition(s) [3]"^
           NUri.string_of_uri uri)))
-  | C.Prod (name,source,dest) when
+   | C.Prod (name,source,dest) when
       does_not_occur ~subst ((name,C.Decl source)::context) 0 1 dest ->
-      strictly_positive ~subst context n nn source &&
+      strictly_positive ~subst context n nn indparamsno uri source &&
        are_all_occurrences_positive ~subst 
         ((name,C.Decl source)::context) uri indparamsno
         (i+1) (n + 1) (nn + 1) dest
@@ -328,7 +333,6 @@ and are_all_occurrences_positive ~subst context uri indparamsno i n nn te =
        are_all_occurrences_positive ~subst ((name,C.Decl source)::context)
         uri indparamsno (i+1) (n + 1) (nn + 1) dest
    | _ ->
-prerr_endline ("MM: " ^ NCicPp.ppterm ~subst ~metasenv:[] ~context te);
      raise
       (TypeCheckerFailure (lazy ("Malformed inductive constructor type " ^
         (NUri.string_of_uri uri))))
@@ -628,15 +632,16 @@ let rec typeof ~subst ~metasenv context term =
          * have them already *)
                 let _,leftno,itl,_,i = E.get_checked_indtys r in
                 let itl_len = List.length itl in
-                let _,_,_,cl = List.nth itl i in
+                let _,itname,ittype,cl = List.nth itl i in
                 let cl_len = List.length cl in
-                 (* is it a singleton or empty non recursive and non informative
-                    definition? *)
+                 (* is it a singleton, non recursive and non informative
+                    definition or an empty one? *)
                  if not
                   (cl_len = 0 ||
                    (itl_len = 1 && cl_len = 1 &&
-                    is_non_informative leftno
-                     (let _,_,x = List.hd cl in x)))
+                    let _,_,constrty = List.hd cl in
+                      is_non_recursive_singleton r itname ittype constrty &&
+                      is_non_informative leftno constrty))
                  then
                   raise (TypeCheckerFailure (lazy
                    ("Sort elimination not allowed")));
@@ -681,6 +686,11 @@ and eat_prods ~subst ~metasenv context he ty_he args_with_ty =
   in
     aux ty_he args_with_ty
 
+and is_non_recursive_singleton (Ref.Ref (uri,_)) iname ity cty =
+     let ctx = [iname, C.Decl ity] in
+     let cty = debruijn uri 1 [] cty in
+     does_not_occur ~subst:[] ctx 0 1 cty
+
 and is_non_informative paramsno c =
  let rec aux context c =
    match R.whd context c with
@@ -691,7 +701,6 @@ and is_non_informative paramsno c =
  let context',dx = split_prods ~subst:[] [] paramsno c in
   aux context' dx
 
-
 and check_mutual_inductive_defs uri ~metasenv ~subst leftno tyl = 
   (* let's check if the arity of the inductive types are well formed *)
   List.iter (fun (_,_,x,_) -> ignore (typeof ~subst ~metasenv [] x)) tyl;
@@ -700,11 +709,12 @@ and check_mutual_inductive_defs uri ~metasenv ~subst leftno tyl =
   let tys = List.rev_map (fun (_,n,ty,_) -> (n,(C.Decl ty))) tyl in
   ignore
    (List.fold_right
-    (fun (_,_,ty,cl) i ->
+    (fun (it_relev,_,ty,cl) i ->
        let context,ty_sort = split_prods ~subst [] ~-1 ty in
        let sx_context_ty_rev,_ = HExtlib.split_nth leftno (List.rev context) in
        List.iter
-         (fun (_,_,te) -> 
+         (fun (k_relev,_,te) ->
+	   let _,k_relev = HExtlib.split_nth leftno k_relev in
            let te = debruijn uri len [] te in
            let context,te = split_prods ~subst tys leftno te in
            let _,chopped_context_rev =
@@ -755,11 +765,42 @@ and check_mutual_inductive_defs uri ~metasenv ~subst leftno tyl =
            then
              raise
                (TypeCheckerFailure
-                 (lazy ("Non positive occurence in "^NUri.string_of_uri uri))))
+                 (lazy ("Non positive occurence in "^NUri.string_of_uri
+		 uri)))
+           else check_relevance ~subst ~metasenv context k_relev te) 
          cl;
-        i + 1)
+        check_relevance ~subst ~metasenv [] it_relev ty;
+	i+1)
     tyl 1)
 
+and check_relevance ~subst ~metasenv context relevance ty =
+  let error context ty =
+    raise (TypeCheckerFailure 
+     (lazy ("Wrong relevance declaration: " ^ 
+     String.concat "," (List.map string_of_bool relevance)^ 
+     "\nfor type: "^PP.ppterm ~metasenv ~subst ~context ty)))
+  in
+  let rec aux context relevance ty =
+    match R.whd ~subst context ty with
+    | C.Prod (name,so,de) ->
+        let sort = typeof ~subst ~metasenv context so in
+        (match (relevance,R.whd ~subst context sort) with
+	  | [],_ -> ()
+          | false::tl,C.Sort C.Prop -> aux ((name,(C.Decl so))::context) tl de
+	  | true::_,C.Sort C.Prop
+	  | false::_,C.Sort _
+          | false::_,C.Meta _ -> error context ty
+          | true::tl,C.Sort _
+          | true::tl,C.Meta _ -> aux ((name,(C.Decl so))::context) tl de
+          | _ -> raise (AssertFailure (lazy (Printf.sprintf
+                 "Prod: the type %s of the source of %s is not a sort"
+                  (PP.ppterm ~subst ~metasenv ~context sort)
+                  (PP.ppterm ~subst ~metasenv ~context so)))))
+    | _ -> (match relevance with
+      | [] -> ()
+      | _::_ -> error context ty)
+  in aux context relevance ty
+
 and guarded_by_destructors r_uri r_len ~subst ~metasenv context recfuns t = 
  let recursor f k t = U.fold shift_k k (fun k () -> f k) () t in
  let rec aux (context, recfuns, x as k) t = 
@@ -908,8 +949,7 @@ and guarded_by_constructors ~subst ~metasenv context t indURI indlen nn =
          ("Too many args for constructor: " ^ String.concat " "
          (List.map (fun x-> PP.ppterm ~subst ~metasenv ~context x) args))))
       in
-      let left, args = HExtlib.split_nth paramsno tl in
-      List.for_all (does_not_occur ~subst context n nn) left &&
+      let _, args = HExtlib.split_nth paramsno tl in
       analyse_instantiated_type rec_params args
    | C.Appl ((C.Match (_,out,te,pl))::_) 
    | C.Match (_,out,te,pl) as t ->
@@ -918,6 +958,9 @@ and guarded_by_constructors ~subst ~metasenv context t indURI indlen nn =
        does_not_occur ~subst context n nn out &&
        does_not_occur ~subst context n nn te &&
        List.for_all (aux context n nn h) pl
+(* IMPOSSIBLE unsless we allow to pass cofix to other fix/cofix as we do for 
+   higher order fix in g_b_destructors.
+
    | C.Const (Ref.Ref (u,(Ref.Fix _| Ref.CoFix _)) as ref)
    | C.Appl(C.Const (Ref.Ref(u,(Ref.Fix _| Ref.CoFix _)) as ref) :: _) as t ->
       let tl = match t with C.Appl (_::tl) -> tl | _ -> [] in
@@ -929,6 +972,7 @@ and guarded_by_constructors ~subst ~metasenv context t indURI indlen nn =
        (fun (_,_,_,_,bo) ->
           aux (context@tys) n nn h (debruijn u len context bo))
        fl
+*)
    | C.Const _
    | C.Appl _ as t -> does_not_occur ~subst context n nn t
  in
@@ -1022,44 +1066,39 @@ and type_of_constant ((Ref.Ref (uri,_)) as ref) =
      ty
   | _ -> raise (AssertFailure (lazy "type_of_constant: environment/reference"))
 
-and get_relevance ~subst context te args = 
-  match te with 
-  | C.Const r when List.length (E.get_relevance r) >= List.length args -> 
-      let relevance = E.get_relevance r in 
-      (match r with
-        | Ref.Ref (_,Ref.Con (_,_,lno)) ->
-            let _,relevance = HExtlib.split_nth lno relevance in
-              HExtlib.mk_list false lno @ relevance
-        | _ -> relevance)
-  | t ->
-      let ty = typeof ~subst ~metasenv:[] context t in
-      let rec aux context ty = function
-        | [] -> [] 
-	| arg::tl -> match R.whd ~subst context ty with
-          | C.Prod (name,so,de) -> 
-	      let sort = typeof ~subst ~metasenv:[] context so in
-	      let new_ty = S.subst ~avoid_beta_redexes:true arg de in
-	      (match R.whd ~subst context sort with
-	         | C.Sort C.Prop -> 
-	             false::(aux ((name,(C.Decl so))::context) new_ty tl)
-	         | C.Sort _
-		 | C.Meta _ -> true::(aux ((name,(C.Decl so))::context) de tl)
-	         | _ -> raise (TypeCheckerFailure (lazy (Printf.sprintf
-		        "Prod: the type %s of the source of %s is not a sort" 
-		         (PP.ppterm ~subst ~metasenv:[] ~context sort)
-			 (PP.ppterm ~subst ~metasenv:[] ~context so)))))
-          | _ ->
-             raise 
-               (TypeCheckerFailure
-                 (lazy (Printf.sprintf
-                   "Appl: %s is not a function, it cannot be applied"
-                   (PP.ppterm ~subst ~metasenv:[] ~context
-                    (let res = List.length tl in
-                     let eaten = List.length args - res in
-                      (C.Appl
-                       (t::fst
-                        (HExtlib.split_nth eaten args))))))))
-      in aux context ty args
+and get_relevance ~subst context t args = 
+   let ty = typeof ~subst ~metasenv:[] context t in
+   let rec aux context ty = function
+     | [] -> [] 
+     | arg::tl -> match R.whd ~subst context ty with
+       | C.Prod (_,so,de) -> 
+           let sort = typeof ~subst ~metasenv:[] context so in
+           let new_ty = S.subst ~avoid_beta_redexes:true arg de in
+           (*prerr_endline ("so: " ^ PP.ppterm ~subst ~metasenv:[]
+	     ~context so);
+           prerr_endline ("sort: " ^ PP.ppterm ~subst ~metasenv:[]
+	     ~context sort);*)
+	   (match R.whd ~subst context sort with
+              | C.Sort C.Prop ->
+                  false::(aux context new_ty tl)
+              | C.Sort _
+     	      | C.Meta _ -> true::(aux context new_ty tl)
+              | _ -> raise (TypeCheckerFailure (lazy (Printf.sprintf
+     	        "Prod: the type %s of the source of %s is not a sort" 
+     	         (PP.ppterm ~subst ~metasenv:[] ~context sort)
+     		 (PP.ppterm ~subst ~metasenv:[] ~context so)))))
+       | _ ->
+          raise 
+            (TypeCheckerFailure
+              (lazy (Printf.sprintf
+                "Appl: %s is not a function, it cannot be applied"
+                (PP.ppterm ~subst ~metasenv:[] ~context
+                 (let res = List.length tl in
+                  let eaten = List.length args - res in
+                   (C.Appl
+                    (t::fst
+                     (HExtlib.split_nth eaten args))))))))
+   in aux context ty args
 ;;
 
 let typecheck_context ~metasenv ~subst context =
@@ -1122,124 +1161,6 @@ let typecheck_subst ~metasenv subst =
     ) [] subst)
 ;;
 
-let check_rel1_irrelevant ~metasenv ~subst context = fun _ -> ();;
-(*  let shift e (k, context) = k+1,e::context in
-  let rec aux (evil, context as k) () t =
-    match R.whd ~subst context t with
-    | C.Rel i when i = evil -> (*
-        raise (TypeCheckerFailure (lazy (Printf.sprintf
-         "Argument %s declared as irrelevante is used in a relevant position" 
-           (PP.ppterm ~subst ~metasenv ~context (C.Rel i))))) *) ()
-    | C.Meta _ -> ()
-    | C.Lambda (name,so,tgt) -> 
-        (* checking so is not needed since the implicit version of CC
-         * has untyped lambdas (curry style), see Barras and Bernardo  *)
-        aux (shift (name,C.Decl so) k) () tgt 
-    | C.Appl (C.Const ref::args) -> 
-         let relevance = NCicEnvironment.get_relevance ref in
-         HExtlib.list_iter_default2 
-           (fun t -> function false -> () | _ -> aux k () t)
-           args true relevance
-    | C.Match (_, _, _, []) -> ()
-    | C.Match (ref, _, t, [p]) -> 
-        aux k () p;
-        let _,lno,itl,_,_ = E.get_checked_indtys ref in
-        let _,_,_,cl = List.hd itl in
-        let _,_,c = List.hd cl in
-        if not (is_non_informative lno c) then aux k () t
-    | C.Match (_, _, t, pl) -> List.iter (aux k ()) (t::pl)
-    | t -> U.fold shift k aux () t
-  in 
-    aux (1, context) () *)
-
-let check_relevance ~subst ~metasenv relevance ty =
-  let error () =
-    raise (TypeCheckerFailure 
-     (lazy ("Wrong relevance declaration: " ^ 
-     String.concat "," (List.map string_of_bool relevance)^ 
-     "\nfor type: "^PP.ppterm ~metasenv ~subst ~context:[] ty)))
-  in
-  let rec aux context relevance ty =
-    match R.whd ~subst context ty with
-    | C.Prod (name,so,de) ->
-        let sort = typeof ~subst ~metasenv context so in
-        (match (relevance,R.whd ~subst context sort) with
-	  | [],_ -> ()
-          | false::tl,C.Sort C.Prop -> aux ((name,(C.Decl so))::context) tl de
-	  | true::_,C.Sort C.Prop
-	  | false::_,C.Sort _
-          | false::_,C.Meta _ -> error ()
-          | true::tl,C.Sort _
-          | true::tl,C.Meta _ -> aux ((name,(C.Decl so))::context) tl de
-          | _ -> raise (TypeCheckerFailure (lazy (Printf.sprintf
-                 "Prod: the type %s of the source of %s is not a sort"
-                  (PP.ppterm ~subst ~metasenv ~context sort)
-                  (PP.ppterm ~subst ~metasenv ~context so)))))
-    | _ -> (match relevance with
-      | [] -> ()
-      | _::_ -> error ())
-  in aux [] relevance ty
-;;
-(* old check_relevance
-
-let shift e (in_type, context, relevance) = 
-    assert (relevance = []); in_type, e::context, relevance
-  in
-  let rec aux2 (_,context,relevance as k) t = 
-    let error () = () (*
-      raise (TypeCheckerFailure 
-       (lazy ("Wrong relevance declaration: " ^ 
-       String.concat "," (List.map string_of_bool relevance)^ 
-       "\nfor: "^PP.ppterm ~metasenv ~subst ~context t))) *)
-    in
-    let rec aux (in_type, context, relevance as k) () t = 
-      match relevance, R.whd ~subst context t, in_type with
-      | _,C.Meta _,_ -> ()
-      | true::tl,C.Lambda (name,so,t), false 
-      | true::tl,C.Prod (name,so,t), true -> 
-          aux (in_type, (name, C.Decl so)::context, tl) () t
-      | false::tl,C.Lambda (name,so,t), false 
-      | false::tl,C.Prod (name,so,t), true -> 
-          let context = (name, C.Decl so)::context in
-          check_rel1_irrelevant ~metasenv ~subst context t;
-          aux (in_type, context, tl) () t
-      | [], C.Match (ref,oty,t,pl), _ ->
-          aux k () t;
-          let _,lno,itl,_,i = E.get_checked_indtys ref in
-          let rel,_,_,cl = List.nth itl i in
-          let _, rel = 
-            try HExtlib.split_nth lno rel 
-            with Failure _ -> [],[]
-          in
-          aux2 (false, context, rel) oty;
-          List.iter2 
-            (fun p (rel,_,_) -> 
-               let _,rel = 
-                 try HExtlib.split_nth lno rel 
-                 with Failure _ -> [],[]
-               in
-               aux2 (false, context, rel) p)
-            pl cl
-      | [],t,_ -> U.fold shift k aux () t
-      | rel1,C.Appl (C.Const ref :: args),_ ->
-          let relevance = E.get_relevance ref in
-          let _, relevance = 
-            try HExtlib.split_nth (List.length args) relevance 
-            with Failure _ -> [],[] 
-          in
-          prerr_endline ("rimane: "^String.concat "," (List.map string_of_bool relevance)^ " contro "^ String.concat "," (List.map string_of_bool rel1) );
-          HExtlib.list_iter_default2 (fun r1 r2 -> if not r1 && r2 then error ())
-            rel1 true relevance
-      | rel1,C.Const ref,_ ->
-          let relevance = E.get_relevance ref in
-          HExtlib.list_iter_default2 (fun r1 r2 -> if not r1 && r2 then error ())
-            rel1 true relevance
-      | _,_,_ -> error ()
-    in
-       aux k () t
-  in
-    aux2 (in_type, [], relevance)
-;;*)
 
 let typecheck_obj (uri,_height,metasenv,subst,kind) =
  (* height is not checked since it is only used to implement an optimization *)
@@ -1255,11 +1176,11 @@ let typecheck_obj (uri,_height,metasenv,subst,kind) =
         "inferred type:\n%s\nexpected type:\n%s")
         (PP.ppterm ~subst ~metasenv ~context:[] ty_te) 
         (PP.ppterm ~subst ~metasenv ~context:[] ty))));
-      check_relevance ~subst ~metasenv relevance ty
+      check_relevance ~subst ~metasenv [] relevance ty
       (*check_relevance ~in_type:false ~subst ~metasenv relevance te*)
    | C.Constant (relevance,_,None,ty,_) ->
       ignore (typeof ~subst ~metasenv [] ty);
-      check_relevance ~subst ~metasenv relevance ty
+      check_relevance ~subst ~metasenv [] relevance ty
    | C.Inductive (_, leftno, tyl, _) -> 
        check_mutual_inductive_defs uri ~metasenv ~subst leftno tyl
    | C.Fixpoint (inductive,fl,_) ->
@@ -1267,6 +1188,7 @@ let typecheck_obj (uri,_height,metasenv,subst,kind) =
         List.fold_left
          (fun (types,kl) (relevance,name,k,ty,_) ->
            let _ = typeof ~subst ~metasenv [] ty in
+	    check_relevance ~subst ~metasenv [] relevance ty;
             ((name,C.Decl ty)::types, k::kl)
          ) ([],[]) fl
       in