X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2FeliminationTactics.ml;h=5a293bcafcd4683661b077eee638a24d7992e971;hb=b3e08a6954c8b6946f42f5c7e0bed7912d5ac87c;hp=29961db389d1c3a039b23286b4eb643f075a0146;hpb=c6cc2a7227d6750076f591a62d7b1896ebf1ebfa;p=helm.git

diff --git a/helm/software/components/tactics/eliminationTactics.ml b/helm/software/components/tactics/eliminationTactics.ml
index 29961db38..5a293bcaf 100644
--- a/helm/software/components/tactics/eliminationTactics.ml
+++ b/helm/software/components/tactics/eliminationTactics.ml
@@ -43,7 +43,7 @@ module PEH  = ProofEngineHelpers
 let premise_pattern what = None, [what, C.Implicit (Some `Hole)], None 
 
 let get_inductive_def uri =
-   match E.get_obj Un.empty_ugraph uri with
+   match E.get_obj Un.oblivion_ugraph uri with
       | C.InductiveDefinition (tys, _, lpsno, _), _ -> 
          lpsno, tys
       | _                                           -> assert false
@@ -70,7 +70,7 @@ let rec check_type sorts metasenv context t =
          let _, psno = PEH.split_with_whd ([], arity) in
          let not_relation = (lpsno = psno) in
          let not_recursive = is_not_recursive uri tyno tys in
-         let ty_ty, _ = TC.type_of_aux' metasenv context t Un.empty_ugraph in
+         let ty_ty, _ = TC.type_of_aux' metasenv context t Un.oblivion_ugraph in
          let sort = match PEH.split_with_whd (context, ty_ty) with
             | (_, C.Sort sort) ::_ , _ -> CicPp.ppsort sort
 	    | (_, C.Meta _) :: _, _    -> CicPp.ppsort (C.Type (Un.fresh ()))
@@ -155,7 +155,7 @@ let warn s = debug_print (lazy ("DECOMPOSE: " ^ (Lazy.force s)))
 
 (* roba seria ------------------------------------------------------------- *)
 
-let decompose_tac ?(sorts=[CicPp.ppsort C.Prop; CicPp.ppsort C.CProp]) 
+let decompose_tac ?(sorts=[CicPp.ppsort C.Prop; CicPp.ppsort (C.CProp (CicUniv.fresh ()))]) 
                   ?(mk_fresh_name_callback = F.mk_fresh_name ~subst:[]) () =
    let decompose_tac status =
       let (proof, goal) = status in