diff options
Diffstat (limited to 'engine/universes.mli')
-rw-r--r-- | engine/universes.mli | 13 |
1 files changed, 1 insertions, 12 deletions
diff --git a/engine/universes.mli b/engine/universes.mli index 6c2cee485..0f6e419d0 100644 --- a/engine/universes.mli +++ b/engine/universes.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -189,22 +189,11 @@ 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. *) -val unsafe_constr_of_global : Globnames.global_reference -> constr in_universe_context - (** Returns the type of the global reference, by creating a fresh instance of polymorphic references and computing their instantiated universe context. (side-effect on the 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_opt_subst : (existential -> constr option) -> |