From 420c919854f50b9f9d47ba8299dc27f0df051d30 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Wed, 7 Jun 2017 17:07:08 +0200
Subject: Do not hashcons universes beforehand.

This should save a lot of useless reallocations and hashset crawling, which
end up costing a lot.
---
 checker/univ.mli | 1 -
 1 file changed, 1 deletion(-)

(limited to 'checker/univ.mli')

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. *)
-- 
cgit v1.2.3