X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FnCicTypeChecker.ml;h=4b00edd05b2878ccea79ea6712540c2cfaf7db2a;hb=44ccb088991b937c54cbe13f0a135e36da9d5d8d;hp=46caae5acbed96d74038abd74ec7ebead2d80f43;hpb=09dc8295b3ec33bfa731189788330ba21b5f1428;p=helm.git

diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml
index 46caae5ac..4b00edd05 100644
--- a/helm/software/components/ng_kernel/nCicTypeChecker.ml
+++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml
@@ -28,281 +28,9 @@ let shift_k e (c,rf,x,safes) =
 
 (* $Id: cicTypeChecker.ml 8213 2008-03-13 18:48:26Z sacerdot $ *)
 
-(*
-exception CicEnvironmentError;;
-
-(*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 ;-)              *)
-and weakly_positive context n nn uri te =
- let module C = Cic in
-(*CSC: Che schifo! Bisogna capire meglio e trovare una soluzione ragionevole!*)
-  let dummy_mutind =
-   C.MutInd (HelmLibraryObjects.Datatypes.nat_URI,0,[])
-  in
-  (*CSC: mettere in cicSubstitution *)
-  let rec subst_inductive_type_with_dummy_mutind =
-   function
-      C.MutInd (uri',0,_) when UriManager.eq uri' uri ->
-       dummy_mutind
-    | C.Appl ((C.MutInd (uri',0,_))::tl) when UriManager.eq uri' uri ->
-       dummy_mutind
-    | C.Cast (te,ty) -> subst_inductive_type_with_dummy_mutind te
-    | C.Prod (name,so,ta) ->
-       C.Prod (name, subst_inductive_type_with_dummy_mutind so,
-        subst_inductive_type_with_dummy_mutind ta)
-    | C.Lambda (name,so,ta) ->
-       C.Lambda (name, subst_inductive_type_with_dummy_mutind so,
-        subst_inductive_type_with_dummy_mutind ta)
-    | C.Appl tl ->
-       C.Appl (List.map subst_inductive_type_with_dummy_mutind tl)
-    | C.MutCase (uri,i,outtype,term,pl) ->
-       C.MutCase (uri,i,
-        subst_inductive_type_with_dummy_mutind outtype,
-        subst_inductive_type_with_dummy_mutind term,
-        List.map subst_inductive_type_with_dummy_mutind pl)
-    | C.Fix (i,fl) ->
-       C.Fix (i,List.map (fun (name,i,ty,bo) -> (name,i,
-        subst_inductive_type_with_dummy_mutind ty,
-        subst_inductive_type_with_dummy_mutind bo)) fl)
-    | C.CoFix (i,fl) ->
-       C.CoFix (i,List.map (fun (name,ty,bo) -> (name,
-        subst_inductive_type_with_dummy_mutind ty,
-        subst_inductive_type_with_dummy_mutind bo)) fl)
-    | C.Const (uri,exp_named_subst) ->
-       let exp_named_subst' =
-        List.map
-         (function (uri,t) -> (uri,subst_inductive_type_with_dummy_mutind t))
-         exp_named_subst
-       in
-        C.Const (uri,exp_named_subst')
-    | C.MutInd (uri,typeno,exp_named_subst) ->
-       let exp_named_subst' =
-        List.map
-         (function (uri,t) -> (uri,subst_inductive_type_with_dummy_mutind t))
-         exp_named_subst
-       in
-        C.MutInd (uri,typeno,exp_named_subst')
-    | C.MutConstruct (uri,typeno,consno,exp_named_subst) ->
-       let exp_named_subst' =
-        List.map
-         (function (uri,t) -> (uri,subst_inductive_type_with_dummy_mutind t))
-         exp_named_subst
-       in
-        C.MutConstruct (uri,typeno,consno,exp_named_subst')
-    | t -> t
-  in
-  match CicReduction.whd context te with
-(*
-     C.Appl ((C.MutInd (uri',0,_))::tl) when UriManager.eq uri' uri -> true
-*)
-     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 ->
-       (* dummy abstraction, so we behave as in the anonimous case *)
-       strictly_positive context n nn
-        (subst_inductive_type_with_dummy_mutind source) &&
-         weakly_positive ((Some (name,(C.Decl source)))::context)
-         (n + 1) (nn + 1) uri dest
-   | C.Prod (name,source,dest) ->
-       does_not_occur context n nn
-         (subst_inductive_type_with_dummy_mutind source)&&
-         weakly_positive ((Some (name,(C.Decl source)))::context)
-         (n + 1) (nn + 1) uri dest
-   | _ ->
-     raise (TypeCheckerFailure (lazy "Malformed inductive constructor type"))
-
-(* instantiate_parameters ps (x1:T1)...(xn:Tn)C                             *)
-(* returns ((x_|ps|:T_|ps|)...(xn:Tn)C){ps_1 / x1 ; ... ; ps_|ps| / x_|ps|} *)
-and instantiate_parameters params c =
- let module C = Cic in
-  match (c,params) with
-     (c,[]) -> c
-   | (C.Prod (_,_,ta), he::tl) ->
-       instantiate_parameters tl
-        (CicSubstitution.subst he ta)
-   | (C.Cast (te,_), _) -> instantiate_parameters params te
-   | (t,l) -> raise (AssertFailure (lazy "1"))
-
-and strictly_positive context n nn te =
- let module C = Cic in
- let module U = UriManager in
-  match CicReduction.whd context te with
-   | t when does_not_occur context n nn t -> true
-   | C.Rel _ -> true
-   | C.Cast (te,ty) ->
-      (*CSC: bisogna controllare ty????*)
-      strictly_positive context n nn te
-   | C.Prod (name,so,ta) ->
-      does_not_occur context n nn so &&
-       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) -> 
-      let (ok,paramsno,ity,cl,name) =
-        let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
-          match o with
-              C.InductiveDefinition (tl,_,paramsno,_) ->
-                let (name,_,ity,cl) = List.nth tl i in
-                (List.length tl = 1, paramsno, ity, cl, name) 
-                (* (true, paramsno, ity, cl, name) *)
-            | _ ->
-                raise 
-                  (TypeCheckerFailure
-                     (lazy ("Unknown inductive type:" ^ U.string_of_uri uri)))
-      in 
-      let (params,arguments) = split tl paramsno in
-      let lifted_params = List.map (CicSubstitution.lift 1) params in
-      let cl' =
-        List.map
-          (fun (_,te) ->
-             instantiate_parameters lifted_params
-               (CicSubstitution.subst_vars exp_named_subst te)
-          ) cl
-      in
-        ok &&
-          List.fold_right
-          (fun x i -> i && does_not_occur context n nn x)
-          arguments true &&
-         (*CSC: MEGAPATCH3 (sara' quella giusta?)*)
-          List.fold_right
-          (fun x i ->
-             i &&
-               weakly_positive
-               ((Some (C.Name name,(Cic.Decl ity)))::context) (n+1) (nn+1) uri
-               x
-          ) cl' true
-   | t -> false
-       
-(* the inductive type indexes are s.t. n < x <= nn *)
-and are_all_occurrences_positive context uri indparamsno i n nn te =
- let module C = Cic in
-  match CicReduction.whd context te with
-     C.Appl ((C.Rel m)::tl) when m = i ->
-      (*CSC: riscrivere fermandosi a 0 *)
-      (* let's check if the inductive type is applied at least to *)
-      (* indparamsno parameters                                   *)
-      let last =
-       List.fold_left
-        (fun k x ->
-          if k = 0 then 0
-          else
-           match CicReduction.whd context x with
-              C.Rel m when m = n - (indparamsno - k) -> k - 1
-            | _ ->
-              raise (TypeCheckerFailure
-               (lazy 
-               ("Non-positive occurence in mutual inductive definition(s) [1]" ^
-                UriManager.string_of_uri uri)))
-        ) indparamsno tl
-      in
-       if last = 0 then
-        List.fold_right (fun x i -> i && does_not_occur context n nn x) tl true
-       else
-        raise (TypeCheckerFailure
-         (lazy ("Non-positive occurence in mutual inductive definition(s) [2]"^
-          UriManager.string_of_uri uri)))
-   | C.Rel m when m = i ->
-      if indparamsno = 0 then
-       true
-      else
-        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 ->
-      (* dummy abstraction, so we behave as in the anonimous case *)
-      strictly_positive context n nn source &&
-       are_all_occurrences_positive
-        ((Some (name,(C.Decl source)))::context) uri indparamsno
-        (i+1) (n + 1) (nn + 1) dest
-   | C.Prod (name,source,dest) ->
-      does_not_occur context n nn source &&
-       are_all_occurrences_positive ((Some (name,(C.Decl source)))::context)
-        uri indparamsno (i+1) (n + 1) (nn + 1) dest
-   | _ ->
-     raise
-      (TypeCheckerFailure (lazy ("Malformed inductive constructor type " ^
-        (UriManager.string_of_uri uri))))
-
-(* Main function to checks the correctness of a mutual *)
-(* inductive block definition. This is the function    *)
-(* exported to the proof-engine.                       *)
-and typecheck_mutual_inductive_defs ~logger uri (itl,_,indparamsno) ugraph =
- let module U = UriManager in
-  (* let's check if the arity of the inductive types are well *)
-  (* formed                                                   *)
-  let ugrap1 = List.fold_left 
-   (fun ugraph (_,_,x,_) -> let _,ugraph' = 
-      type_of ~logger x ugraph in ugraph') 
-   ugraph itl in
-
-  (* let's check if the types of the inductive constructors  *)
-  (* are well formed.                                        *)
-  (* In order not to use type_of_aux we put the types of the *)
-  (* mutual inductive types at the head of the types of the  *)
-  (* constructors using Prods                                *)
-  let len = List.length itl in
-  let tys =
-    List.map (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) itl in
-  let _,ugraph2 =
-    List.fold_right
-      (fun (_,_,_,cl) (i,ugraph) ->
-        let ugraph'' = 
-          List.fold_left
-            (fun ugraph (name,te) -> 
-              let debruijnedte = debruijn uri len te in
-              let augmented_term =
-                List.fold_right
-                  (fun (name,_,ty,_) i -> Cic.Prod (Cic.Name name, ty, i))
-                  itl debruijnedte
-              in
-              let _,ugraph' = type_of ~logger augmented_term ugraph in
-              (* let's check also the positivity conditions *)
-              if
-                not
-                  (are_all_occurrences_positive tys uri indparamsno i 0 len
-                     debruijnedte)
-              then
-                begin
-                prerr_endline (UriManager.string_of_uri uri);
-                prerr_endline (string_of_int (List.length tys));
-                raise
-                  (TypeCheckerFailure
-                    (lazy ("Non positive occurence in " ^ U.string_of_uri uri)))                end 
-              else
-                ugraph'
-            ) ugraph cl in
-        (i + 1),ugraph''
-      ) itl (1,ugrap1)
-  in
-  ugraph2
 
-(* Main function to checks the correctness of a mutual *)
-(* inductive block definition.                         *)
-and check_mutual_inductive_defs uri obj ugraph =
-  match obj with
-      Cic.InductiveDefinition (itl, params, indparamsno, _) ->
-        typecheck_mutual_inductive_defs uri (itl,params,indparamsno) ugraph 
-    | _ ->
-        raise (TypeCheckerFailure (
-                lazy ("Unknown mutual inductive definition:" ^
-                 UriManager.string_of_uri uri)))
 
+(*
 (* the boolean h means already protected *)
 (* args is the list of arguments the type of the constructor that may be *)
 (* found in head position must be applied to.                            *)
@@ -584,7 +312,7 @@ let debruijn ?(cb=fun _ _ -> ()) uri number_of_types =
   aux 0
 ;;
 
-let sort_of_prod ~subst context (name,s) (t1, t2) =
+let sort_of_prod ~metasenv ~subst context (name,s) (t1, t2) =
    let t1 = R.whd ~subst context t1 in
    let t2 = R.whd ~subst ((name,C.Decl s)::context) t2 in
    match t1, t2 with
@@ -599,19 +327,21 @@ let sort_of_prod ~subst context (name,s) (t1, t2) =
    | _ -> 
       raise (TypeCheckerFailure (lazy (Printf.sprintf
         "Prod: expected two sorts, found = %s, %s" 
-         (NCicPp.ppterm t1) (NCicPp.ppterm t2))))
+         (NCicPp.ppterm ~subst ~metasenv ~context t1) 
+         (NCicPp.ppterm ~subst ~metasenv ~context t2))))
 ;;
 
-let eat_prods ~subst ~metasenv context ty_he args_with_ty = 
+let eat_prods ~subst ~metasenv context he ty_he args_with_ty = 
   let rec aux ty_he = function 
   | [] -> ty_he
   | (arg, ty_arg)::tl ->
-      (match R.whd ~subst context ty_he with 
+      match R.whd ~subst context ty_he with 
       | C.Prod (n,s,t) ->
 (*
-          prerr_endline (NCicPp.ppterm ~context s ^ " - Vs - " ^ NCicPp.ppterm
+          prerr_endline (NCicPp.ppterm ~subst ~metasenv ~context s ^ " - Vs - "
+          ^ NCicPp.ppterm ~subst ~metasenv
           ~context ty_arg);
-          prerr_endline (NCicPp.ppterm ~context (S.subst ~avoid_beta_redexes:true arg t));
+          prerr_endline (NCicPp.ppterm ~subst ~metasenv ~context (S.subst ~avoid_beta_redexes:true arg t));
 *)
           if R.are_convertible ~subst ~metasenv context ty_arg s then
             aux (S.subst ~avoid_beta_redexes:true arg t) tl
@@ -619,12 +349,23 @@ let eat_prods ~subst ~metasenv context ty_he args_with_ty =
             raise 
               (TypeCheckerFailure 
                 (lazy (Printf.sprintf
-                  ("Appl: wrong parameter-type, expected %s, found %s")
-                  (NCicPp.ppterm ty_arg) (NCicPp.ppterm s))))
+                  ("Appl: wrong application of %s: the parameter %s has type"^^
+                   "\n%s\nbut it should have type \n%s\n")
+                  (NCicPp.ppterm ~subst ~metasenv ~context he)
+                  (NCicPp.ppterm ~subst ~metasenv ~context arg)
+                  (NCicPp.ppterm ~subst ~metasenv ~context ty_arg)
+                  (NCicPp.ppterm ~subst ~metasenv ~context s))))
        | _ ->
           raise 
             (TypeCheckerFailure
-              (lazy "Appl: this is not a function, it cannot be applied")))
+              (lazy (Printf.sprintf
+                "Appl: %s is not a function, it cannot be applied"
+                (NCicPp.ppterm ~subst ~metasenv ~context
+                 (let res = List.length tl in
+                  let eaten = List.length args_with_ty - res in
+                   (NCic.Appl
+                    (he::List.map fst
+                     (fst (HExtlib.split_nth eaten args_with_ty)))))))))
   in
     aux ty_he args_with_ty
 ;;
@@ -642,7 +383,7 @@ let fix_lefts_in_constrs ~subst uri paramsno tyl i =
     cl 
   in
   let lefts = fst (split_prods ~subst [] paramsno arity) in
-  tys@lefts, len, cl'
+  lefts@tys, len, cl'
 ;;
 
 exception DoesOccur;;
@@ -669,7 +410,121 @@ let does_not_occur ~subst context n nn t =
    with DoesOccur -> false
 ;;
 
-exception NotGuarded;;
+(*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!*)
+  let dummy = C.Sort (C.Type ~-1) in
+  (*CSC: mettere in cicSubstitution *)
+  let rec subst_inductive_type_with_dummy _ = function
+    | C.Const (Ref.Ref (_,uri',Ref.Ind 0)) when NUri.eq uri' uri -> dummy
+    | C.Appl ((C.Const (Ref.Ref (_,uri',Ref.Ind 0)))::tl) 
+        when NUri.eq uri' uri -> dummy
+    | 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"))
+
+(* instantiate_parameters ps (x1:T1)...(xn:Tn)C                             *)
+(* returns ((x_|ps|:T_|ps|)...(xn:Tn)C){ps_1 / x1 ; ... ; ps_|ps| / x_|ps|} *)
+and instantiate_parameters params c =
+  match c, params with
+  | c,[] -> c
+  | C.Prod (_,_,ta), he::tl -> instantiate_parameters tl (S.subst he ta)
+  | t,l -> raise (AssertFailure (lazy "1"))
+
+and strictly_positive ~subst context n nn te =
+  match R.whd context te with
+   | t when does_not_occur ~subst context n nn t -> true
+   | C.Rel _ -> true
+   | 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
+   | C.Appl (C.Const (Ref.Ref (_,uri,Ref.Ind i) as r)::tl) -> 
+      let _,paramsno,tyl,_,i = E.get_checked_indtys r in
+      let _,name,ity,cl = List.nth tyl i in
+      let ok = List.length tyl = 1 in
+      let params, arguments = HExtlib.split_nth paramsno tl in
+      let lifted_params = List.map (S.lift 1) params in
+      let cl =
+        List.map (fun (_,_,te) -> instantiate_parameters lifted_params te) cl 
+      in
+      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
+   | _ -> 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
+           | y -> raise (TypeCheckerFailure (lazy 
+              ("Argument "^string_of_int (indparamsno - k + 1) ^ " (of " ^
+              string_of_int indparamsno ^ " fixed) is not homogeneous in "^
+              "appl:\n"^ NCicPp.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)))
+  | C.Rel m when m = i ->
+      if indparamsno = 0 then
+       true
+      else
+        raise (TypeCheckerFailure
+         (lazy ("Non-positive occurence in mutual inductive definition(s) [3]"^
+          NUri.string_of_uri uri)))
+  | 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 &&
+       are_all_occurrences_positive ~subst 
+        ((name,C.Decl source)::context) uri indparamsno
+        (i+1) (n + 1) (nn + 1) dest
+   | C.Prod (name,source,dest) ->
+       if not (does_not_occur ~subst context n nn source) then
+         raise (TypeCheckerFailure (lazy ("Non-positive occurrence in "^
+         NCicPp.ppterm ~context ~metasenv:[] ~subst te)));
+       are_all_occurrences_positive ~subst ((name,C.Decl source)::context)
+        uri indparamsno (i+1) (n + 1) (nn + 1) dest
+   | _ ->
+     raise
+      (TypeCheckerFailure (lazy ("Malformed inductive constructor type " ^
+        (NUri.string_of_uri uri))))
+;;
+
+exception NotGuarded of string Lazy.t;;
 
 let rec typeof ~subst ~metasenv context term =
   let rec typeof_aux context = 
@@ -685,22 +540,22 @@ let rec typeof ~subst ~metasenv context term =
     | C.Sort s -> C.Sort (C.Type 0)
     | C.Implicit _ -> raise (AssertFailure (lazy "Implicit found"))
     | C.Meta (n,l) as t -> 
-       let canonical_context,ty =
+       let canonical_ctx,ty =
         try
          let _,c,_,ty = U.lookup_subst n subst in c,ty
         with U.Subst_not_found _ -> try
          let _,_,c,ty = U.lookup_meta n metasenv in c,ty
         with U.Meta_not_found _ ->
          raise (AssertFailure (lazy (Printf.sprintf
-          "%s not found" (NCicPp.ppterm t))))
+          "%s not found" (NCicPp.ppterm ~subst ~metasenv ~context t))))
        in
-        check_metasenv_consistency t context canonical_context l;
+        check_metasenv_consistency t ~subst ~metasenv context canonical_ctx l;
         S.subst_meta l ty
     | C.Const ref -> type_of_constant ref
     | C.Prod (name,s,t) ->
        let sort1 = typeof_aux context s in
        let sort2 = typeof_aux ((name,(C.Decl s))::context) t in
-       sort_of_prod ~subst context (name,s) (sort1,sort2)
+       sort_of_prod ~metasenv ~subst context (name,s) (sort1,sort2)
     | C.Lambda (n,s,t) ->
        let sort = typeof_aux context s in
        (match R.whd ~subst context sort with
@@ -710,17 +565,21 @@ let rec typeof ~subst ~metasenv context term =
            (TypeCheckerFailure (lazy (Printf.sprintf
              ("Not well-typed lambda-abstraction: " ^^
              "the source %s should be a type; instead it is a term " ^^ 
-             "of type %s") (NCicPp.ppterm s) (NCicPp.ppterm sort)))));
+             "of type %s") (NCicPp.ppterm ~subst ~metasenv ~context s)
+             (NCicPp.ppterm ~subst ~metasenv ~context sort)))));
        let ty = typeof_aux ((n,(C.Decl s))::context) t in
          C.Prod (n,s,ty)
     | C.LetIn (n,ty,t,bo) ->
        let ty_t = typeof_aux context t in
+       let _ = typeof_aux context ty in
        if not (R.are_convertible ~subst ~metasenv context ty ty_t) then
          raise 
           (TypeCheckerFailure 
             (lazy (Printf.sprintf
               "The type of %s is %s but it is expected to be %s" 
-                (NCicPp.ppterm t) (NCicPp.ppterm ty_t) (NCicPp.ppterm ty))))
+                (NCicPp.ppterm ~subst ~metasenv ~context t) 
+                (NCicPp.ppterm ~subst ~metasenv ~context ty_t) 
+                (NCicPp.ppterm ~subst ~metasenv ~context ty))))
        else
          let ty_bo = typeof_aux  ((n,C.Def (t,ty))::context) bo in
          S.subst ~avoid_beta_redexes:true t ty_bo
@@ -728,17 +587,20 @@ let rec typeof ~subst ~metasenv context term =
        let ty_he = typeof_aux context he in
        let args_with_ty = List.map (fun t -> t, typeof_aux context t) args in
 (*
-       prerr_endline ("HEAD: " ^ NCicPp.ppterm ~context ty_he);
+       prerr_endline ("HEAD: " ^ NCicPp.ppterm ~subst ~metasenv ~context ty_he);
        prerr_endline ("TARGS: " ^ String.concat " | " (List.map (NCicPp.ppterm
-       ~context) (List.map snd args_with_ty)));
+       ~subst ~metasenv ~context) (List.map snd args_with_ty)));
        prerr_endline ("ARGS: " ^ String.concat " | " (List.map (NCicPp.ppterm
-       ~context) (List.map fst args_with_ty)));
+       ~subst ~metasenv ~context) (List.map fst args_with_ty)));
 *)
