X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic%2FcicUniv.mli;h=7a4331905b50ea95689302c90135011e5649ec5d;hb=63adafe5fb700c8ecf13f74fc31086c173617e86;hp=eb3c50866f73482a578f0f8376bd376c8e124236;hpb=55b82bd235d82ff7f0a40d980effe1efde1f5073;p=helm.git

diff --git a/helm/software/components/cic/cicUniv.mli b/helm/software/components/cic/cicUniv.mli
index eb3c50866..7a4331905 100644
--- a/helm/software/components/cic/cicUniv.mli
+++ b/helm/software/components/cic/cicUniv.mli
@@ -27,7 +27,7 @@
 (*
   The strings contains an unreadable message
 *)
-exception UniverseInconsistency of string
+exception UniverseInconsistency of string Lazy.t
 
 (*
   Cic.Type of universe 
@@ -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
@@ -136,7 +139,7 @@ val recons_graph: universe_graph -> universe_graph
   (** re-hash-cons a single universe *)
 val recons_univ: universe -> universe
 
-  (** consistency chek that should be done before committin the graph to the
+  (** consistency check that should be done before committin the graph to the
    * cache *)
 val assert_univs_have_uri: universe_graph -> universe list-> unit