]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/cic/cicUniv.mli
parameter sintax added to axiom statement
[helm.git] / helm / software / components / cic / cicUniv.mli
index fa7f544c06036deebda609dfecba3446b5af760e..8a24614c2a814482838d09be95c148ebd179d52a 100644 (file)
@@ -60,6 +60,10 @@ val empty_ugraph: universe_graph
 (* an universe that does nothing: i.e. no constraints are kept, no merges.. *)
 val oblivion_ugraph: universe_graph
 
+(* one of the previous two, no set to empty_ugraph *)
+val default_ugraph: universe_graph
+
+
 (*
   These are the real functions to add eq/ge/gt constraints 
   to the passed graph, returning an updated graph or raising