-       eat_prods ~subst ~metasenv context ty_he args_with_ty
+       eat_prods ~subst ~metasenv context he ty_he args_with_ty
    | C.Appl _ -> raise (AssertFailure (lazy "Appl of length < 2"))
    | C.Match (Ref.Ref (_,_,Ref.Ind tyno) as r,outtype,term,pl) ->
       let outsort = typeof_aux context outtype in
-      let leftno = E.get_indty_leftno r in
+      let inductive,leftno,itl,_,_ = E.get_checked_indtys r in
+      let constructorsno =
+        let _,_,_,cl = List.nth itl tyno in List.length cl
+      in
       let parameters, arguments =
         let ty = R.whd ~subst context (typeof_aux context term) in
         let r',tl =
@@ -749,34 +611,29 @@ let rec typeof ~subst ~metasenv context term =
              raise 
                (TypeCheckerFailure (lazy (Printf.sprintf
                  "Case analysis: analysed term %s is not an inductive one"
-                 (NCicPp.ppterm term)))) in
+                 (NCicPp.ppterm ~subst ~metasenv ~context term)))) in
         if not (Ref.eq r r') then
          raise
           (TypeCheckerFailure (lazy (Printf.sprintf
             ("Case analysys: analysed term type is %s, but is expected " ^^
              "to be (an application of) %s")
-            (NCicPp.ppterm ty) (NCicPp.ppterm (C.Const r')))))
+            (NCicPp.ppterm ~subst ~metasenv ~context ty) 
+            (NCicPp.ppterm ~subst ~metasenv ~context (C.Const r')))))
         else
          try HExtlib.split_nth leftno tl
          with
           Failure _ ->
-           raise (TypeCheckerFailure (lazy (Printf.sprintf
-            "%s is partially applied" (NCicPp.ppterm ty)))) in
+           raise (TypeCheckerFailure (lazy (Printf.sprintf 
+           "%s is partially applied" 
+           (NCicPp.ppterm  ~subst ~metasenv ~context ty)))) in
       (* let's control if the sort elimination is allowed: [(I q1 ... qr)|B] *)
       let sort_of_ind_type =
         if parameters = [] then C.Const r
         else C.Appl ((C.Const r)::parameters) in
       let type_of_sort_of_ind_ty = typeof_aux context sort_of_ind_type in
-      if not (check_allowed_sort_elimination ~subst ~metasenv r context
-          sort_of_ind_type type_of_sort_of_ind_ty outsort)
-      then raise (TypeCheckerFailure (lazy ("Sort elimination not allowed")));
+      check_allowed_sort_elimination ~subst ~metasenv r context
+       sort_of_ind_type type_of_sort_of_ind_ty outsort;
       (* let's check if the type of branches are right *)
-      let leftno,constructorsno =
-        let inductive,leftno,itl,_,i = E.get_checked_indtys r in
-        let _,name,ty,cl = List.nth itl i in
-        let cl_len = List.length cl in
-        leftno, cl_len
-      in
       if List.length pl <> constructorsno then
        raise (TypeCheckerFailure (lazy ("Wrong number of cases in a match")));
       let j,branches_ok,p_ty, exp_p_ty =
@@ -803,10 +660,12 @@ let rec typeof ~subst ~metasenv context term =
         raise
          (TypeCheckerFailure 
           (lazy (Printf.sprintf ("Branch for constructor %s :=\n%s\n"^^
-          "has type %s\nnot convertible with %s") (NCicPp.ppterm (C.Const 
-          (Ref.mk_constructor j r)))
-          (NCicPp.ppterm ~context (List.nth pl (j-1)))
-          (NCicPp.ppterm ~context p_ty) (NCicPp.ppterm ~context exp_p_ty)))); 
+          "has type %s\nnot convertible with %s") 
+          (NCicPp.ppterm  ~subst ~metasenv ~context
+            (C.Const (Ref.mk_constructor (j-1) r)))
+          (NCicPp.ppterm ~metasenv ~subst ~context (List.nth pl (j-2)))
+          (NCicPp.ppterm ~metasenv ~subst ~context p_ty) 
+          (NCicPp.ppterm ~metasenv ~subst ~context exp_p_ty)))); 
       let res = outtype::arguments@[term] in
       R.head_beta_reduce (C.Appl res)
     | C.Match _ -> assert false
@@ -831,7 +690,9 @@ let rec typeof ~subst ~metasenv context term =
   (* check_metasenv_consistency checks that the "canonical" context of a
      metavariable is consitent - up to relocation via the relocation list l -
      with the actual context *)
-  and check_metasenv_consistency term context canonical_context l =
+  and check_metasenv_consistency 
+    ~subst ~metasenv term context canonical_context l 
+  =
    match l with
     | shift, NCic.Irl n ->
        let context = snd (HExtlib.split_nth shift context) in
@@ -841,10 +702,11 @@ let rec typeof ~subst ~metasenv context term =
          | _,_,[] ->
             raise (AssertFailure (lazy (Printf.sprintf
              "Local and canonical context %s have different lengths"
-             (NCicPp.ppterm term))))
+             (NCicPp.ppterm ~subst ~context ~metasenv term))))
          | m,[],_::_ ->
             raise (TypeCheckerFailure (lazy (Printf.sprintf
-             "Unbound variable -%d in %s" m (NCicPp.ppterm term))))
+             "Unbound variable -%d in %s" m 
+             (NCicPp.ppterm ~subst ~metasenv ~context term))))
          | m,t::tl,ct::ctl ->
             (match t,ct with
                 (_,C.Decl t1), (_,C.Decl t2)
@@ -856,15 +718,15 @@ let rec typeof ~subst ~metasenv context term =
                         (lazy (Printf.sprintf 
                       ("Not well typed metavariable local context for %s: " ^^ 
                        "%s expected, which is not convertible with %s")
-                      (NCicPp.ppterm term) (NCicPp.ppterm t2) (NCicPp.ppterm t1)
-                      )))
+                      (NCicPp.ppterm ~subst ~metasenv ~context term) 
+                      (NCicPp.ppterm ~subst ~metasenv ~context t2) 
+                      (NCicPp.ppterm ~subst ~metasenv ~context t1))))
               | _,_ ->
                raise 
