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 288efe616885b833ceedb5984af376fda2f8b2ae..fd501df8c47c4adfa320d90151ebc07b47c89e74 100644 (file)
--- a/helm/software/components/cic/cicUniv.mli
+++ b/helm/software/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
@@ -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
 *)
@@ -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