X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicUnivUtils.ml;h=c027194543abc4cc0d4bc5aa4aa448eb7d996bf4;hb=8c578ae2acfb32b39610aebbd4baab3a31775a9f;hp=1897772a8e869b16a8af8955e24ecd277abda242;hpb=58bd1746df1d9dc734f8ac75220d25997c09bed1;p=helm.git

diff --git a/helm/ocaml/cic_proof_checking/cicUnivUtils.ml b/helm/ocaml/cic_proof_checking/cicUnivUtils.ml
index 1897772a8..c02719454 100644
--- a/helm/ocaml/cic_proof_checking/cicUnivUtils.ml
+++ b/helm/ocaml/cic_proof_checking/cicUnivUtils.ml
@@ -45,16 +45,14 @@ let universes_of_obj uri t =
     | C.Var (u,exp_named_subst) ->
         if List.mem u !don then [] else
         (don := u::!don;
-         aux_obj (CicEnvironment.get_obj ~not_jet_cooked:true u 
-		    CicUniv.empty_ugraph))
+         aux_obj (CicEnvironment.get_obj CicUniv.empty_ugraph u))
     | C.MutInd (u,_,exp_named_subst) ->
 	if List.mem u !don || eq u uri then 
 	  [] 
 	else
           begin
 	    don := u::!don;
-            (match fst(CicEnvironment.get_obj ~not_jet_cooked:true u  
-                         CicUniv.empty_ugraph)
+            (match fst(CicEnvironment.get_obj CicUniv.empty_ugraph u)
               with
                | C.InductiveDefinition (l,_,_) -> 
 		   List.fold_left (
@@ -73,8 +71,7 @@ let universes_of_obj uri t =
 	else
 	  begin
 	    don := u::!don;
-	    (match fst(CicEnvironment.get_obj ~not_jet_cooked:true u 
-			 CicUniv.empty_ugraph) with
+	    (match fst(CicEnvironment.get_obj CicUniv.empty_ugraph u) with
 	       | C.InductiveDefinition (l,_,_) -> 
 		   List.fold_left (
 		     fun x (_,_,_t,l') ->
@@ -120,36 +117,31 @@ let universes_of_obj uri t =
            List.fold_left (
              fun l u ->
                l @ if eq u uri then [] else 
-                 (aux_obj (CicEnvironment.get_obj ~not_jet_cooked:true u
-                              CicUniv.empty_ugraph)))
+                 (aux_obj (CicEnvironment.get_obj CicUniv.empty_ugraph u)))
 	   [] v
        | C.Constant (_,None,ty,v) -> aux ty @
            List.fold_left (
              fun l u ->
                l @ if eq u uri then [] else 
-                 (aux_obj (CicEnvironment.get_obj ~not_jet_cooked:true u
-                              CicUniv.empty_ugraph)))
+                 (aux_obj (CicEnvironment.get_obj CicUniv.empty_ugraph u)))
 	     [] v
        | C.CurrentProof (_,conjs,te,ty,v) -> aux te @ aux ty @
            List.fold_left (
              fun l u ->
                l @ if eq u uri then [] else 
-                 (aux_obj (CicEnvironment.get_obj ~not_jet_cooked:true u
-                              CicUniv.empty_ugraph)))
+                 (aux_obj (CicEnvironment.get_obj CicUniv.empty_ugraph u)))
 	     [] v
        | C.Variable (_,Some bo,ty,v) -> aux bo @ aux ty @
            List.fold_left (
              fun l u ->
                l @ if eq u uri then [] else 
-                 (aux_obj (CicEnvironment.get_obj ~not_jet_cooked:true u
-                              CicUniv.empty_ugraph)))
+                 (aux_obj (CicEnvironment.get_obj CicUniv.empty_ugraph u)))
 	     [] v
        | C.Variable (_,None ,ty,v) -> aux ty @ 
            List.fold_left (
              fun l u ->
                l @ if eq u uri then [] else 
-                 (aux_obj (CicEnvironment.get_obj ~not_jet_cooked:true u
-                              CicUniv.empty_ugraph)))
+                 (aux_obj (CicEnvironment.get_obj CicUniv.empty_ugraph u)))
 	     [] v
        | C.InductiveDefinition (l,v,_) -> 
 	   (List.fold_left (
@@ -161,8 +153,7 @@ let universes_of_obj uri t =
 	   (List.fold_left
               (fun l u -> 
 	       l @ if eq u uri then [] else 
-                 (aux_obj (CicEnvironment.get_obj ~not_jet_cooked:true u
-			      CicUniv.empty_ugraph)))
+                 (aux_obj (CicEnvironment.get_obj CicUniv.empty_ugraph u)))
 	      [] v)
     )
   in