GentacticGeneric tactic expressions. Internally implemented using Genarg.
val of_raw_genarg : Genarg.raw_generic_argument -> raw_generic_tacticThe genarg must have registrations for all the following APIs.
val of_glob_genarg : Genarg.glob_generic_argument -> glob_generic_tacticThe genarg must have registrations for all the following APIs except those operating at the "raw" level.
val print_raw : Environ.env -> Evd.evar_map -> ?level:Constrexpr.entry_relative_level -> raw_generic_tactic -> Pp.tval print_glob : Environ.env -> Evd.evar_map -> ?level:Constrexpr.entry_relative_level -> glob_generic_tactic -> Pp.tval subst : Mod_subst.substitution -> glob_generic_tactic -> glob_generic_tacticval intern : ?strict:bool -> Environ.env -> ?ltacvars:Names.Id.Set.t -> raw_generic_tactic -> glob_generic_tacticstrict is default true
val interp : ?lfun:Geninterp.Val.t Names.Id.Map.t -> glob_generic_tactic -> unit Proofview.tacticval wit_generic_tactic : raw_generic_tactic Genarg.vernac_genarg_typeval to_raw_genarg : raw_generic_tactic -> Genarg.raw_generic_argumentFor serlib