-                   (TypeCheckerFailure 
-                     (lazy (Printf.sprintf 
+                   (TypeCheckerFailure (lazy (Printf.sprintf 
                     ("Not well typed metavariable local context for %s: " ^^ 
                      "a definition expected, but a declaration found")
-                    (NCicPp.ppterm term)))));
+                    (NCicPp.ppterm ~subst ~metasenv ~context term)))));
             compare (m - 1,tl,ctl)
         in
          compare (n,context,canonical_context)
@@ -908,7 +770,8 @@ let rec typeof ~subst ~metasenv context term =
                    (lazy (Printf.sprintf 
                      ("Not well typed metavariable local context: " ^^ 
                       "expected a term convertible with %s, found %s")
-                     (NCicPp.ppterm ct) (NCicPp.ppterm t))))
+                     (NCicPp.ppterm ~subst ~metasenv ~context ct) 
+                     (NCicPp.ppterm ~subst ~metasenv ~context t))))
           | t, (_,C.Decl ct) ->
               let type_t = typeof_aux context t in
               if not (R.are_convertible ~subst ~metasenv context type_t ct) then
@@ -916,13 +779,15 @@ let rec typeof ~subst ~metasenv context term =
                  (lazy (Printf.sprintf 
                   ("Not well typed metavariable local context: "^^
                   "expected a term of type %s, found %s of type %s") 
-                  (NCicPp.ppterm ct) (NCicPp.ppterm t) (NCicPp.ppterm type_t))))
+                  (NCicPp.ppterm ~subst ~metasenv ~context ct) 
+                  (NCicPp.ppterm ~subst ~metasenv ~context t) 
+                  (NCicPp.ppterm ~subst ~metasenv ~context type_t))))
         ) l lifted_canonical_context 
        with
         Invalid_argument _ ->
           raise (AssertFailure (lazy (Printf.sprintf
            "Local and canonical context %s have different lengths"
-           (NCicPp.ppterm term))))
+           (NCicPp.ppterm ~subst ~metasenv ~context term))))
 
   and is_non_informative context paramsno c =
    let rec aux context c =
