X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_exportation%2FcicExportation.ml;h=cd5ab3ace32f14593d9b85f29a3f52ff34955173;hb=2e2648a9ed26d9b813de8e6a10e2776162565f09;hp=69c949c6325044044414012e62094805ffd7fa96;hpb=5cd2efd21063b304c30a9486a562bdff7852957b;p=helm.git

diff --git a/helm/software/components/cic_exportation/cicExportation.ml b/helm/software/components/cic_exportation/cicExportation.ml
index 69c949c63..cd5ab3ace 100644
--- a/helm/software/components/cic_exportation/cicExportation.ml
+++ b/helm/software/components/cic_exportation/cicExportation.ml
@@ -223,7 +223,7 @@ let rec pp ~in_type t context =
         (if stl = "" then "" else "(" ^ stl ^ ") ") ^ hes
     | C.Appl (C.MutConstruct (uri,n,_,_) as he::tl) ->
        let nparams =
-        match fst(CicEnvironment.get_obj CicUniv.empty_ugraph uri) with
+        match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph uri) with
            C.InductiveDefinition (_,_,nparams,_) -> nparams
          | _ -> assert false in
        let hes = pp ~in_type he context in
@@ -236,7 +236,7 @@ let rec pp ~in_type t context =
         pp_exp_named_subst exp_named_subst context
     | C.MutInd (uri,n,exp_named_subst) ->
        (try
-         match fst(CicEnvironment.get_obj CicUniv.empty_ugraph uri) with
+         match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph uri) with
             C.InductiveDefinition (dl,_,_,_) ->
              let (name,_,_,_) = get_nth dl (n+1) in
               qualified_name_of_uri current_module_uri
@@ -250,7 +250,7 @@ let rec pp ~in_type t context =
        )
     | C.MutConstruct (uri,n1,n2,exp_named_subst) ->
        (try
-         match fst(CicEnvironment.get_obj CicUniv.empty_ugraph uri) with
+         match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph uri) with
             C.InductiveDefinition (dl,_,_,_) ->
              let _,_,_,cons = get_nth dl (n1+1) in
               let id,_ = get_nth cons n2 in
@@ -289,7 +289,7 @@ let rec pp ~in_type t context =
             if patterns = [] then "assert false"
             else
              (let connames_and_argsno, go_up, go_pu, go_down, go_nwod =
-               (match fst(CicEnvironment.get_obj CicUniv.empty_ugraph uri) with
+               (match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph uri) with
                    C.InductiveDefinition (dl,_,paramsno,_) ->
                     let (_,_,_,cons) = get_nth dl (n1+1) in
                     let rc =