Hashconsed constr in an implicit environment, keeping variables which have different types and bodies separate.

For instance the x subterms in fun x : bool => x and fun x : nat => x are different (and have different hashes modulo accidental collision) and the x subterms in fun (y:nat) (x:bool) => x and fun (x:bool) (y:nat) => x are different (one is Rel 1, the other is Rel 2) but the x subterms in fun (y:nat) (x:bool) => x and fun (y:bool) (x:bool) => x are shared.

This allows using it as a cache key while typechecking.

Hashconsing information of subterms is also kept.

How many times this term appeared as a subterm of the argument to of_constr.

Build a t without hashconsing. Its refcount may be 1 even if an identical term was already seen.

May not be used to build Rel.

This is intended for the reconstruction of the inductive type when checking CaseInvert.

Imperative tables indexed by HConstr.t. The interfaces exposed are the same as Hashtbl but are not guaranteed to be implemented by Hashtbl.