@@ -944,61 +809,116 @@ let rec typeof ~subst ~metasenv context term =
     let arity2 = R.whd ~subst context arity2 in
       match arity1,arity2 with
        | C.Prod (name,so1,de1), C.Prod (_,so2,de2) ->
-          R.are_convertible ~subst ~metasenv context so1 so2 &&
-           aux ((name, C.Decl so1)::context)
-            (mkapp (S.lift 1 ind) (C.Rel 1)) de1 de2
+          if not (R.are_convertible ~subst ~metasenv context so1 so2) then
+           raise (TypeCheckerFailure (lazy (Printf.sprintf
+            "In outtype: expected %s, found %s"
+            (NCicPp.ppterm ~subst ~metasenv ~context so1)
+            (NCicPp.ppterm ~subst ~metasenv ~context so2)
+            )));
+          aux ((name, C.Decl so1)::context)
+           (mkapp (S.lift 1 ind) (C.Rel 1)) de1 de2
        | C.Sort _, C.Prod (name,so,ta) ->
-        (R.are_convertible ~subst ~metasenv context so ind &&
-          match arity1,ta with
-          | (C.Sort (C.CProp | C.Type _), C.Sort _)
-          | (C.Sort C.Prop, C.Sort C.Prop) -> true
-          | (C.Sort C.Prop, C.Sort (C.CProp | C.Type _)) ->
-              let inductive,leftno,itl,_,i = E.get_checked_indtys r in
-              let itl_len = List.length itl in
-              let _,name,ty,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? *)
-               cl_len = 0 ||
-                (itl_len = 1 && cl_len = 1 &&
-                 is_non_informative [name,C.Decl ty] leftno
-                  (let _,_,x = List.nth cl 0 in x))
-          | _,_ -> false)
-       | _,_ -> false
+          if not (R.are_convertible ~subst ~metasenv context so ind) then
+           raise (TypeCheckerFailure (lazy (Printf.sprintf
+            "In outtype: expected %s, found %s"
+            (NCicPp.ppterm ~subst ~metasenv ~context ind)
+            (NCicPp.ppterm ~subst ~metasenv ~context so)
+            )));
+          (match arity1,ta with
+            | (C.Sort (C.CProp | C.Type _), C.Sort _)
+            | (C.Sort C.Prop, C.Sort C.Prop) -> ()
+            | (C.Sort C.Prop, C.Sort (C.CProp | C.Type _)) ->
+        (* TODO: we should pass all these parameters since we
+         * have them already *)
+                let inductive,leftno,itl,_,i = E.get_checked_indtys r in
+                let itl_len = List.length itl in
+                let _,name,ty,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? *)
+                 if not
+                  (cl_len = 0 ||
+                   (itl_len = 1 && cl_len = 1 &&
+                    is_non_informative [name,C.Decl ty] leftno
+                     (let _,_,x = List.nth cl 0 in x)))
+                 then
+                  raise (TypeCheckerFailure (lazy
+                   ("Sort elimination not allowed")));
+          | _,_ -> ())
+       | _,_ -> ()
    in
     aux 
 
  in 
    typeof_aux context term
 
