new snapshot

[helm.git] / components / cic / cicUniv.mli

diff --git a/components/cic/cicUniv.mli b/components/cic/cicUniv.mli
index eb3c50866f73482a578f0f8376bd376c8e124236..7a4331905b50ea95689302c90135011e5649ec5d 100644 (file)
--- a/components/cic/cicUniv.mli
+++ b/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