positivity check fixed, a MutInd not applied (but with an exp-named-subst)

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

diff --git a/helm/software/components/cic/cicUniv.mli b/helm/software/components/cic/cicUniv.mli
index eb3c50866f73482a578f0f8376bd376c8e124236..fd501df8c47c4adfa320d90151ebc07b47c89e74 100644 (file)
--- 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
@@ -69,6 +72,9 @@ val add_ge:
 val add_gt: 
   ?fast:bool -> universe -> universe -> universe_graph -> universe_graph
 
+val do_rank: universe_graph -> unit
+val get_rank: universe -> int
+
 (*
   debug function to print the graph to standard error
 *)
@@ -136,7 +142,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
 
@@ -152,3 +158,4 @@ val eq: universe -> universe -> bool
 val get_spent_time: unit -> float
 val reset_spent_time: unit -> unit
 
+val is_anon: universe -> bool