diff options
Diffstat (limited to 'library/universes.mli')
| -rw-r--r-- | library/universes.mli | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/library/universes.mli b/library/universes.mli index 3b951997aa..4544bd4d38 100644 --- a/library/universes.mli +++ b/library/universes.mli @@ -144,6 +144,9 @@ val normalize_universe_subst : universe_subst ref -> val constr_of_global : Globnames.global_reference -> constr +(** ** DEPRECATED ** synonym of [constr_of_global] *) +val constr_of_reference : Globnames.global_reference -> constr + (** [unsafe_constr_of_global gr] turns [gr] into a constr, works on polymorphic references by taking the original universe instance that is not recorded anywhere. The constraints are forgotten as well. DO NOT USE in new code. *) @@ -154,6 +157,12 @@ val unsafe_constr_of_global : Globnames.global_reference -> constr in_universe_c universe counter, use with care). *) val type_of_global : Globnames.global_reference -> types in_universe_context_set +(** [unsafe_type_of_global gr] returns [gr]'s type, works on polymorphic + references by taking the original universe instance that is not recorded + anywhere. The constraints are forgotten as well. + USE with care. *) +val unsafe_type_of_global : Globnames.global_reference -> types + (** Full universes substitutions into terms *) val nf_evars_and_universes_local : (existential -> constr option) -> universe_level_subst -> |