From 2b7ccb235b503f4c978009c2d7908d305cf85925 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Mon, 21 Jul 2014 18:31:41 +0200 Subject: Cleanup substitution inside universe instances, only done through subst_fn now, and disable hashconsing of substituted instances which had a huge performance penalty in general. They are hashconsed when put in the environment only now. --- library/universes.mli | 3 --- 1 file changed, 3 deletions(-) (limited to 'library/universes.mli') diff --git a/library/universes.mli b/library/universes.mli index 2fc476732..565f9fb0a 100644 --- a/library/universes.mli +++ b/library/universes.mli @@ -191,9 +191,6 @@ 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 -> - constr -> constr - val nf_evars_and_universes_opt_subst : (existential -> constr option) -> universe_opt_subst -> constr -> constr -- cgit v1.2.3