diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-09-04 11:24:40 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-09-04 11:28:28 +0200 |
| commit | 84916b37627cce78a313f850ecbcff1c3b8c3d49 (patch) | |
| tree | cbe69729218326516618c53d90122cd5b489b846 /pretyping/typing.mli | |
| parent | 1c3340c10b56ba821fe381f1e89bcfd48a04121e (diff) | |
Fix bug #3559, ensuring a canonical order of universe level quantifications when
introducing constants (e.g. Top.1 is always before Top.2), compatible with the one
used before introduction of hMaps in LMap/LSet.
Diffstat (limited to 'pretyping/typing.mli')
| -rw-r--r-- | pretyping/typing.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/typing.mli b/pretyping/typing.mli index 26dc8c560..03e62e006 100644 --- a/pretyping/typing.mli +++ b/pretyping/typing.mli @@ -12,7 +12,7 @@ open Environ open Evd (** This module provides the typing machine with existential variables - (but without universes). *) + and universes. *) (** Typecheck a term and return its type *) val type_of : env -> evar_map -> constr -> types |