X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Facic_procedural%2FproceduralHelpers.ml;h=4d86521074122e31e6907a28c25887355809dd99;hb=f3ad825f16c02c0c5fca620980882e409871e6f1;hp=31c7f4e8d5058a4e16e8cc40b3b16c4800f3de9a;hpb=cc23f034c9419186602d9250456241f2eba90d7c;p=helm.git

diff --git a/helm/software/components/acic_procedural/proceduralHelpers.ml b/helm/software/components/acic_procedural/proceduralHelpers.ml
index 31c7f4e8d..4d8652107 100644
--- a/helm/software/components/acic_procedural/proceduralHelpers.ml
+++ b/helm/software/components/acic_procedural/proceduralHelpers.ml
@@ -81,7 +81,7 @@ let compose f g x = f (g x)
 let fst3 (x, _, _) = x
 
 let refine c t =
-   try let t, _, _, _ = Rf.type_of_aux' [] c t Un.empty_ugraph in t
+   try let t, _, _, _ = Rf.type_of_aux' [] c t Un.oblivion_ugraph in t
    with e -> 
       Printf.eprintf "REFINE EROR: %s\n" (Printexc.to_string e);
       Printf.eprintf "Ref: context: %s\n" (Pp.ppcontext c);
@@ -89,7 +89,7 @@ let refine c t =
       raise e
 
 let get_type c t =
-   try let ty, _ = TC.type_of_aux' [] c t Un.empty_ugraph in ty
+   try let ty, _ = TC.type_of_aux' [] c t Un.oblivion_ugraph in ty
    with e -> 
       Printf.eprintf "TC: context: %s\n" (Pp.ppcontext c);
       Printf.eprintf "TC: term   : %s\n" (Pp.ppterm t);
@@ -124,7 +124,7 @@ let is_not_atomic = function
 let is_atomic t = not (is_not_atomic t)
 
 let get_ind_type uri tyno =
-   match E.get_obj Un.empty_ugraph uri with
+   match E.get_obj Un.oblivion_ugraph uri with
       | C.InductiveDefinition (tys, _, lpsno, _), _ -> lpsno, List.nth tys tyno
       | _                                           -> assert false
 
@@ -133,7 +133,7 @@ let get_default_eliminator context uri tyno ty =
    let ext = match get_tail context (get_type context ty) with
       | C.Sort C.Prop     -> "_ind"
       | C.Sort C.Set      -> "_rec"
-      | C.Sort C.CProp    -> "_rec"
+      | C.Sort (C.CProp _)   -> "_rect"
       | C.Sort (C.Type _) -> "_rect"
       | t                 -> 
          Printf.eprintf "CicPPP get_default_eliminator: %s\n" (Pp.ppterm t);