diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-06-07 17:07:08 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-09-01 12:04:59 +0200 |
| commit | 420c919854f50b9f9d47ba8299dc27f0df051d30 (patch) | |
| tree | b5f75108a039efa92bd3875960997f9e5a82b684 /checker/univ.mli | |
| parent | 3072bd9d080984833f5eb007bf15c6e9305619e3 (diff) | |
Do not hashcons universes beforehand.
This should save a lot of useless reallocations and hashset crawling, which
end up costing a lot.
Diffstat (limited to 'checker/univ.mli')
| -rw-r--r-- | checker/univ.mli | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/checker/univ.mli b/checker/univ.mli index 0a21019b1..0eadc6801 100644 --- a/checker/univ.mli +++ b/checker/univ.mli @@ -164,7 +164,6 @@ sig val is_empty : t -> bool val equal : t -> t -> bool - (** Equality (note: instances are hash-consed, this is O(1)) *) val subst_fn : universe_level_subst_fn -> t -> t (** Substitution by a level-to-level function. *) |