From 71563ebb86a83bc7cdfc17f58493f59428d764b0 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 12 Jul 2017 14:49:26 +0200 Subject: Safer API for constr_of_global, and getting rid of unsafe_constr_of_global. --- engine/universes.mli | 11 ----------- 1 file changed, 11 deletions(-) (limited to 'engine/universes.mli') diff --git a/engine/universes.mli b/engine/universes.mli index 5f4d212b6..8d0f106de 100644 --- a/engine/universes.mli +++ b/engine/universes.mli @@ -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) -> -- cgit v1.2.3