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

diff --git a/helm/software/components/cic_proof_checking/cicTypeChecker.ml b/helm/software/components/cic_proof_checking/cicTypeChecker.ml
index 883bc3296..6cbb44f80 100644
--- a/helm/software/components/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/software/components/cic_proof_checking/cicTypeChecker.ml
@@ -54,6 +54,21 @@ let rec split l n =
       raise (TypeCheckerFailure (lazy "Parameters number < left parameters number"))
 ;;
 
+(* 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
@@ -126,74 +141,63 @@ let debrujin_constructor ?(cb=fun _ _ -> ()) ?(check_exp_named_subst=true) uri n
 
 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,_,_,_) ->
@@ -711,7 +718,8 @@ and split_prods ~subst context n te =
  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"))
 
@@ -749,7 +757,7 @@ and specialize_inductive_type ~logger ~subst ~metasenv context t =
                cl 
             in
             name, isind, arity, cl)
-          tl
+          tl, paramsno
       | _ -> assert false)
   | _ -> assert false
 
@@ -763,10 +771,12 @@ and check_is_really_smaller_arg
  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 rec_uri rec_uri_len 
         ~logger ~metasenv ~subst (Some (name,Cic.Decl ty)::context)
@@ -774,11 +784,15 @@ and check_is_really_smaller_arg
    | 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 tys = 
+         let tys,_ = 
            specialize_inductive_type ~logger ~subst ~metasenv context term 
          in
-         let tys_ctx = 
-           List.map (fun (name,_,ty,_) -> Some (Cic.Name name, Cic.Decl ty)) tys
+         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
@@ -835,7 +849,9 @@ and guarded_by_destructors
 =
  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
@@ -888,12 +904,15 @@ and guarded_by_destructors
            List.for_all
              (guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst context n nn kl x safes)
              tl &&
-           let tys = 
+           let tys,_ = 
              specialize_inductive_type ~logger ~subst ~metasenv context t
            in
-           let tys_ctx = 
-             List.map 
-               (fun (name,_,ty,_) -> Some (Cic.Name name, Cic.Decl ty)) tys
+           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
@@ -989,228 +1008,124 @@ and guarded_by_destructors
       List.fold_right
        (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 *)
+      let rec_params =
+       let c = 
+         debrujin_constructor ~check_exp_named_subst:false
+           indURI len_tys context consty 
        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 *)
-       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 =
@@ -1424,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
@@ -1537,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 =
@@ -1548,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
@@ -1560,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
@@ -1853,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"))
@@ -1869,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
@@ -1895,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
@@ -2050,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 *)
 
@@ -2184,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);;