diff options
| author | glondu | 2011-01-11 16:57:35 +0000 |
|---|---|---|
| committer | glondu | 2011-01-11 16:57:35 +0000 |
| commit | 64edc250dddb2ea8404a68d4d387088c4b10ecac (patch) | |
| tree | f196b049468801aaf9b1091136cfef83bd748880 /kernel | |
| parent | be4fe5a4351ad7b315983c5959daf8ff6c7a193e (diff) | |
More coherent comment ordering
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13784 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/univ.ml | 30 | ||||
| -rw-r--r-- | kernel/univ.mli | 2 |
2 files changed, 17 insertions, 15 deletions
diff --git a/kernel/univ.ml b/kernel/univ.ml index 7f49e6e761..db5b071313 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -13,6 +13,9 @@ (* Revisions by Bruno Barras, Hugo Herbelin, Pierre Letouzey *) +open Pp +open Util + (* Universes are stratified by a partial ordering $\le$. Let $\~{}$ be the associated equivalence. We also have a strict ordering $<$ between equivalence classes, and we maintain that $<$ is acyclic, @@ -25,21 +28,6 @@ union-find algorithm. The assertions $<$ and $\le$ are represented by adjacency lists *) -open Pp -open Util - -(* An algebraic universe [universe] is either a universe variable - [universe_level] or a formal universe known to be greater than some - universe variables and strictly greater than some (other) universe - variables - - Universes variables denote universes initially present in the term - to type-check and non variable algebraic universes denote the - universes inferred while type-checking: it is either the successor - of a universe present in the initial term to type-check or the - maximum of two algebraic universes - *) - type universe_level = | Set | Level of Names.dir_path * int @@ -63,6 +51,18 @@ let string_of_univ_level = function module UniverseLMap = Map.Make (struct type t = universe_level let compare = cmp_univ_level end) +(* An algebraic universe [universe] is either a universe variable + [universe_level] or a formal universe known to be greater than some + universe variables and strictly greater than some (other) universe + variables + + Universes variables denote universes initially present in the term + to type-check and non variable algebraic universes denote the + universes inferred while type-checking: it is either the successor + of a universe present in the initial term to type-check or the + maximum of two algebraic universes + *) + type universe = | Atom of universe_level | Max of universe_level list * universe_level list diff --git a/kernel/univ.mli b/kernel/univ.mli index 268321ece4..83c69da99d 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -90,4 +90,6 @@ val dump_universes : (constraint_type -> string -> string -> unit) -> universes -> unit +(** {6 Hash-consing } *) + val hcons1_univ : universe -> universe |