X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_proof_checking%2FcicTypeChecker.ml;h=6cbb44f8044432db90ae2cd361d2831cb132be8d;hb=d025518bc5930796c748704b069a2719b34b00d3;hp=5f1c933f2f0e295e03904c6ca05348012f09dae8;hpb=6a95acad523131e0775e703d5d4bfac756609fb0;p=helm.git

diff --git a/helm/software/components/cic_proof_checking/cicTypeChecker.ml b/helm/software/components/cic_proof_checking/cicTypeChecker.ml
index 5f1c933f2..6cbb44f80 100644
--- a/helm/software/components/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/software/components/cic_proof_checking/cicTypeChecker.ml
@@ -54,7 +54,22 @@ let rec split l n =
       raise (TypeCheckerFailure (lazy "Parameters number < left parameters number"))
 ;;
 
-let debrujin_constructor ?(cb=fun _ _ -> ()) uri number_of_types =
+(* XXX: bug *)
+let ugraph_convertibility ug1 ug2 ul2 = true;;
+
+let check_and_clean_ugraph inferred_ugraph unchecked_ugraph uri obj =
+ match unchecked_ugraph with
+ | Some (ug,ul) ->
+     if not (ugraph_convertibility inferred_ugraph ug ul) then
+       raise (TypeCheckerFailure (lazy 
+         ("inferred univ graph not equal with declared ugraph")))
+     else 
+      ug,ul,obj
+ | None -> 
+     CicUnivUtils.clean_and_fill uri obj inferred_ugraph 
+;;
+
+let debrujin_constructor ?(cb=fun _ _ -> ()) ?(check_exp_named_subst=true) uri number_of_types context =
  let rec aux k t =
   let module C = Cic in
   let res =
