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 /kernel/univ.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 'kernel/univ.mli')
| -rw-r--r-- | kernel/univ.mli | 5 |
1 files changed, 1 insertions, 4 deletions
diff --git a/kernel/univ.mli b/kernel/univ.mli index 9b68dbc8c..25d25fa35 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -272,7 +272,7 @@ sig (** To concatenate two instances, used for discharge *) val equal : t -> t -> bool - (** Equality (note: instances are hash-consed, this is O(1)) *) + (** Equality *) val hcons : t -> t (** Hash-consing. *) @@ -289,9 +289,6 @@ sig val subst_fn : universe_level_subst_fn -> t -> t (** Substitution by a level-to-level function. *) - val subst : universe_level_subst -> t -> t - (** Substitution by a level-to-level function. *) - val pr : t -> Pp.std_ppcmds (** Pretty-printing, no comments *) |