diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-07-21 18:31:41 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-07-21 18:41:37 +0200 |
| commit | 2b7ccb235b503f4c978009c2d7908d305cf85925 (patch) | |
| tree | ad3c4a3d218c20318c70fdd261edddcafbaf8b19 /library/universes.mli | |
| parent | 99efd521c3bd01f885248f6ac03c450e98929b2e (diff) | |
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.
Diffstat (limited to 'library/universes.mli')
| -rw-r--r-- | library/universes.mli | 3 |
1 files changed, 0 insertions, 3 deletions
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 |