]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/cic/cicUniv.mli
added oblivion_universe and used it in paxck_coercions
[helm.git] / helm / software / components / cic / cicUniv.mli
index 288efe616885b833ceedb5984af376fda2f8b2ae..7a4331905b50ea95689302c90135011e5649ec5d 100644 (file)
@@ -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