`HConstr`

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.

`val self : t -> Constr.constr`

`val kind : t -> (t, t, Sorts.t, UVars.Instance.t, Sorts.relevance) Constr.kind_of_term`

`val refcount : t -> int`

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

.

`val of_constr : Environ.env -> Constr.constr -> t`

`val of_kind_nohashcons : (t, t, Sorts.t, UVars.Instance.t, Sorts.relevance) Constr.kind_of_term -> t`

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.

`module Tbl : sig ... end`

Imperative tables indexed by `HConstr.t`

. The interfaces exposed are the same as `Hashtbl`

but are not guaranteed to be implemented by `Hashtbl`

.