-and check_mutual_inductive_defs _ = ()
+and check_mutual_inductive_defs uri ~metasenv ~subst is_ind 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;
+  (* let's check if the types of the inductive constructors are well formed. *)
+  let len = List.length tyl in
+  let tys = List.rev (List.map (fun (_,n,ty,_) -> (n,(C.Decl ty))) tyl) in
+  ignore
+   (List.fold_right
+    (fun (_,_,_,cl) i ->
+       List.iter
+         (fun (_,name,te) -> 
+           let debruijnedte = debruijn uri len te in
+           ignore (typeof ~subst ~metasenv tys debruijnedte);
+           (* let's check also the positivity conditions *)
+           if 
+             not
+               (are_all_occurrences_positive ~subst tys uri leftno i 0 len
+                  debruijnedte) 
+           then
+             raise
+               (TypeCheckerFailure
+                 (lazy ("Non positive occurence in "^NUri.string_of_uri uri))))
+         cl;
+        i + 1)
+    tyl 1)
 
-and eat_lambdas ~subst context n te =
+and eat_lambdas ~subst ~metasenv context n te =
   match (n, R.whd ~subst context te) with
   | (0, _) -> (te, context)
   | (n, C.Lambda (name,so,ta)) when n > 0 ->
-      eat_lambdas ~subst ((name,(C.Decl so))::context) (n - 1) ta
+      eat_lambdas ~subst ~metasenv ((name,(C.Decl so))::context) (n - 1) ta
    | (n, te) ->
-      raise (AssertFailure 
-        (lazy (Printf.sprintf "9 (%d, %s)" n (NCicPp.ppterm te))))
+      raise (AssertFailure (lazy (Printf.sprintf "9 (%d, %s)" n 
+        (NCicPp.ppterm ~subst ~metasenv ~context te))))
 
-and guarded_by_destructors ~subst context recfuns t = 
+and guarded_by_destructors ~subst ~metasenv context recfuns t = 
  let recursor f k t = NCicUtils.fold shift_k k (fun k () -> f k) () t in
- let rec aux (context, recfuns, x, safes as k) = function
-  | C.Rel m when List.mem_assoc m recfuns -> raise NotGuarded 
+ let rec aux (context, recfuns, x, safes as k) t = 
+  match R.whd ~subst context t with (* TODO: use ~delta:false as mush as poss*)
+  | C.Rel m as t when List.mem_assoc m recfuns -> 
+      raise (NotGuarded (lazy 
+        (NCicPp.ppterm ~subst ~metasenv ~context t ^ " passed around")))
   | C.Rel m ->
      (match List.nth context (m-1) with 
      | _,C.Decl _ -> ()
      | _,C.Def (bo,_) -> aux (context, recfuns, x, safes) (S.lift m bo))
   | C.Meta _ -> ()
-  | C.Appl ((C.Rel m)::tl) when List.mem_assoc m recfuns ->
+  | C.Appl ((C.Rel m)::tl) as t when List.mem_assoc m recfuns ->
      let rec_no = List.assoc m recfuns in
-     if not (List.length tl > rec_no) then raise NotGuarded
+     if not (List.length tl > rec_no) then 
+       raise (NotGuarded (lazy 
+         (NCicPp.ppterm ~context ~subst ~metasenv t ^ 
+         " is a partial application of a fix")))
      else
        let rec_arg = List.nth tl rec_no in
-       if not (is_really_smaller ~subst k rec_arg) then raise
-       NotGuarded;
+       if not (is_really_smaller ~subst ~metasenv k rec_arg) then 
+         raise (NotGuarded (lazy 
+           (NCicPp.ppterm ~context ~subst ~metasenv rec_arg ^ " not smaller")));
        List.iter (aux k) tl
+       (*
+  | C.Appl (C.Const ((Ref.Ref (_,_,Ref.Fix (i,j))) as r)::args) ->
+      List.iter (aux k) args;
+      let fixes,_,_ = E.get_checked_fixes r in
+      let _,_,_,_,bo = List.nth fixes i in
+      let bo_wout_lam, context = eat_lambdas ~subst ~metasenv context j in
+      (* debruijna body..... *) assert false
+*)
   | C.Match (Ref.Ref (_,uri,_) as ref,outtype,term,pl) as t ->
      (match R.whd ~subst context term with
      | C.Rel m | C.Appl (C.Rel m :: _ ) as t when List.mem m safes || m = x ->
@@ -1011,15 +931,15 @@ and guarded_by_destructors ~subst context recfuns t =
          List.iter (aux k) args; 
          List.iter2
            (fun p (_,_,bruijnedc) ->
-             let rl = recursive_args ~subst c_ctx 0 len bruijnedc in
+             let rl = recursive_args ~subst ~metasenv c_ctx 0 len bruijnedc in
              let p, k = get_new_safes ~subst k p rl in
              aux k p) 
            pl cl
      | _ -> recursor aux k t)
   | t -> recursor aux k t
  in
-  try aux (context, recfuns, 1, []) t;true
-  with NotGuarded -> false
+  try aux (context, recfuns, 1, []) t
+  with NotGuarded s -> raise (TypeCheckerFailure s)
 
 (*
  | C.Fix (_, fl) ->
@@ -1061,15 +981,18 @@ and guarded_by_destructors ~subst context recfuns t =
        ) fl true
 *)
 
-and guarded_by_constructors ~subst _ _ _ _ _ _ _ = assert false
+and guarded_by_constructors ~subst ~metasenv _ _ _ _ _ _ _ = true
 
-and recursive_args ~subst context n nn te =
+and recursive_args ~subst ~metasenv context n nn te =
   match R.whd context te with
-  | C.Rel _ -> []
+  | C.Rel _ | C.Appl _ -> []
   | C.Prod (name,so,de) ->
      (not (does_not_occur ~subst context n nn so)) ::
-      (recursive_args ~subst ((name,(C.Decl so))::context) (n+1) (nn + 1) de)
-  | _ -> raise (AssertFailure (lazy ("recursive_args")))
+      (recursive_args ~subst ~metasenv 
+        ((name,(C.Decl so))::context) (n+1) (nn + 1) de)
+  | t -> 
+     raise (AssertFailure (lazy ("recursive_args:" ^ NCicPp.ppterm ~subst
+     ~metasenv ~context:[] t)))
 
 and get_new_safes ~subst (context, recfuns, x, safes as k) p rl =
   match R.whd ~subst context p, rl with
@@ -1087,20 +1010,15 @@ and split_prods ~subst context n te =
        split_prods ~subst ((name,(C.Decl so))::context) (n - 1) ta
   | _ -> raise (AssertFailure (lazy "split_prods"))
 
-and is_really_smaller ~subst (context, recfuns, x, safes as k) te =
+and is_really_smaller ~subst ~metasenv (context, recfuns, x, safes as k) te =
  match R.whd ~subst context te with
  | C.Rel m when List.mem m safes -> true
- | C.Rel _ -> false
- | C.LetIn _ -> raise (AssertFailure (lazy "letin after whd"))
- | C.Sort _ | C.Implicit _ | C.Prod _ | C.Lambda _ 
- | C.Const (Ref.Ref (_,_,(Ref.Decl | Ref.Def | Ref.Ind _ | Ref.CoFix _))) ->
-    raise (AssertFailure (lazy "not a constructor"))
- | C.Appl ([]|[_]) -> raise (AssertFailure (lazy "empty/unary appl"))
+ | C.Lambda (name, s, t) ->
+     is_really_smaller ~subst ~metasenv (shift_k (name, C.Decl s) k) t
  | C.Appl (he::_) ->
-    (*CSC: sulla coda ci vogliono dei controlli? secondo noi no, ma *)
-    (*CSC: solo perche' non abbiamo trovato controesempi            *)
-    (*TASSI: da capire soprattutto se he è un altro fix che non ha ridotto...*)
-    is_really_smaller ~subst k he
+     is_really_smaller ~subst ~metasenv k he
+ | C.Appl _
+ | C.Rel _ 
  | C.Const (Ref.Ref (_,_,Ref.Con _)) -> false
  | C.Const (Ref.Ref (_,_,Ref.Fix _)) -> assert false
    (*| C.Fix (_, fl) ->
@@ -1121,24 +1039,23 @@ and is_really_smaller ~subst (context, recfuns, x, safes as k) te =
             is_really_smaller ~subst (tys@context) n_plus_len nn_plus_len kl
              x_plus_len safes' bo
          ) fl true*)
- | C.Meta _ -> 
-     true (* XXX if this check is repeated when the user completes the
-             definition *)
+ | C.Meta _ -> true 
  | C.Match (Ref.Ref (_,uri,_) as ref,outtype,term,pl) ->
     (match term with
     | C.Rel m | C.Appl (C.Rel m :: _ ) when List.mem m safes || m = x ->
         let isinductive, paramsno, tl, _, i = E.get_checked_indtys ref in
         if not isinductive then
-          List.for_all (is_really_smaller ~subst k) pl
+          List.for_all (is_really_smaller ~subst ~metasenv k) pl
         else
           let c_ctx,len,cl = fix_lefts_in_constrs ~subst uri paramsno tl i in
           List.for_all2
            (fun p (_,_,debruijnedte) -> 
-             let rl' = recursive_args ~subst c_ctx 0 len debruijnedte in
+             let rl'=recursive_args ~subst ~metasenv c_ctx 0 len debruijnedte in
              let e, k = get_new_safes ~subst k p rl' in
-             is_really_smaller ~subst k e)
+             is_really_smaller ~subst ~metasenv k e)
            pl cl
-    | _ -> List.for_all (is_really_smaller ~subst k) pl)
+    | _ -> List.for_all (is_really_smaller ~subst ~metasenv k) pl)
+ | _ -> assert false
 
 and returns_a_coinductive ~subst context ty =
   match R.whd ~subst context ty with
