Module HConstr

type t

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 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.

val hcons : t -> Constr.t