@@ -83,7 +98,7 @@ let debrujin_constructor ?(cb=fun _ _ -> ()) uri number_of_types =
        in
         C.Const (uri,exp_named_subst')
     | C.MutInd (uri',tyno,exp_named_subst) when UriManager.eq uri uri' ->
-       if exp_named_subst != [] then
+       if check_exp_named_subst && exp_named_subst != [] then
         raise (TypeCheckerFailure
           (lazy ("non-empty explicit named substitution is applied to "^
            "a mutual inductive type which is being defined"))) ;
@@ -121,79 +136,68 @@ let debrujin_constructor ?(cb=fun _ _ -> ()) uri number_of_types =
    cb t res;
    res
  in
-  aux 0
+  aux (List.length context)
 ;;
 
 exception CicEnvironmentError;;
 
-let rec type_of_constant ~logger uri ugraph =
+let rec type_of_constant ~logger uri orig_ugraph =
  let module C = Cic in
  let module R = CicReduction in
  let module U = UriManager in
  let cobj,ugraph =
-   match CicEnvironment.is_type_checked ~trust:true ugraph uri with
+   match CicEnvironment.is_type_checked ~trust:true orig_ugraph uri with
       CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph'
-    | CicEnvironment.UncheckedObj uobj ->
+    | CicEnvironment.UncheckedObj (uobj,unchecked_ugraph) ->
        logger#log (`Start_type_checking uri) ;
        (* let's typecheck the uncooked obj *)
-
-(****************************************************************
-  TASSI: FIXME qui e' inutile ricordarselo, 
-  tanto poi lo richiediamo alla cache che da quello su disco
-*****************************************************************) 
-
-       let ugraph_dust = 
-         (match uobj with
+       let inferred_ugraph = 
+         match uobj with
            C.Constant (_,Some te,ty,_,_) ->
-           let _,ugraph = type_of ~logger ty ugraph in
-           let type_of_te,ugraph' = type_of ~logger te ugraph in
-              let b',ugraph'' = (R.are_convertible [] type_of_te ty ugraph') in
-              if not b' then
+           let _,ugraph = type_of ~logger ty CicUniv.empty_ugraph in
+           let type_of_te,ugraph = type_of ~logger te ugraph in
+              let b,ugraph = R.are_convertible [] type_of_te ty ugraph in
+              if not b then
                raise (TypeCheckerFailure (lazy (sprintf
                 "the constant %s is not well typed because the type %s of the body is not convertible to the declared type %s"
                 (U.string_of_uri uri) (CicPp.ppterm type_of_te)
                 (CicPp.ppterm ty))))
               else
-                ugraph'
+                ugraph
          | C.Constant (_,None,ty,_,_) ->
            (* only to check that ty is well-typed *)
-           let _,ugraph' = type_of ~logger ty ugraph in 
-           ugraph'
+           let _,ugraph = type_of ~logger ty CicUniv.empty_ugraph in 
+           ugraph
          | C.CurrentProof (_,conjs,te,ty,_,_) ->
-             let _,ugraph1 =
+             let _,ugraph =
               List.fold_left
                (fun (metasenv,ugraph) ((_,context,ty) as conj) ->
-                 let _,ugraph' = 
-		   type_of_aux' ~logger metasenv context ty ugraph 
+                 let _,ugraph = 
+		  type_of_aux' ~logger metasenv context ty ugraph 
 		 in
-                 (metasenv @ [conj],ugraph')
-               ) ([],ugraph) conjs
+                 (metasenv @ [conj],ugraph)
+               ) ([],CicUniv.empty_ugraph) conjs
              in
-              let _,ugraph2 = type_of_aux' ~logger conjs [] ty ugraph1 in
-               let type_of_te,ugraph3 = 
-		 type_of_aux' ~logger conjs [] te ugraph2 
-	       in
-               let b,ugraph4 = (R.are_convertible [] type_of_te ty ugraph3) in
+             let _,ugraph = type_of_aux' ~logger conjs [] ty ugraph in
+             let type_of_te,ugraph = type_of_aux' ~logger conjs [] te ugraph in
+             let b,ugraph = R.are_convertible [] type_of_te ty ugraph in
                if not b then
                  raise (TypeCheckerFailure (lazy (sprintf
                   "the current proof %s is not well typed because the type %s of the body is not convertible to the declared type %s"
                   (U.string_of_uri uri) (CicPp.ppterm type_of_te)
                   (CicPp.ppterm ty))))
                else 
-                 ugraph4
+                 ugraph
          | _ ->
              raise
-              (TypeCheckerFailure (lazy ("Unknown constant:" ^ U.string_of_uri uri))))
+              (TypeCheckerFailure (lazy ("Unknown constant:" ^ U.string_of_uri uri)))
        in 
-	 try
-	   CicEnvironment.set_type_checking_info uri;
-	   logger#log (`Type_checking_completed uri) ;
-	   match CicEnvironment.is_type_checked ~trust:false ugraph uri with
-               CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph'
-             | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError
-	 with Invalid_argument s ->
-	   (*debug_print (lazy s);*)
-	   uobj,ugraph_dust       
+       let ugraph, ul, obj = check_and_clean_ugraph inferred_ugraph unchecked_ugraph uri uobj in
+       CicEnvironment.set_type_checking_info uri (obj, ugraph, ul);
+       logger#log (`Type_checking_completed uri) ;
+       match CicEnvironment.is_type_checked ~trust:false orig_ugraph uri with
+           CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph'
+         | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError
   in
    match cobj,ugraph with
       (C.Constant (_,_,ty,_,_)),g -> ty,g
@@ -201,42 +205,43 @@ let rec type_of_constant ~logger uri ugraph =
     | _ ->
         raise (TypeCheckerFailure (lazy ("Unknown constant:" ^ U.string_of_uri uri)))
 
-and type_of_variable ~logger uri ugraph =
+and type_of_variable ~logger uri orig_ugraph =
  let module C = Cic in
  let module R = CicReduction in
  let module U = UriManager in
   (* 0 because a variable is never cooked => no partial cooking at one level *)
-  match CicEnvironment.is_type_checked ~trust:true ugraph uri with
-     CicEnvironment.CheckedObj ((C.Variable (_,_,ty,_,_)),ugraph') -> ty,ugraph'
-   | CicEnvironment.UncheckedObj (C.Variable (_,bo,ty,_,_)) ->
+  match CicEnvironment.is_type_checked ~trust:true orig_ugraph uri with
+  | CicEnvironment.CheckedObj ((C.Variable (_,_,ty,_,_)),ugraph') -> ty,ugraph'
+  | CicEnvironment.UncheckedObj 
+     (C.Variable (_,bo,ty,_,_) as uobj, unchecked_ugraph) 
+    ->
       logger#log (`Start_type_checking uri) ;
       (* only to check that ty is well-typed *)
-      let _,ugraph1 = type_of ~logger ty ugraph in
-      let ugraph2 = 
-       (match bo with
+      let _,ugraph = type_of ~logger ty CicUniv.empty_ugraph in
+      let inferred_ugraph = 
+       match bo with
            None -> ugraph
          | Some bo ->
-	     let ty_bo,ugraph' = type_of ~logger bo ugraph1 in
-             let b,ugraph'' = (R.are_convertible [] ty_bo ty ugraph') in
+	     let ty_bo,ugraph = type_of ~logger bo ugraph in
+             let b,ugraph = R.are_convertible [] ty_bo ty ugraph in
              if not b then
               raise (TypeCheckerFailure
                 (lazy ("Unknown variable:" ^ U.string_of_uri uri)))
 	     else
-	       ugraph'') 
+	       ugraph 
       in
-	(try
-	   CicEnvironment.set_type_checking_info uri ;
-	   logger#log (`Type_checking_completed uri) ;
-	   match CicEnvironment.is_type_checked ~trust:false ugraph uri with
-               CicEnvironment.CheckedObj ((C.Variable (_,_,ty,_,_)),ugraph') -> 
-		 ty,ugraph'
-	     | CicEnvironment.CheckedObj _ 
-             | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError
-         with Invalid_argument s ->
-           (*debug_print (lazy s);*)
-           ty,ugraph2)
+       let ugraph, ul, obj = 
+         check_and_clean_ugraph inferred_ugraph unchecked_ugraph uri uobj 
+       in
+       CicEnvironment.set_type_checking_info uri (obj, ugraph, ul);
+       logger#log (`Type_checking_completed uri) ;
+       (match CicEnvironment.is_type_checked ~trust:false orig_ugraph uri with
+           CicEnvironment.CheckedObj((C.Variable(_,_,ty,_,_)),ugraph)->ty,ugraph
+         | CicEnvironment.CheckedObj _ 
+         | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError)
    |  _ ->
-	raise (TypeCheckerFailure (lazy ("Unknown variable:" ^ U.string_of_uri uri)))
+	raise (TypeCheckerFailure (lazy 
+          ("Unknown variable:" ^ U.string_of_uri uri)))
 
 and does_not_occur ?(subst=[]) context n nn te =
  let module C = Cic in
@@ -264,14 +269,15 @@ and does_not_occur ?(subst=[]) context n nn te =
         with
          CicUtil.Subst_not_found _ -> true)
     | C.Cast (te,ty) ->
-       does_not_occur ~subst context n nn te && does_not_occur ~subst context n nn ty
+       does_not_occur ~subst context n nn te && 
+       does_not_occur ~subst context n nn ty
     | C.Prod (name,so,dest) ->
        does_not_occur ~subst context n nn so &&
         does_not_occur ~subst ((Some (name,(C.Decl so)))::context) (n + 1)
          (nn + 1) dest
     | C.Lambda (name,so,dest) ->
        does_not_occur ~subst context n nn so &&
-        does_not_occur ~subst ((Some (name,(C.Decl so)))::context) (n + 1) (nn + 1)
+        does_not_occur ~subst ((Some (name,(C.Decl so)))::context) (n+1) (nn+1)
          dest
     | C.LetIn (name,so,ty,dest) ->
        does_not_occur ~subst context n nn so &&
@@ -279,16 +285,17 @@ and does_not_occur ?(subst=[]) context n nn te =
          does_not_occur ~subst ((Some (name,(C.Def (so,ty))))::context)
           (n + 1) (nn + 1) dest
     | C.Appl l ->
-       List.fold_right (fun x i -> i && does_not_occur ~subst context n nn x) l true
+       List.for_all (does_not_occur ~subst context n nn) l
     | C.Var (_,exp_named_subst)
     | C.Const (_,exp_named_subst)
     | C.MutInd (_,_,exp_named_subst)
     | C.MutConstruct (_,_,_,exp_named_subst) ->
-       List.fold_right (fun (_,x) i -> i && does_not_occur ~subst context n nn x)
-        exp_named_subst true
+       List.for_all (fun (_,x) -> does_not_occur ~subst context n nn x)
+        exp_named_subst
     | C.MutCase (_,_,out,te,pl) ->
-       does_not_occur ~subst context n nn out && does_not_occur ~subst context n nn te &&
-        List.fold_right (fun x i -> i && does_not_occur ~subst context n nn x) pl true
+       does_not_occur ~subst context n nn out && 
+       does_not_occur ~subst context n nn te &&
+       List.for_all (does_not_occur ~subst context n nn) pl
     | C.Fix (_,fl) ->
        let len = List.length fl in
         let n_plus_len = n + len in
@@ -550,25 +557,35 @@ and typecheck_mutual_inductive_defs ~logger uri (itl,_,indparamsno) ugraph =
   (* 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
+    List.rev_map (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) itl in
   let _,ugraph2 =
     List.fold_right
-      (fun (_,_,_,cl) (i,ugraph) ->
+      (fun (_,_,ty,cl) (i,ugraph) ->
+        let _,ty_sort = split_prods ~subst:[] [] ~-1 ty in
 	let ugraph'' = 
           List.fold_left
             (fun ugraph (name,te) -> 
-              let debrujinedte = debrujin_constructor uri len te in
-              let augmented_term =
-		List.fold_right
-		  (fun (name,_,ty,_) i -> Cic.Prod (Cic.Name name, ty, i))
-		  itl debrujinedte
-              in
-              let _,ugraph' = type_of ~logger augmented_term ugraph in
+              let te = debrujin_constructor uri len [] te in
+              let context,te = split_prods ~subst:[] tys indparamsno te in
+              let con_sort,ugraph = type_of_aux' ~logger [] context te ugraph in
+              let ugraph =
+               match
+                CicReduction.whd context con_sort, CicReduction.whd [] ty_sort
+               with
+                  Cic.Sort (Cic.Type u1), Cic.Sort (Cic.Type u2) ->
+                   CicUniv.add_ge u2 u1 ugraph
+                | Cic.Sort _, Cic.Sort Cic.Prop
+                | Cic.Sort Cic.CProp, Cic.Sort Cic.CProp
+                | Cic.Sort _, Cic.Sort Cic.Type _ -> ugraph
+                | _, _ ->
+                   raise
+                    (TypeCheckerFailure
+                      (lazy ("Wrong constructor or inductive arity shape"))) in
               (* let's check also the positivity conditions *)
               if
 		not
-		  (are_all_occurrences_positive tys uri indparamsno i 0 len
-                     debrujinedte)
+		  (are_all_occurrences_positive context uri indparamsno
+                    (i+indparamsno) indparamsno (len+indparamsno) te)
               then
                 begin
                 prerr_endline (UriManager.string_of_uri uri);
@@ -577,7 +594,7 @@ and typecheck_mutual_inductive_defs ~logger uri (itl,_,indparamsno) ugraph =
 		  (TypeCheckerFailure
                     (lazy ("Non positive occurence in " ^ U.string_of_uri uri)))                end 
               else
-		ugraph'
+		ugraph
             ) ugraph cl in
 	(i + 1),ugraph''
       ) itl (1,ugrap1)
@@ -595,65 +612,55 @@ and check_mutual_inductive_defs uri obj ugraph =
 		lazy ("Unknown mutual inductive definition:" ^
 		 UriManager.string_of_uri uri)))
 
-and type_of_mutual_inductive_defs ~logger uri i ugraph =
+and type_of_mutual_inductive_defs ~logger uri i orig_ugraph =
  let module C = Cic in
  let module R = CicReduction in
  let module U = UriManager in
   let cobj,ugraph1 =
-   match CicEnvironment.is_type_checked ~trust:true ugraph uri with
+   match CicEnvironment.is_type_checked ~trust:true orig_ugraph uri with
        CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph'
-     | CicEnvironment.UncheckedObj uobj ->
+     | CicEnvironment.UncheckedObj (uobj,unchecked_ugraph) ->
 	 logger#log (`Start_type_checking uri) ;
-	 let ugraph1_dust = 
-	   check_mutual_inductive_defs ~logger uri uobj ugraph 
-	 in
-	   (* TASSI: FIXME: check ugraph1 == ugraph ritornato da env *)
-	   try 
-	     CicEnvironment.set_type_checking_info uri ;
-	     logger#log (`Type_checking_completed uri) ;
-	     (match CicEnvironment.is_type_checked ~trust:false ugraph uri with
-		  CicEnvironment.CheckedObj (cobj,ugraph') -> (cobj,ugraph')
-		| CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError
-	     )
-	   with
-	       Invalid_argument s ->
-		 (*debug_print (lazy s);*)
-		 uobj,ugraph1_dust
+	 let inferred_ugraph = 
+           check_mutual_inductive_defs ~logger uri uobj CicUniv.empty_ugraph 
+         in
+         let ugraph, ul, obj = check_and_clean_ugraph inferred_ugraph unchecked_ugraph uri uobj in
+	 CicEnvironment.set_type_checking_info uri (obj,ugraph,ul);
+	 logger#log (`Type_checking_completed uri) ;
+	 (match CicEnvironment.is_type_checked ~trust:false orig_ugraph uri with
+	      CicEnvironment.CheckedObj (cobj,ugraph') -> (cobj,ugraph')
+	    | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError
+	 )
   in
-    match cobj with
-	C.InductiveDefinition (dl,_,_,_) ->
-	  let (_,_,arity,_) = List.nth dl i in
-	    arity,ugraph1
-      | _ ->
-	  raise (TypeCheckerFailure
-           (lazy ("Unknown mutual inductive definition:" ^ U.string_of_uri uri)))
+  match cobj with
+  | C.InductiveDefinition (dl,_,_,_) ->
+      let (_,_,arity,_) = List.nth dl i in
+        arity,ugraph1
+  | _ ->
+     raise (TypeCheckerFailure
+      (lazy ("Unknown mutual inductive definition:" ^ U.string_of_uri uri)))
 	    
-and type_of_mutual_inductive_constr ~logger uri i j ugraph =
+and type_of_mutual_inductive_constr ~logger uri i j orig_ugraph =
  let module C = Cic in
  let module R = CicReduction in
  let module U = UriManager in
   let cobj,ugraph1 =
-    match CicEnvironment.is_type_checked ~trust:true ugraph uri with
+    match CicEnvironment.is_type_checked ~trust:true orig_ugraph uri with
 	CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph'
-      | CicEnvironment.UncheckedObj uobj ->
+      | CicEnvironment.UncheckedObj (uobj,unchecked_ugraph) ->
 	  logger#log (`Start_type_checking uri) ;
-	  let ugraph1_dust = 
-	    check_mutual_inductive_defs ~logger uri uobj ugraph 
+	  let inferred_ugraph = 
+	    check_mutual_inductive_defs ~logger uri uobj CicUniv.empty_ugraph 
 	  in
-	    (* check ugraph1 validity ??? == ugraph' *)
-	    try
-	      CicEnvironment.set_type_checking_info uri ;
-	      logger#log (`Type_checking_completed uri) ;
-	      (match 
-                 CicEnvironment.is_type_checked ~trust:false ugraph uri 
-               with
+          let ugraph, ul, obj = check_and_clean_ugraph inferred_ugraph unchecked_ugraph uri uobj in
+	  CicEnvironment.set_type_checking_info uri (obj, ugraph, ul);
+	  logger#log (`Type_checking_completed uri) ;
+	  (match 
+             CicEnvironment.is_type_checked ~trust:false orig_ugraph uri 
+           with
 		 CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph' 
 	       | CicEnvironment.UncheckedObj _ -> 
 		       raise CicEnvironmentError)
-	    with
-		Invalid_argument s ->
-		  (*debug_print (lazy s);*)
-		  uobj,ugraph1_dust
   in
     match cobj with
 	C.InductiveDefinition (dl,_,_,_) ->
@@ -666,65 +673,53 @@ and type_of_mutual_inductive_constr ~logger uri i j ugraph =
 
 and recursive_args context n nn te =
  let module C = Cic in
-  match CicReduction.whd context te with
-     C.Rel _ -> []
-   | C.Var _
-   | C.Meta _
-   | C.Sort _
-   | C.Implicit _
-   | C.Cast _ (*CSC ??? *) ->
-      raise (AssertFailure (lazy "3")) (* due to type-checking *)
-   | C.Prod (name,so,de) ->
-      (not (does_not_occur context n nn so)) ::
-       (recursive_args ((Some (name,(C.Decl so)))::context) (n+1) (nn + 1) de)
-   | C.Lambda _
-   | C.LetIn _ ->
-      raise (AssertFailure (lazy "4")) (* due to type-checking *)
-   | C.Appl _ -> []
-   | C.Const _ -> raise (AssertFailure (lazy "5"))
-   | C.MutInd _
-   | C.MutConstruct _
-   | C.MutCase _
-   | C.Fix _
-   | C.CoFix _ -> raise (AssertFailure (lazy "6")) (* due to type-checking *)
+ match CicReduction.whd context te with
+    C.Rel _ 
+  | C.MutInd _ -> []
+  | C.Var _
+  | C.Meta _
+  | C.Sort _
+  | C.Implicit _
+  | C.Cast _ (*CSC ??? *) ->
+     raise (AssertFailure (lazy "3")) (* due to type-checking *)
+  | C.Prod (name,so,de) ->
+     (not (does_not_occur context n nn so)) ::
+      (recursive_args ((Some (name,(C.Decl so)))::context) (n+1) (nn + 1) de)
+  | C.Lambda _
+  | C.LetIn _ ->
+     raise (AssertFailure (lazy "4")) (* due to type-checking *)
+  | C.Appl _ -> []
+  | C.Const _ -> raise (AssertFailure (lazy "5"))
+  | C.MutConstruct _
+  | C.MutCase _
+  | C.Fix _
+  | C.CoFix _ -> raise (AssertFailure (lazy "6")) (* due to type-checking *)
 
-and get_new_safes ~subst context p c rl safes n nn x =
+and get_new_safes ~subst context p rl safes n nn x =
  let module C = Cic in
  let module U = UriManager in
  let module R = CicReduction in
-  match (R.whd ~subst context c, R.whd ~subst context p, rl) with
-     (C.Prod (_,so,ta1), C.Lambda (name,_,ta2), b::tl) ->
-       (* we are sure that the two sources are convertible because we *)
-       (* have just checked this. So let's go along ...               *)
-       let safes' =
-        List.map (fun x -> x + 1) safes
-       in
-        let safes'' =
-         if b then 1::safes' else safes'
-        in
-         get_new_safes ~subst ((Some (name,(C.Decl so)))::context)
-          ta2 ta1 tl safes'' (n+1) (nn+1) (x+1)
-   | (C.Prod _, (C.MutConstruct _ as e), _)
-   | (C.Prod _, (C.Rel _ as e), _)
-   | (C.MutInd _, e, [])
-   | (C.Appl _, e, []) -> (e,safes,n,nn,x,context)
-   | (c,p,l) ->
-      (* CSC: If the next exception is raised, it just means that   *)
-      (* CSC: the proof-assistant allows to use very strange things *)
-      (* CSC: as a branch of a case whose type is a Prod. In        *)
-      (* CSC: particular, this means that a new (C.Prod, x,_) case  *)
-      (* CSC: must be considered in this match. (e.g. x = MutCase)  *)
+  match R.whd ~subst context p, rl with
+   | C.Lambda (name,so,ta), b::tl ->
+       let safes = List.map (fun x -> x + 1) safes in
+       let safes = if b then 1::safes else safes in
+       get_new_safes ~subst ((Some (name,(C.Decl so)))::context)
+          ta tl safes (n+1) (nn+1) (x+1)
+   | C.MutConstruct _ as e, _
+   | (C.Rel _ as e), _
+   | e, [] -> (e,safes,n,nn,x,context)
+   | p,_::_ ->
       raise
        (AssertFailure (lazy
-         (Printf.sprintf "Get New Safes: c=%s ; p=%s"
-           (CicPp.ppterm c) (CicPp.ppterm p))))
+         (Printf.sprintf "Get New Safes: p=%s" (CicPp.ppterm p))))
 
 and split_prods ~subst context n te =
  let module C = Cic in
  let module R = CicReduction in
   match (n, R.whd ~subst context te) with
      (0, _) -> context,te
-   | (n, C.Prod (name,so,ta)) when n > 0 ->
+   | (n, C.Sort _) when n <= 0 -> context,te
+   | (n, C.Prod (name,so,ta)) ->
        split_prods ~subst ((Some (name,(C.Decl so)))::context) (n - 1) ta
    | (_, _) -> raise (AssertFailure (lazy "8"))
 
@@ -741,7 +736,34 @@ and eat_lambdas ~subst context n te =
    | (n, te) ->
        raise (AssertFailure (lazy (sprintf "9 (%d, %s)" n (CicPp.ppterm te))))
 
-and check_is_really_smaller_arg ~subst context n nn kl x safes te =
+and specialize_inductive_type ~logger ~subst ~metasenv context t = 
+  let ty,_= type_of_aux' ~logger ~subst metasenv context t CicUniv.oblivion_ugraph in
+  match CicReduction.whd ~subst context ty with
+  | Cic.MutInd (uri,_,exp) 
+  | Cic.Appl (Cic.MutInd (uri,_,exp) :: _) as ty ->
+      let args = match ty with Cic.Appl (_::tl) -> tl | _ -> [] in
+      let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
+      (match o with
+      | Cic.InductiveDefinition (tl,_,paramsno,_) ->
+          let left_args,_ = HExtlib.split_nth paramsno args in
+          List.map (fun (name, isind, arity, cl) ->
+            let arity = CicSubstitution.subst_vars exp arity in
+            let arity = instantiate_parameters left_args arity in
+            let cl =
+              List.map
+               (fun (id,ty) -> 
+                 let ty = CicSubstitution.subst_vars exp ty in
+                 id, instantiate_parameters left_args ty) 
+               cl 
+            in
+            name, isind, arity, cl)
+          tl, paramsno
+      | _ -> assert false)
+  | _ -> assert false
+
+and check_is_really_smaller_arg 
+  ~logger ~metasenv ~subst rec_uri rec_uri_len context n nn kl x safes te 
+=
  let module C = Cic in
  let module U = UriManager in
  (*CSC: we could perform beta-iota(-zeta?) immediately, and
@@ -749,65 +771,56 @@ and check_is_really_smaller_arg ~subst context n nn kl x safes te =
  match CicReduction.whd ~subst context te with
      C.Rel m when List.mem m safes -> true
    | C.Rel _ 
-   | C.Appl _
    | C.MutConstruct _
    | C.Const _
    | C.Var _ -> false
+   | C.Appl (he::_) ->
+        check_is_really_smaller_arg rec_uri rec_uri_len 
+          ~logger ~metasenv ~subst context n nn kl x safes he
    | C.Lambda (name,ty,ta) ->
-      check_is_really_smaller_arg ~subst (Some (name,Cic.Decl ty)::context)
-       (n+1) (nn+1) kl (x+1) (List.map (fun n -> n+1) safes) ta
+      check_is_really_smaller_arg rec_uri rec_uri_len 
+        ~logger ~metasenv ~subst (Some (name,Cic.Decl ty)::context)
+        (n+1) (nn+1) kl (x+1) (List.map (fun n -> n+1) safes) ta
    | C.MutCase (uri,i,outtype,term,pl) ->
       (match term with
-          C.Rel m | C.Appl ((C.Rel m)::_) when List.mem m safes || m = x ->
-           let (lefts_and_tys,len,isinductive,paramsno,cl) =
-            let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
-            match o with
-               C.InductiveDefinition (tl,_,paramsno,_) ->
-                let (_,isinductive,_,cl) = List.nth tl i in
-                 let tys =
-                  List.map (fun (n,_,ty,_) ->
-                   Some(Cic.Name n,(Cic.Decl ty))) tl
-                 in
-                  let cl' =
-                   List.map
-                    (fun (id,ty) ->
-                      (id, snd (split_prods ~subst tys paramsno ty))) cl in
-                  let lefts =
-                   match tl with
-                      [] -> assert false
-                    | (_,_,ty,_)::_ ->
-                       fst (split_prods ~subst [] paramsno ty)
-                  in
-                   (lefts@tys,List.length tl,isinductive,paramsno,cl')
-             | _ ->
-                raise (TypeCheckerFailure
-                  (lazy ("Unknown mutual inductive definition:" ^
-                  UriManager.string_of_uri uri)))
-           in
-            if not isinductive then
-              List.fold_right
-               (fun p i ->
-                 i && check_is_really_smaller_arg ~subst context n nn kl x safes p)
-               pl true
-            else
-              List.for_all2
-               (fun p (_,c) ->
-                 let rl' =
-                  let debrujinedte = debrujin_constructor uri len c in
-                   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
-                  check_is_really_smaller_arg 
-                    ~subst context' n' nn' kl x' safes' e
-               ) pl cl
+      | C.Rel m | C.Appl ((C.Rel m)::_) when List.mem m safes || m = x ->
+         let tys,_ = 
+           specialize_inductive_type ~logger ~subst ~metasenv context term 
+         in
+         let tys_ctx,_ = 
+           List.fold_left
+             (fun (types,len) (n,_,ty,_) ->
+               Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
+               len+1) 
+             ([],0) tys
+         in
+         let _,isinductive,_,cl = List.nth tys i in
+         if not isinductive then
+           List.for_all
+            (check_is_really_smaller_arg rec_uri rec_uri_len 
+              ~logger ~metasenv ~subst context n nn kl x safes)
+            pl
+         else
+           List.for_all2
+            (fun p (_,c) ->
+              let rec_params =
+               let c = 
+                 debrujin_constructor ~check_exp_named_subst:false
+                  rec_uri rec_uri_len context c in
+               let len_ctx = List.length context in
+               recursive_args (context@tys_ctx) len_ctx (len_ctx+rec_uri_len) c
+              in
+              let (e, safes',n',nn',x',context') =
+                get_new_safes ~subst context p rec_params safes n nn x
+              in
+               check_is_really_smaller_arg rec_uri rec_uri_len 
+                ~logger ~metasenv ~subst context' n' nn' kl x' safes' e
+            ) pl cl
         | _ ->
-          List.fold_right
-           (fun p i ->
-             i && check_is_really_smaller_arg ~subst context n nn kl x safes p
-           ) pl true
+          List.for_all
+           (check_is_really_smaller_arg 
+             rec_uri rec_uri_len ~logger ~metasenv ~subst 
+             context n nn kl x safes) pl
       )
    | C.Fix (_, fl) ->
       let len = List.length fl in
@@ -821,25 +834,30 @@ and check_is_really_smaller_arg ~subst context n nn kl x safes te =
               len+1)
 	  ) ([],0) fl
        and safes' = List.map (fun x -> x + len) safes in
-        List.fold_right
-         (fun (_,_,_,bo) i ->
-           i &&
-            check_is_really_smaller_arg ~subst (tys@context) n_plus_len nn_plus_len kl
+        List.for_all
+         (fun (_,_,_,bo) ->
+            check_is_really_smaller_arg 
+              rec_uri rec_uri_len ~logger ~metasenv ~subst 
+                (tys@context) n_plus_len nn_plus_len kl
              x_plus_len safes' bo
-         ) fl true
+         ) fl
    | t ->
       raise (AssertFailure (lazy ("An inhabitant of an inductive type in normal form cannot have this shape: " ^ CicPp.ppterm t)))
 
-and guarded_by_destructors ~subst context n nn kl x safes t =
+and guarded_by_destructors 
+  ~logger ~metasenv ~subst rec_uri rec_uri_len context n nn kl x safes t 
+=
  let module C = Cic in
  let module U = UriManager in
-  match CicReduction.whd ~subst context t with
+  let t = CicReduction.whd ~delta:false ~subst context t in
+  let res =
+   match t with
      C.Rel m when m > n && m <= nn -> false
    | C.Rel m ->
       (match List.nth context (m-1) with
           Some (_,C.Decl _) -> true
         | Some (_,C.Def (bo,_)) ->
-           guarded_by_destructors ~subst context n nn kl x safes
+           guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst context n nn kl x safes
             (CicSubstitution.lift m bo)
         | None -> raise (TypeCheckerFailure (lazy "Reference to deleted hypothesis"))
       )
@@ -847,164 +865,84 @@ and guarded_by_destructors ~subst context n nn kl x safes t =
    | C.Sort _
    | C.Implicit _ -> true
    | C.Cast (te,ty) ->
-      guarded_by_destructors ~subst context n nn kl x safes te &&
-       guarded_by_destructors ~subst context n nn kl x safes ty
+      guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst context n nn kl x safes te &&
+       guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst context n nn kl x safes ty
    | C.Prod (name,so,ta) ->
-      guarded_by_destructors ~subst context n nn kl x safes so &&
-       guarded_by_destructors ~subst ((Some (name,(C.Decl so)))::context)
+      guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst context n nn kl x safes so &&
+       guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst ((Some (name,(C.Decl so)))::context)
         (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
    | C.Lambda (name,so,ta) ->
-      guarded_by_destructors ~subst context n nn kl x safes so &&
-       guarded_by_destructors ~subst ((Some (name,(C.Decl so)))::context)
+      guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst context n nn kl x safes so &&
+       guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst ((Some (name,(C.Decl so)))::context)
         (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
    | C.LetIn (name,so,ty,ta) ->
-      guarded_by_destructors ~subst context n nn kl x safes so &&
-       guarded_by_destructors ~subst context n nn kl x safes ty &&
-        guarded_by_destructors ~subst ((Some (name,(C.Def (so,ty))))::context)
+      guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst context n nn kl x safes so &&
+       guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst context n nn kl x safes ty &&
+        guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst ((Some (name,(C.Def (so,ty))))::context)
          (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
    | C.Appl ((C.Rel m)::tl) when m > n && m <= nn ->
       let k = List.nth kl (m - n - 1) in
        if not (List.length tl > k) then false
        else
-        List.fold_right
-         (fun param i ->
-           i && guarded_by_destructors ~subst context n nn kl x safes param
-         ) tl true &&
-         check_is_really_smaller_arg ~subst context n nn kl x safes (List.nth tl k)
+        List.for_all
+         (guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst context n nn kl x safes) tl &&
+        check_is_really_smaller_arg 
+          rec_uri rec_uri_len 
+          ~logger ~metasenv ~subst context n nn kl x safes (List.nth tl k)
    | C.Var (_,exp_named_subst)
    | C.Const (_,exp_named_subst)
    | C.MutInd (_,_,exp_named_subst)
    | C.MutConstruct (_,_,_,exp_named_subst) ->
-      List.fold_right
-       (fun (_,t) i -> i && guarded_by_destructors ~subst context n nn kl x safes t)
-       exp_named_subst true
+      List.for_all
+       (fun (_,t) -> guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst context n nn kl x safes t)
+       exp_named_subst 
    | C.MutCase (uri,i,outtype,term,pl) ->
       (match CicReduction.whd ~subst context term with
-          C.Rel m when List.mem m safes || m = x ->
-           let (lefts_and_tys,len,isinductive,paramsno,cl) =
-	    let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
-            match o with
-               C.InductiveDefinition (tl,_,paramsno,_) ->
-                let len = List.length tl in
-                 let (_,isinductive,_,cl) = List.nth tl i in
-                  let tys =
-                   List.map (fun (n,_,ty,_) ->
-                    Some(Cic.Name n,(Cic.Decl ty))) tl
-                  in
-                   let cl' =
-                    List.map
-                     (fun (id,ty) ->
-                      let debrujinedty = debrujin_constructor uri len ty in
-                       (id, snd (split_prods ~subst tys paramsno ty),
-                        snd (split_prods ~subst tys paramsno debrujinedty)
-                       )) cl in
-                   let lefts =
-                    match tl with
-                       [] -> assert false
-                     | (_,_,ty,_)::_ ->
-                        fst (split_prods ~subst [] paramsno ty)
-                   in
-                    (lefts@tys,len,isinductive,paramsno,cl')
-             | _ ->
-                raise (TypeCheckerFailure
-                  (lazy ("Unknown mutual inductive definition:" ^
-                  UriManager.string_of_uri uri)))
+        | C.Rel m 
+        | C.Appl ((C.Rel m)::_) as t when List.mem m safes || m = x ->
+           let tl = match t with C.Appl (_::tl) -> tl | _ -> [] in
+           List.for_all
+             (guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst context n nn kl x safes)
+             tl &&
+           let tys,_ = 
+             specialize_inductive_type ~logger ~subst ~metasenv context t
            in
-            if not isinductive then
-             guarded_by_destructors ~subst context n nn kl x safes outtype &&
-              guarded_by_destructors ~subst context n nn kl x safes term &&
-              (*CSC: manca ??? il controllo sul tipo di term? *)
-              List.fold_right
-               (fun p i ->
-                 i && guarded_by_destructors ~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
-             guarded_by_destructors ~subst context n nn kl x safes outtype &&
-              (*CSC: manca ??? il controllo sul tipo di term? *)
-              List.fold_right
-               (fun (p,(name,c,brujinedc)) i ->
-                   i &&
-                 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
-                   guarded_by_destructors ~subst context' n' nn' kl x' safes' e
-               ) pl_and_cl true
-        | C.Appl ((C.Rel m)::tl) when List.mem m safes || m = x ->
-           let (lefts_and_tys,len,isinductive,paramsno,cl) =
-	    let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
-            match o with
-               C.InductiveDefinition (tl,_,paramsno,_) ->
-                let (_,isinductive,_,cl) = List.nth tl i in
-                 let tys =
-                  List.map
-                   (fun (n,_,ty,_) -> Some(Cic.Name n,(Cic.Decl ty))) tl
-                 in
-                  let cl' =
-                   List.map
-                    (fun (id,ty) ->
-                      (id, snd (split_prods ~subst tys paramsno ty))) cl in
-                  let lefts =
-                   match tl with
-                      [] -> assert false
-                    | (_,_,ty,_)::_ ->
-                       fst (split_prods ~subst [] paramsno ty)
-                  in
-                   (lefts@tys,List.length tl,isinductive,paramsno,cl')
-             | _ ->
-                raise (TypeCheckerFailure
-                  (lazy ("Unknown mutual inductive definition:" ^
-                  UriManager.string_of_uri uri)))
+           let tys_ctx,_ = 
+             List.fold_left
+               (fun (types,len) (n,_,ty,_) ->
+                 Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
+                 len+1) 
+               ([],0) tys
            in
+           let _,isinductive,_,cl = List.nth tys i in
             if not isinductive then
-             guarded_by_destructors ~subst context n nn kl x safes outtype &&
-              guarded_by_destructors ~subst context n nn kl x safes term &&
-              (*CSC: manca ??? il controllo sul tipo di term? *)
-              List.fold_right
-               (fun p i ->
-                 i && guarded_by_destructors ~subst context n nn kl x safes p)
-               pl true
+             guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst context n nn kl x safes outtype &&
+              guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst context n nn kl x safes term &&
+              List.for_all
+               (guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst context n nn kl x safes)
+               pl
             else
-             let pl_and_cl =
-              try
-               List.combine pl cl
-              with
-               Invalid_argument _ ->
-                raise (TypeCheckerFailure (lazy "not enough patterns"))
-             in
-             guarded_by_destructors ~subst context n nn kl x safes outtype &&
-              (*CSC: manca ??? il controllo sul tipo di term? *)
-              List.fold_right
-               (fun t i ->
-                 i && guarded_by_destructors ~subst context n nn kl x safes t)
-               tl true &&
-              List.fold_right
-               (fun (p,(_,c)) i ->
-                 let rl' =
-                  let debrujinedte = debrujin_constructor uri len c in
-                   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 &&
-                   guarded_by_destructors ~subst context' n' nn' kl x' safes' e
-               ) pl_and_cl true
+             guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst context n nn kl x safes outtype &&
+             List.for_all2
+              (fun p (_,c) ->
+               let rec_params =
+                let c = 
+                 debrujin_constructor ~check_exp_named_subst:false 
+                  rec_uri rec_uri_len context c in
+                let len_ctx = List.length context in
+                recursive_args (context@tys_ctx) len_ctx (len_ctx+rec_uri_len) c
+               in
+               let (e, safes',n',nn',x',context') =
+                get_new_safes ~subst context p rec_params safes n nn x
+               in
+                guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst context' n' nn' kl x' safes' e
+               ) pl cl
         | _ ->
-          guarded_by_destructors ~subst context n nn kl x safes outtype &&
-           guarded_by_destructors ~subst context n nn kl x safes term &&
+          guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst context n nn kl x safes outtype &&
+           guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst context n nn kl x safes term &&
            (*CSC: manca ??? il controllo sul tipo di term? *)
            List.fold_right
-            (fun p i -> i && guarded_by_destructors ~subst context n nn kl x safes p)
+            (fun p i -> i && guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst context n nn kl x safes p)
             pl true
       )
    | C.Appl (C.Fix (fixno, fl)::_) | C.Fix (fixno,fl) as t->
@@ -1021,29 +959,30 @@ and guarded_by_destructors ~subst context n nn kl x safes t =
 	  ) ([],0) fl in
        let safes' = List.map (fun x -> x + len) safes in
         List.for_all
-         (guarded_by_destructors ~subst context n nn kl x safes) l &&
+         (guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst context n nn kl x safes) l &&
         snd (List.fold_left
          (fun (fixno',i) (_,recno,ty,bo) ->
            fixno'+1,
            i &&
-           guarded_by_destructors ~subst context n nn kl x_plus_len safes' ty &&
+           guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst context n nn kl x_plus_len safes' ty &&
            if
             fixno' = fixno &&
             List.length l > recno &&
             (*case where the recursive argument is already really_smaller *)
-            check_is_really_smaller_arg ~subst context n nn kl x safes
-             (List.nth l recno)
+            check_is_really_smaller_arg 
+              rec_uri rec_uri_len ~logger ~metasenv ~subst context n nn kl x safes
+              (List.nth l recno)
            then
             let bo_without_lambdas,_,context =
              eat_lambdas ~subst (tys@context) (recno+1) bo
             in
              (* we assume the formal argument to be safe *)
-             guarded_by_destructors ~subst context (n_plus_len+recno+1)
+             guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst context (n_plus_len+recno+1)
               (nn_plus_len+recno+1) kl (x_plus_len+recno+1)
               (1::List.map (fun x -> x+recno+1) safes')
               bo_without_lambdas
            else
-            guarded_by_destructors ~subst (tys@context) n_plus_len nn_plus_len
+            guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst (tys@context) n_plus_len nn_plus_len
              kl x_plus_len safes' bo
          ) (0,true) fl)
    | C.CoFix (_, fl) ->
@@ -1061,236 +1000,132 @@ and guarded_by_destructors ~subst context n nn kl x safes t =
         List.fold_right
          (fun (_,ty,bo) i ->
            i &&
-            guarded_by_destructors ~subst context n nn kl x_plus_len safes' ty &&
-            guarded_by_destructors ~subst (tys@context) n_plus_len nn_plus_len kl
+            guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst context n nn kl x_plus_len safes' ty &&
+            guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst (tys@context) n_plus_len nn_plus_len kl
              x_plus_len safes' bo
          ) fl true
    | C.Appl tl ->
       List.fold_right
-       (fun t i -> i && guarded_by_destructors ~subst context n nn kl x safes t)
+       (fun t i -> i && guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst context n nn kl x safes t)
        tl true
+  in
+   if res then res
+   else
+    let t' = CicReduction.whd ~subst context t in
+     if t = t' then
+      false
+     else
+      guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst context n nn kl x safes t'
 
 (* 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.                            *)
-and guarded_by_constructors ~subst context n nn h te args coInductiveTypeURI =
+and guarded_by_constructors ~logger ~subst ~metasenv indURI =
  let module C = Cic in
-  (*CSC: There is a lot of code replication between the cases X and    *)
-  (*CSC: (C.Appl X tl). Maybe it will be better to define a function   *)
-  (*CSC: that maps X into (C.Appl X []) when X is not already a C.Appl *)
+ let rec aux context n nn h te =
   match CicReduction.whd ~subst context te with
-     C.Rel m when m > n && m <= nn -> h
-   | C.Rel _ -> true
-   | C.Meta _
+   | C.Rel m when m > n && m <= nn -> h
+   | C.Rel _ 
+   | C.Meta _ -> true
    | C.Sort _
    | C.Implicit _
    | C.Cast _
    | C.Prod _
-   | C.LetIn _ ->
-      (* the term has just been type-checked *)
-      raise (AssertFailure (lazy "17"))
+   | C.MutInd _ 
+   | C.LetIn _ -> raise (AssertFailure (lazy "17"))
    | C.Lambda (name,so,de) ->
       does_not_occur ~subst context n nn so &&
-       guarded_by_constructors ~subst ((Some (name,(C.Decl so)))::context)
-        (n + 1) (nn + 1) h de args coInductiveTypeURI
+      aux ((Some (name,(C.Decl so)))::context) (n + 1) (nn + 1) h de
    | C.Appl ((C.Rel m)::tl) when m > n && m <= nn ->
-      h &&
-       List.fold_right (fun x i -> i && does_not_occur ~subst context n nn x) tl true
-   | C.Appl ((C.MutConstruct (uri,i,j,exp_named_subst))::tl) ->
-      let consty =
-	let obj,_ = 
-	  try 
-	    CicEnvironment.get_cooked_obj ~trust:false CicUniv.empty_ugraph uri
-	  with Not_found -> assert false
-	in
-       match obj with
-          C.InductiveDefinition (itl,_,_,_) ->
-           let (_,_,_,cl) = List.nth itl i in
-            let (_,cons) = List.nth cl (j - 1) in
-             CicSubstitution.subst_vars exp_named_subst cons
-        | _ ->
-            raise (TypeCheckerFailure
-             (lazy ("Unknown mutual inductive definition:" ^ UriManager.string_of_uri uri)))
+      h && List.for_all (does_not_occur ~subst context n nn) tl
+   | C.MutConstruct (_,_,_,exp_named_subst) ->
+      List.for_all 
+        (fun (_,x) -> does_not_occur ~subst context n nn x) exp_named_subst
+   | C.Appl ((C.MutConstruct (uri,i,j,exp_named_subst))::tl) as t ->
+      List.for_all 
+        (fun (_,x) -> does_not_occur ~subst context n nn x) exp_named_subst &&
+      let consty, len_tys, tys_ctx, paramsno =
+       let tys, paramsno = 
+         specialize_inductive_type ~logger ~subst ~metasenv context t in
+       let _,_,_,cl = List.nth tys i in  
+       let _,ty = List.nth cl (j-1) in  
+         ty, List.length tys,
+         fst(List.fold_left
+          (fun (types,len) (n,_,ty,_) ->
+           Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types, len+1)
+          ([],0) tys), paramsno
       in
-       let rec analyse_branch context ty te =
-        match CicReduction.whd ~subst context ty with
-           C.Meta _ -> raise (AssertFailure (lazy "34"))
-         | C.Rel _
-         | C.Var _
-         | C.Sort _ ->
-            does_not_occur ~subst context n nn te
-         | C.Implicit _
-         | C.Cast _ ->
-            raise (AssertFailure (lazy "24"))(* due to type-checking *)
-         | C.Prod (name,so,de) ->
-            analyse_branch ((Some (name,(C.Decl so)))::context) de te
-         | C.Lambda _
-         | C.LetIn _ ->
-            raise (AssertFailure (lazy "25"))(* due to type-checking *)
-         | C.Appl ((C.MutInd (uri,_,_))::_) when uri == coInductiveTypeURI -> 
-             guarded_by_constructors ~subst context n nn true te []
-              coInductiveTypeURI
-         | C.Appl ((C.MutInd (uri,_,_))::_) -> 
-            guarded_by_constructors ~subst context n nn true te tl
-             coInductiveTypeURI
-         | C.Appl _ ->
-            does_not_occur ~subst context n nn te
-         | C.Const _ -> raise (AssertFailure (lazy "26"))
-         | C.MutInd (uri,_,_) when uri == coInductiveTypeURI ->
-            guarded_by_constructors ~subst context n nn true te []
-             coInductiveTypeURI
-         | C.MutInd _ ->
-            does_not_occur ~subst context n nn te
-         | C.MutConstruct _ -> raise (AssertFailure (lazy "27"))
-         (*CSC: we do not consider backbones with a MutCase, Fix, Cofix *)
-         (*CSC: in head position.                                       *)
-         | C.MutCase _
-         | C.Fix _
-         | C.CoFix _ ->
-            raise (AssertFailure (lazy "28"))(* due to type-checking *)
-       in
-       let rec analyse_instantiated_type context ty l =
-        match CicReduction.whd ~subst context ty with
-           C.Rel _
-         | C.Var _
-         | C.Meta _
-         | C.Sort _
-         | C.Implicit _
-         | C.Cast _ -> raise (AssertFailure (lazy "29"))(* due to type-checking *)
-         | C.Prod (name,so,de) ->
-            begin
-             match l with
-                [] -> true
-              | he::tl ->
-                 analyse_branch context so he &&
-                  analyse_instantiated_type
-                   ((Some (name,(C.Decl so)))::context) de tl
-            end
-         | C.Lambda _
-         | C.LetIn _ ->
-            raise (AssertFailure (lazy "30"))(* due to type-checking *)
-         | C.Appl _ -> 
-            List.fold_left
-             (fun i x -> i && does_not_occur ~subst context n nn x) true l
-         | C.Const _ -> raise (AssertFailure (lazy "31"))
-         | C.MutInd _ ->
-            List.fold_left
-             (fun i x -> i && does_not_occur ~subst context n nn x) true l
-         | C.MutConstruct _ -> raise (AssertFailure (lazy "32"))
-         (*CSC: we do not consider backbones with a MutCase, Fix, Cofix *)
-         (*CSC: in head position.                                       *)
-         | C.MutCase _
-         | C.Fix _
-         | C.CoFix _ ->
-            raise (AssertFailure (lazy "33"))(* due to type-checking *)
-       in
-        let rec instantiate_type args consty =
-         function
-            [] -> true
-          | tlhe::tltl as l ->
-             let consty' = CicReduction.whd ~subst context consty in
-              match args with 
-                 he::tl ->
-                  begin
-                   match consty' with
-                      C.Prod (_,_,de) ->
-                       let instantiated_de = CicSubstitution.subst he de in
-                        (*CSC: siamo sicuri che non sia troppo forte? *)
-                        does_not_occur ~subst context n nn tlhe &
-                         instantiate_type tl instantiated_de tltl
-                    | _ ->
-                      (*CSC:We do not consider backbones with a MutCase, a    *)
-                      (*CSC:FixPoint, a CoFixPoint and so on in head position.*)
-                      raise (AssertFailure (lazy "23"))
-                  end
-               | [] -> analyse_instantiated_type context consty' l
-                  (* These are all the other cases *)
+      let rec_params =
+       let c = 
+         debrujin_constructor ~check_exp_named_subst:false
+           indURI len_tys context consty 
        in
-        instantiate_type args consty tl
-   | C.Appl ((C.CoFix (_,fl))::tl) ->
-      List.fold_left (fun i x -> i && does_not_occur ~subst context n nn x) true tl &&
-       let len = List.length fl in
-        let n_plus_len = n + len
-        and nn_plus_len = nn + len
-        (*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *)
-        and tys,_ =
-          List.fold_left
-            (fun (types,len) (n,ty,_) ->
-               (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
-                len+1)
-	    ) ([],0) fl
-        in
-         List.fold_right
-          (fun (_,ty,bo) i ->
-            i && does_not_occur ~subst context n nn ty &&
-             guarded_by_constructors ~subst (tys@context) n_plus_len nn_plus_len
-              h bo args coInductiveTypeURI
-          ) fl true
-   | C.Appl ((C.MutCase (_,_,out,te,pl))::tl) ->
-       List.fold_left (fun i x -> i && does_not_occur ~subst context n nn x) true tl &&
-        does_not_occur ~subst context n nn out &&
-         does_not_occur ~subst context n nn te &&
-          List.fold_right
-           (fun x i ->
-             i &&
-             guarded_by_constructors ~subst context n nn h x args
-              coInductiveTypeURI
-           ) pl true
-   | C.Appl l ->
-      List.fold_right (fun x i -> i && does_not_occur ~subst context n nn x) l true
-   | C.Var (_,exp_named_subst)
-   | C.Const (_,exp_named_subst) ->
-      List.fold_right
-       (fun (_,x) i -> i && does_not_occur ~subst context n nn x) exp_named_subst true
-   | C.MutInd _ -> assert false
-   | C.MutConstruct (_,_,_,exp_named_subst) ->
-      List.fold_right
-       (fun (_,x) i -> i && does_not_occur ~subst context n nn x) exp_named_subst true
-   | C.MutCase (_,_,out,te,pl) ->
+       let len_ctx = List.length context in
+       recursive_args (context@tys_ctx) len_ctx (len_ctx+len_tys) c
+      in
+      let rec analyse_instantiated_type rec_spec args =
+       match rec_spec, args with
+       | h::rec_spec, he::args -> 
+           aux context n nn h he &&
+           analyse_instantiated_type rec_spec args 
+       | _,[] -> true
+       | _ -> raise (AssertFailure (lazy 
+         ("Too many args for constructor: " ^ String.concat " "
+         (List.map (fun x-> CicPp.ppterm x) args))))
+      in
+      let left, args = HExtlib.split_nth paramsno tl in
+      List.for_all (does_not_occur ~subst context n nn) left &&
+      analyse_instantiated_type rec_params args
+   | C.Appl ((C.MutCase (_,_,out,te,pl))::_) 
+   | C.MutCase (_,_,out,te,pl) as t ->
+       let tl = match t with C.Appl (_::tl) -> tl | _ -> [] in
+       List.for_all (does_not_occur ~subst context n nn) tl &&
        does_not_occur ~subst context n nn out &&
-        does_not_occur ~subst context n nn te &&
-         List.fold_right
-          (fun x i ->
-            i &&
-             guarded_by_constructors ~subst context n nn h x args
-              coInductiveTypeURI
-          ) pl true
-   | C.Fix (_,fl) ->
+       does_not_occur ~subst context n nn te &&
+       List.for_all (aux context n nn h ) pl
+   | C.Fix (_,fl)
+   | C.Appl (C.Fix (_,fl)::_) as t ->
+       let tl = match t with C.Appl (_::tl) -> tl | _ -> [] in
       let len = List.length fl in
        let n_plus_len = n + len
        and nn_plus_len = nn + len
-       (*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *)
        and tys,_ =
         List.fold_left
           (fun (types,len) (n,_,ty,_) ->
              (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
               len+1)
-	  ) ([],0) fl
+          ) ([],0) fl
        in
-        List.fold_right
-         (fun (_,_,ty,bo) i ->
-           i && does_not_occur ~subst context n nn ty &&
-            does_not_occur ~subst (tys@context) n_plus_len nn_plus_len bo
-         ) fl true
-   | C.CoFix (_,fl) ->
-      let len = List.length fl in
+        List.for_all (does_not_occur ~subst context n nn) tl &&
+        List.for_all
+         (fun (_,_,ty,bo) ->
+           does_not_occur ~subst context n nn ty &&
+           aux (tys@context) n_plus_len nn_plus_len h bo)
+         fl
+   | C.Appl ((C.CoFix (_,fl))::_) 
+   | C.CoFix (_,fl) as t ->
+       let tl = match t with C.Appl (_::tl) -> tl | _ -> [] in
+       let len = List.length fl in
        let n_plus_len = n + len
        and nn_plus_len = nn + len
-       (*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *)
        and tys,_ =
-        List.fold_left
-          (fun (types,len) (n,ty,_) ->
-             (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
-              len+1)
-	  ) ([],0) fl
+          List.fold_left
+            (fun (types,len) (n,ty,_) ->
+               (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
+                len+1)
+            ) ([],0) fl
        in
-        List.fold_right
-         (fun (_,ty,bo) i ->
-           i && does_not_occur ~subst context n nn ty &&
-            guarded_by_constructors ~subst (tys@context) n_plus_len nn_plus_len
-             h bo
-             args coInductiveTypeURI
-         ) fl true
+       List.for_all (does_not_occur ~subst context n nn) tl &&
+       List.for_all 
+         (fun (_,ty,bo) ->
+            does_not_occur ~subst context n nn ty &&
+            aux (tys@context) n_plus_len nn_plus_len h bo) 
+         fl
+   | C.Var _
+   | C.Const _
+   | C.Appl _ as t -> does_not_occur ~subst context n nn t
+ in
+   aux 
 
 and check_allowed_sort_elimination ~subst ~metasenv ~logger context uri i
   need_dummy ind arity1 arity2 ugraph =
@@ -1504,7 +1339,7 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph =
     | C.Var (uri,exp_named_subst) ->
       incr fdebug ;
 	let ugraph1 = 
-	  check_exp_named_subst ~logger ~subst context exp_named_subst ugraph 
+	  check_exp_named_subst uri ~logger ~subst context exp_named_subst ugraph 
 	in 
 	let ty,ugraph2 = type_of_variable ~logger uri ugraph1 in
 	let ty1 = CicSubstitution.subst_vars exp_named_subst ty in
@@ -1617,7 +1452,7 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph =
    | C.Const (uri,exp_named_subst) ->
        incr fdebug ;
        let ugraph1 = 
-	 check_exp_named_subst ~logger ~subst  context exp_named_subst ugraph 
+	 check_exp_named_subst uri ~logger ~subst  context exp_named_subst ugraph 
        in
        let cty,ugraph2 = type_of_constant ~logger uri ugraph1 in
        let cty1 =
@@ -1628,11 +1463,9 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph =
    | C.MutInd (uri,i,exp_named_subst) ->
       incr fdebug ;
        let ugraph1 = 
-	 check_exp_named_subst ~logger  ~subst context exp_named_subst ugraph 
+	 check_exp_named_subst uri ~logger  ~subst context exp_named_subst ugraph 
        in
-	 (* TASSI: da me c'era anche questa, ma in CVS no *)
        let mty,ugraph2 = type_of_mutual_inductive_defs ~logger uri i ugraph1 in
-	 (* fine parte dubbia *)
        let cty =
 	 CicSubstitution.subst_vars exp_named_subst mty
        in
@@ -1640,9 +1473,8 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph =
 	 cty,ugraph2
    | C.MutConstruct (uri,i,j,exp_named_subst) ->
        let ugraph1 = 
-	 check_exp_named_subst ~logger ~subst context exp_named_subst ugraph 
+	 check_exp_named_subst uri ~logger ~subst context exp_named_subst ugraph
        in
-	 (* TASSI: idem come sopra *)
        let mty,ugraph2 = 
 	 type_of_mutual_inductive_constr ~logger uri i j ugraph1 
        in
@@ -1861,12 +1693,33 @@ end;
 		   let (m, eaten, context') =
 		     eat_lambdas ~subst (types @ context) (x + 1) bo
 		   in
+                   let rec_uri, rec_uri_len =
+                    let he =
+                     match List.hd context' with
+                        Some (_,Cic.Decl he) -> he
+                      | _ -> assert false
+                    in
+                     match CicReduction.whd ~subst (List.tl context') he with
+                     | Cic.MutInd (uri,_,_)
+                     | Cic.Appl (Cic.MutInd (uri,_,_)::_) ->
+                         uri,
+                           (match
+                            CicEnvironment.get_obj
+                             CicUniv.oblivion_ugraph uri
+                           with
+                           | Cic.InductiveDefinition (tl,_,_,_), _ ->
+                               List.length tl
+                           | _ -> assert false)
+                     | _ -> assert false
+                   in 
 		     (*
 		       let's control the guarded by 
 		       destructors conditions D{f,k,x,M}
 		     *)
-		     if not (guarded_by_destructors ~subst context' eaten 
-			       (len + eaten) kl 1 [] m) then
+		     if not (guarded_by_destructors ~logger ~metasenv ~subst 
+                       rec_uri rec_uri_len context' eaten (len + eaten) kl 
+                       1 [] m) 
+                     then
 		       raise
 			 (TypeCheckerFailure 
 			   (lazy ("Fix: not guarded by destructors:"^CicPp.ppterm t)))
@@ -1912,8 +1765,8 @@ end;
 			    let's control the guarded by constructors 
 			    conditions C{f,M}
 			  *)
-			  if not (guarded_by_constructors ~subst
-                              (types @ context) 0 len false bo [] uri) then
+			  if not (guarded_by_constructors ~logger ~subst ~metasenv uri
+                 (types @ context) 0 len false bo) then
 			    raise
 			      (TypeCheckerFailure 
 				(lazy "CoFix: not guarded by constructors"))
@@ -1928,7 +1781,24 @@ end;
        let (_,ty,_) = List.nth fl i in
 	 ty,ugraph2
 
- and check_exp_named_subst ~logger ~subst context =
+ and check_exp_named_subst uri ~logger ~subst context ens ugraph =
+   let params =
+    let obj,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+    (match obj with
+        Cic.Constant (_,_,_,params,_) -> params
+      | Cic.Variable (_,_,_,params,_) -> params
+      | Cic.CurrentProof (_,_,_,_,params,_) -> params
+      | Cic.InductiveDefinition (_,params,_,_) -> params
+    ) in
+   let rec check_same_order params ens =
+    match params,ens with
+     | _,[] -> ()
+     | [],_::_ ->
+        raise (TypeCheckerFailure (lazy "Bad explicit named substitution"))
+     | uri::tl,(uri',_)::tl' when UriManager.eq uri uri' ->
+        check_same_order tl tl'
+     | _::tl,l -> check_same_order tl l
+   in
    let rec check_exp_named_subst_aux ~logger esubsts l ugraph =
      match l with
 	 [] -> ugraph
@@ -1954,7 +1824,8 @@ end;
 		 raise (TypeCheckerFailure (lazy "Wrong Explicit Named Substitution"))
                end
    in
-     check_exp_named_subst_aux ~logger []
+    check_same_order params ens ;
+    check_exp_named_subst_aux ~logger [] ens ugraph
        
  and sort_of_prod ~subst context (name,s) (t1, t2) ugraph =
   let module C = Cic in
@@ -2109,103 +1980,92 @@ in debug_print (lazy "FINE TYPE_OF_AUX'") ; flush stderr ; res
 *)
 ;;
 
-let typecheck_obj0 ~logger uri ugraph =
+let typecheck_obj0 ~logger uri (obj,unchecked_ugraph) =
  let module C = Cic in
-  function
-     C.Constant (_,Some te,ty,_,_) ->
-      let _,ugraph = type_of ~logger ty ugraph in
-      let ty_te,ugraph = type_of ~logger te ugraph in
-      let b,ugraph = (CicReduction.are_convertible [] ty_te ty ugraph) in
-       if not b then
-         raise (TypeCheckerFailure
-          (lazy
-            ("the type of the body is not the one expected:\n" ^
-             CicPp.ppterm ty_te ^ "\nvs\n" ^
-             CicPp.ppterm ty)))
-       else
-        ugraph
-   | C.Constant (_,None,ty,_,_) ->
-      (* only to check that ty is well-typed *)
-      let _,ugraph = type_of ~logger ty ugraph in
-       ugraph
-   | C.CurrentProof (_,conjs,te,ty,_,_) ->
-      (* this block is broken since the metasenv should 
-       * be topologically sorted before typing metas *)
-      ignore(assert false);
-      let _,ugraph =
-       List.fold_left
-        (fun (metasenv,ugraph) ((_,context,ty) as conj) ->
-          let _,ugraph = 
-           type_of_aux' ~logger metasenv context ty ugraph 
-          in
-           metasenv @ [conj],ugraph
-        ) ([],ugraph) conjs
-      in
-       let _,ugraph = type_of_aux' ~logger conjs [] ty ugraph in
-       let type_of_te,ugraph = 
-        type_of_aux' ~logger conjs [] te ugraph
-       in
-       let b,ugraph = CicReduction.are_convertible [] type_of_te ty ugraph in
-        if not b then
-          raise (TypeCheckerFailure (lazy (sprintf
-           "the current proof is not well typed because the type %s of the body is not convertible to the declared type %s"
-           (CicPp.ppterm type_of_te) (CicPp.ppterm ty))))
-        else
+ let ugraph = CicUniv.empty_ugraph in
+ let inferred_ugraph =
+   match obj with
+    | C.Constant (_,Some te,ty,_,_) ->
+        let _,ugraph = type_of ~logger ty ugraph in
+        let ty_te,ugraph = type_of ~logger te ugraph in
+        let b,ugraph = (CicReduction.are_convertible [] ty_te ty ugraph) in
+         if not b then
+           raise (TypeCheckerFailure
+            (lazy
+              ("the type of the body is not the one expected:\n" ^
+               CicPp.ppterm ty_te ^ "\nvs\n" ^
+               CicPp.ppterm ty)))
+         else
+          ugraph
+     | C.Constant (_,None,ty,_,_) ->
+        (* only to check that ty is well-typed *)
+        let _,ugraph = type_of ~logger ty ugraph in
          ugraph
-   | C.Variable (_,bo,ty,_,_) ->
-      (* only to check that ty is well-typed *)
-      let _,ugraph = type_of ~logger ty ugraph in
-       (match bo with
-           None -> ugraph
-         | Some bo ->
-            let ty_bo,ugraph = type_of ~logger bo ugraph in
-  	    let b,ugraph = CicReduction.are_convertible [] ty_bo ty ugraph in
-             if not b then
-              raise (TypeCheckerFailure
-               (lazy "the body is not the one expected"))
-             else
-              ugraph
-            )
-   | (C.InductiveDefinition _ as obj) ->
-      check_mutual_inductive_defs ~logger uri obj ugraph
+     | C.CurrentProof (_,conjs,te,ty,_,_) ->
+        (* this block is broken since the metasenv should 
+         * be topologically sorted before typing metas *)
+        ignore(assert false);
+        let _,ugraph =
+         List.fold_left
+          (fun (metasenv,ugraph) ((_,context,ty) as conj) ->
+            let _,ugraph = 
+             type_of_aux' ~logger metasenv context ty ugraph 
+            in
+             metasenv @ [conj],ugraph
+          ) ([],ugraph) conjs
+        in
+         let _,ugraph = type_of_aux' ~logger conjs [] ty ugraph in
+         let type_of_te,ugraph = 
+          type_of_aux' ~logger conjs [] te ugraph
+         in
+         let b,ugraph = CicReduction.are_convertible [] type_of_te ty ugraph in
+          if not b then
+            raise (TypeCheckerFailure (lazy (sprintf
+             "the current proof is not well typed because the type %s of the body is not convertible to the declared type %s"
+             (CicPp.ppterm type_of_te) (CicPp.ppterm ty))))
+          else
+           ugraph
+     | C.Variable (_,bo,ty,_,_) ->
+        (* only to check that ty is well-typed *)
+        let _,ugraph = type_of ~logger ty ugraph in
+         (match bo with
+             None -> ugraph
+           | Some bo ->
+              let ty_bo,ugraph = type_of ~logger bo ugraph in
+    	    let b,ugraph = CicReduction.are_convertible [] ty_bo ty ugraph in
+               if not b then
+                raise (TypeCheckerFailure
+                 (lazy "the body is not the one expected"))
+               else
+                ugraph
+              )
+     | (C.InductiveDefinition _ as obj) ->
+        check_mutual_inductive_defs ~logger uri obj ugraph
+ in
+   check_and_clean_ugraph inferred_ugraph unchecked_ugraph uri obj
+;;
 
 let typecheck uri =
  let module C = Cic in
  let module R = CicReduction in
  let module U = UriManager in
  let logger = new CicLogger.logger in
-   (* ??? match CicEnvironment.is_type_checked ~trust:true uri with ???? *)
    match CicEnvironment.is_type_checked ~trust:false CicUniv.empty_ugraph uri with
-     CicEnvironment.CheckedObj (cobj,ugraph') -> 
-       (* debug_print (lazy ("NON-INIZIO A TYPECHECKARE " ^ U.string_of_uri uri));*)
-       cobj,ugraph'
-   | CicEnvironment.UncheckedObj uobj ->
+   | CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph'
+   | CicEnvironment.UncheckedObj (uobj,unchecked_ugraph) ->
       (* let's typecheck the uncooked object *)
       logger#log (`Start_type_checking uri) ;
-      (* debug_print (lazy ("INIZIO A TYPECHECKARE " ^ U.string_of_uri uri)); *)
-      let ugraph = typecheck_obj0 ~logger uri CicUniv.empty_ugraph uobj in
-	try
-	  CicEnvironment.set_type_checking_info uri;
-	  logger#log (`Type_checking_completed uri);
-	  match CicEnvironment.is_type_checked ~trust:false ugraph uri with
-	      CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph'
-	    | _ -> raise CicEnvironmentError
-	with
-	    (*
-	      this is raised if set_type_checking_info is called on an object
-	      that has no associated universe file. If we are in univ_maker 
-	      phase this is OK since univ_maker will properly commit the 
-	      object.
-	    *)
-	    Invalid_argument s -> 
-	      (*debug_print (lazy s);*)
-	      uobj,ugraph
+      let ugraph, ul, obj = typecheck_obj0 ~logger uri (uobj,unchecked_ugraph) in
+      CicEnvironment.set_type_checking_info uri (obj,ugraph,ul);
+      logger#log (`Type_checking_completed uri);
+      match CicEnvironment.is_type_checked ~trust:false CicUniv.empty_ugraph uri with
+      | CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph'
+      | _ -> raise CicEnvironmentError
 ;;
 
 let typecheck_obj ~logger uri obj =
- let ugraph = typecheck_obj0 ~logger uri CicUniv.empty_ugraph obj in
- let ugraph, univlist, obj = CicUnivUtils.clean_and_fill uri obj ugraph in
-  CicEnvironment.add_type_checked_obj uri (obj,ugraph,univlist)
+ let ugraph,univlist,obj = typecheck_obj0 ~logger uri (obj,None) in
+ CicEnvironment.add_type_checked_obj uri (obj,ugraph,univlist)
 
 (** wrappers which instantiate fresh loggers *)
 
@@ -2243,10 +2103,10 @@ Deannotate.type_of_aux' :=
       (match el with
           None -> ()
         | Some (_,Cic.Decl ty) ->
-           ignore (type_of_aux' [] context ty CicUniv.oblivion_ugraph)
+           ignore (type_of_aux' [] context ty CicUniv.empty_ugraph)
         | Some (_,Cic.Def (bo,ty)) ->
-           ignore (type_of_aux' [] context ty CicUniv.oblivion_ugraph);
-           ignore (type_of_aux' [] context bo CicUniv.oblivion_ugraph));
+           ignore (type_of_aux' [] context ty CicUniv.empty_ugraph);
+           ignore (type_of_aux' [] context bo CicUniv.empty_ugraph));
       el::context
    ) context []);
-  fst (type_of_aux' [] context t CicUniv.oblivion_ugraph);;
+  fst (type_of_aux' [] context t CicUniv.empty_ugraph);;