diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-10-26 13:33:49 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-10-26 13:33:49 +0000 |
| commit | cf21be5bfd42720bd1cc8756cfcdb388cdaebd80 (patch) | |
| tree | fc2396883396496d349445981f5a18f1c7d9fec3 /kernel/univ.mli | |
| parent | 9f2d6ca25f784bd877c65e4fe20d5a3f6aee784d (diff) | |
When checking for emptiness, use Foo.is_empty instead of (=) Foo.empty
Here Foo is Univ.constraints, Univ.universes, Evd.evar_map, Evd.Metamap
Ok, all these structures are currently ocaml's maps or similar,
with a unique empty value, and (=) can be used on them in this
particular case. But using Foo.is_empty is safer : it will work
even if the underlying representation changes. Example : for
spotting non-legitimate use of (=) we might embed a type into
a record with a functional field.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14614 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/univ.mli')
| -rw-r--r-- | kernel/univ.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/kernel/univ.mli b/kernel/univ.mli index a55775372..8b3f62910 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -47,6 +47,7 @@ val check_eq : check_function (** The empty graph of universes *) val initial_universes : universes +val is_initial_universes : universes -> bool (** {6 Constraints. } *) @@ -55,6 +56,8 @@ type constraints val empty_constraint : constraints val union_constraints : constraints -> constraints -> constraints +val is_empty_constraint : constraints -> bool + type constraint_function = universe -> universe -> constraints -> constraints val enforce_geq : constraint_function |