From b5d891154620e7f198059401344ee8f5488d077d Mon Sep 17 00:00:00 2001
From: letouzey
Date: Mon, 10 Oct 2011 22:54:07 +0000
Subject: Hash-cons the statically allocated Rels (1 to 16) to themselves

 This is just a minor detail, but if we take care to use in mkRel
 always the same physical Rels for n <= 16, then let's ensure that
 these Rels are preserved by hash-consing. This way, we avoid
 killing some sharing during hash-consing of most of constr but not
 all (for instance those in mind).

 In fact, this is probably superfluous since earlier commit
 about "| Rel n as t -> t", but let's be sure.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14542 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/term.ml | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'kernel')

diff --git a/kernel/term.ml b/kernel/term.ml
index a3b0668285..72489b49a8 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -1340,6 +1340,10 @@ let hcons_term (sh_sort,sh_ci,sh_construct,sh_ind,sh_con,sh_na,sh_id) =
     (H.may_add_and_get h y, h)
 
   in
+  (* Make sure our statically allocated Rels (1 to 16) are considered
+     as canonical, and hence hash-consed to themselves *)
+  ignore (hash_term_array rels);
+
   fun t -> fst (sh_rec t)
 
 (* Exported hashing fonction on constr, used mainly in plugins.
-- 
cgit v1.2.3