diff options
| author |  glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-11-03 09:54:06 +0000 |
|---|---|---|
| committer | glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-11-03 09:54:06 +0000 |
| commit | ef0da718a83ebfa1d953ad8fd53506b5657c349a (patch) | |
| tree | 395d540ee787f49b5592dc1d844a8cfca52cdfc1 /kernel/univ.mli | |
| parent | 2a7a989025a5dde9a6f34792e1e1f2b4e3ad3108 (diff) | |
In Univ, unify order_request and constraint_type
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13614 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/univ.mli')
| -rw-r--r-- | kernel/univ.mli | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/kernel/univ.mli b/kernel/univ.mli index 85e227891..e9f25fe85 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -57,9 +57,9 @@ val enforce_eq : constraint_function universes graph. It raises the exception [UniverseInconsistency] if the constraints are not satisfiable. *) -type order_request = Lt | Le | Eq +type constraint_type = Lt | Le | Eq -exception UniverseInconsistency of order_request * universe * universe +exception UniverseInconsistency of constraint_type * universe * universe val merge_constraints : constraints -> universes -> universes @@ -86,7 +86,7 @@ val pr_constraints : constraints -> Pp.std_ppcmds (** {6 Dumping to a file } *) val dump_universes : - ([> `Lt | `Le | `Eq ] -> string -> string -> unit) -> + (constraint_type -> string -> string -> unit) -> universes -> unit val hcons1_univ : universe -> universe |