Up – coq-core » Heads

Module `Heads`

This module is about the computation of an approximation of the head symbol of defined constants and local definitions; it provides the function to compute the head symbols and a table to store the heads

is_rigid tells if some term is known to ultimately reduce to a term with a rigid head symbol

val is_rigid : Environ.env -> Evd.evar_map -> EConstr.constr -> bool