X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic%2FcicUniv.mli;h=8a24614c2a814482838d09be95c148ebd179d52a;hb=2e58d03db0222ac0d885abeaebceac07ac586761;hp=fa7f544c06036deebda609dfecba3446b5af760e;hpb=25bc159057b95f144495872b55115a1762561d69;p=helm.git diff --git a/helm/software/components/cic/cicUniv.mli b/helm/software/components/cic/cicUniv.mli index fa7f544c0..8a24614c2 100644 --- a/helm/software/components/cic/cicUniv.mli +++ b/helm/software/components/cic/cicUniv.mli @@ -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