X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Facic_procedural%2Facic2Procedural.ml;h=e71f443d9cefa3c79fb87a2294099270cab019ed;hb=b82f2275e30c7ae035c719cb001771de9d0baa32;hp=c004fd346b4e2a9ff30714fa3cf84af50a5acf00;hpb=6ba374cbb94797e58cd997c5b41099dd9f679a57;p=helm.git

diff --git a/helm/software/components/acic_procedural/acic2Procedural.ml b/helm/software/components/acic_procedural/acic2Procedural.ml
index c004fd346..e71f443d9 100644
--- a/helm/software/components/acic_procedural/acic2Procedural.ml
+++ b/helm/software/components/acic_procedural/acic2Procedural.ml
@@ -153,7 +153,7 @@ with Invalid_argument _ -> failwith "A2P.get_sort"
 *)
 let get_type msg st bo =
 try   
-   let ty, _ = TC.type_of_aux' [] st.context (H.cic bo) Un.empty_ugraph in
+   let ty, _ = TC.type_of_aux' [] st.context (H.cic bo) Un.oblivion_ugraph in
    ty
 with e -> failwith (msg ^ ": " ^ Printexc.to_string e)
 
@@ -167,7 +167,7 @@ let get_entry st id =
 
 let get_ind_names uri tno =
 try   
-   let ts = match E.get_obj Un.empty_ugraph uri with
+   let ts = match E.get_obj Un.oblivion_ugraph uri with
       | C.InductiveDefinition (ts, _, _, _), _ -> ts 
       | _                                      -> assert false
    in