Module Ltac_pretype

Maps of pattern variables
type constr_under_binders = Names.Id.t list * EConstr.constr
type patvar_map = EConstr.constr Names.Id.Map.t
type extended_patvar_map = constr_under_binders Names.Id.Map.t
type closure = {
idents : Names.Id.t Names.Id.Map.t;
typed : constr_under_binders Names.Id.Map.t;
untyped : closed_glob_constr Names.Id.Map.t;
genargs : Geninterp.Val.t Names.Id.Map.t;

A globalised term together with a closure representing the value of its free variables. Intended for use when these variables are taken from the Ltac environment.

and closed_glob_constr = {
closure : closure;
term : Glob_term.glob_constr;
type var_map = constr_under_binders Names.Id.Map.t

Ltac variable maps

type uconstr_var_map = closed_glob_constr Names.Id.Map.t
type unbound_ltac_var_map = Geninterp.Val.t Names.Id.Map.t
type ltac_var_map = {
ltac_constrs : var_map;

Ltac variables bound to constrs

ltac_uconstrs : uconstr_var_map;

Ltac variables bound to untyped constrs

ltac_idents : Names.Id.t Names.Id.Map.t;

Ltac variables bound to identifiers

ltac_genargs : unbound_ltac_var_map;

All Ltac variables (to pass on ltac subterms, and for error reporting)