oblivion ugraph everywhere outside the kernel

[helm.git] / helm / software / components / cic_exportation / cicExportation.ml

diff --git a/helm/software/components/cic_exportation/cicExportation.ml b/helm/software/components/cic_exportation/cicExportation.ml
index 69c949c6325044044414012e62094805ffd7fa96..cd5ab3ace32f14593d9b85f29a3f52ff34955173 100644 (file)
--- 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 =