diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-12-18 16:35:15 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-12-18 16:35:15 +0000 |
| commit | 2a451f1809389beb123985d746f2e8febd46832e (patch) | |
| tree | 0bedd2eb88e2ec865070b4757546a4ec4a7fbf6b /kernel/univ.mli | |
| parent | 1c98af511e3cdc84c97bfc615a4c012059539d4f (diff) | |
Univ.constraints made fully abstract instead of being a Set of abstract stuff
No need to tell the world about the fact that constraints are
implemented via caml's Set. Other modules just need to know about
the empty and union functions (and addition functions "enforce_geq"
and "enforce_eq" that were already there).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13725 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/univ.mli')
| -rw-r--r-- | kernel/univ.mli | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/kernel/univ.mli b/kernel/univ.mli index e9f25fe85..268321ece 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -42,9 +42,10 @@ val initial_universes : universes (** {6 Constraints. } *) -module Constraint : Set.S +type constraints -type constraints = Constraint.t +val empty_constraint : constraints +val union_constraints : constraints -> constraints -> constraints type constraint_function = universe -> universe -> constraints -> constraints |