diff options
| -rw-r--r-- | kernel/term.ml | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/kernel/term.ml b/kernel/term.ml index a3b066828..72489b49a 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. |