X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fcic%2FcicUniv.mli;h=7a4331905b50ea95689302c90135011e5649ec5d;hb=24dd4569daf1d35bffaa813b8164058d8643f14d;hp=288efe616885b833ceedb5984af376fda2f8b2ae;hpb=b7387d913f7dddf52d1e73173bca3fc8729723ba;p=helm.git

diff --git a/components/cic/cicUniv.mli b/components/cic/cicUniv.mli
index 288efe616..7a4331905 100644
--- a/components/cic/cicUniv.mli
+++ b/components/cic/cicUniv.mli
@@ -57,6 +57,9 @@ val name_universe: universe -> UriManager.uri -> universe
 *)
 val empty_ugraph: universe_graph
 
+(* an universe that does nothing: i.e. no constraints are kept, no merges.. *)
+val oblivion_ugraph: universe_graph
+
 (*
   These are the real functions to add eq/ge/gt constraints 
   to the passed graph, returning an updated graph or raising