@@ -1159,8 +1076,6 @@ and type_of_constant ((Ref.Ref (_,uri,_)) as ref) =
        check_obj_well_typed uobj;
        E.add_obj uobj;
        !logger (`Type_checking_completed uri);
-       if not (fst (E.get_obj uri)) then
-         raise (AssertFailure (lazy "environment error"));
        uobj
   in
   match cobj, ref with
@@ -1181,17 +1096,21 @@ and check_obj_well_typed (uri,height,metasenv,subst,kind) =
  assert (metasenv = [] && subst = []);
  match kind with
    | C.Constant (_,_,Some te,ty,_) ->
-      prerr_endline ("TY: " ^ NCicPp.ppterm ty);
-      prerr_endline ("BO: " ^ NCicPp.ppterm te);
+(*
+      prerr_endline ("TY: " ^ NCicPp.ppterm ~subst ~metasenv ~context:[] ty);
+      prerr_endline ("BO: " ^ NCicPp.ppterm ~subst ~metasenv ~context:[] te);
+*)
       let _ = typeof ~subst ~metasenv [] ty in
       let ty_te = typeof ~subst ~metasenv [] te in
-      prerr_endline "XXXX";
+(*       prerr_endline "XXXX"; *)
       if not (R.are_convertible ~subst ~metasenv [] ty_te ty) then
        raise (TypeCheckerFailure (lazy (Printf.sprintf
         "the type of the body is not the one expected:\n%s\nvs\n%s"
-        (NCicPp.ppterm ty_te) (NCicPp.ppterm ty))))
+        (NCicPp.ppterm ~subst ~metasenv ~context:[] ty_te) 
+        (NCicPp.ppterm ~subst ~metasenv ~context:[] ty))))
    | C.Constant (_,_,None,ty,_) -> ignore (typeof ~subst ~metasenv [] ty)
-   | C.Inductive _ as obj -> check_mutual_inductive_defs obj
+   | C.Inductive (is_ind, leftno, tyl, _) -> 
+       check_mutual_inductive_defs uri ~metasenv ~subst is_ind leftno tyl
    | C.Fixpoint (inductive,fl,_) ->
       let types,kl,len =
         List.fold_left
@@ -1207,14 +1126,13 @@ and check_obj_well_typed (uri,height,metasenv,subst,kind) =
          then raise (TypeCheckerFailure (lazy ("(Co)Fix: ill-typed bodies")))
          else
           if inductive then begin
-            let m, context = eat_lambdas ~subst types (x + 1) bo in
+            let m, context = eat_lambdas ~subst ~metasenv types (x + 1) bo in
             (* guarded by destructors conditions D{f,k,x,M} *)
             let rec enum_from k = 
               function [] -> [] | v::tl -> (k,v)::enum_from (k+1) tl 
             in
-            if not (guarded_by_destructors 
-                      ~subst context (enum_from (x+1) kl) m) then
-              raise(TypeCheckerFailure(lazy("Fix: not guarded by destructors")))
+            guarded_by_destructors 
+             ~subst ~metasenv context (enum_from (x+2) kl) m
           end else
            match returns_a_coinductive ~subst [] ty with
             | None ->
@@ -1222,7 +1140,7 @@ and check_obj_well_typed (uri,height,metasenv,subst,kind) =
                   (lazy "CoFix: does not return a coinductive type"))
             | Some uri ->
                 (* guarded by constructors conditions C{f,M} *)
-                if not (guarded_by_constructors ~subst
+                if not (guarded_by_constructors ~subst ~metasenv
                     types 0 len false bo [] uri)
                 then
                   raise (TypeCheckerFailure