diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2013-12-13 16:39:44 +0000 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2014-05-06 09:58:57 +0200 |
| commit | 29794b8acf407518716f8c02c2ed20729f8802e5 (patch) | |
| tree | a7952e066c733ed10af5a5f43fcbff3ab960971d /library | |
| parent | 55e62174683f293c8f966d8bd486fcb511f66221 (diff) | |
- Fix abstract forgetting about new constraints.
Diffstat (limited to 'library')
| -rw-r--r-- | library/universes.ml | 3 | ||||
| -rw-r--r-- | library/universes.mli | 4 |
2 files changed, 3 insertions, 4 deletions
diff --git a/library/universes.ml b/library/universes.ml index b37970b38..d8fa563a0 100644 --- a/library/universes.ml +++ b/library/universes.ml @@ -144,8 +144,7 @@ let constr_of_global gr = else c let unsafe_constr_of_global gr = - let c, ctx = unsafe_global_instance (Global.env ()) gr in - c + unsafe_global_instance (Global.env ()) gr let constr_of_global_univ (gr,u) = match gr with diff --git a/library/universes.mli b/library/universes.mli index fb662d7a3..a41b07362 100644 --- a/library/universes.mli +++ b/library/universes.mli @@ -145,9 +145,9 @@ val normalize_universe_subst : universe_subst ref -> val constr_of_global : Globnames.global_reference -> constr (** [unsafe_constr_of_global gr] turns [gr] into a constr, works on polymorphic - reference by building a "dummy" universe instance that is not recorded + references by taking the original universe instance that is not recorded anywhere. The constraints are forgotten as well. DO NOT USE in new code. *) -val unsafe_constr_of_global : Globnames.global_reference -> constr +val unsafe_constr_of_global : Globnames.global_reference -> constr in_universe_context val type_of_global : Globnames.global_reference -> types in_universe_context_set |