Module Geninterp

Interpretation functions for generic arguments and interpreted Ltac values.

Dynamic toplevel values
module Val : sig ... end
module ValTMap : functor (Value : Dyn.ValueS) -> Dyn.MapS with type 'a key = 'a Val.typ and type 'a value = 'a Value.t
val val_tag : 'a Genarg.typed_abstract_argument_type -> 'a Val.tag

Retrieve the dynamic type associated to a toplevel genarg.

val register_val0 : ('raw, 'glb, 'top) Genarg.genarg_type -> 'top Val.tag option -> unit

Register the representation of a generic argument. If no tag is given as argument, a new fresh tag with the same name as the argument is associated to the generic type.

Interpretation functions
module TacStore : Store.S
type interp_sign = {
lfun : Val.t Names.Id.Map.t;
poly : bool;
extra : TacStore.t;
}
type ('glb, 'top) interp_fun = interp_sign -> 'glb -> 'top Ftactic.t
val interp : ('raw, 'glb, 'top) Genarg.genarg_type -> ('glb, Val.t) interp_fun
val register_interp0 : ('raw, 'glb, 'top) Genarg.genarg_type -> ('glb, Val.t) interp_fun -> unit