Gentactic (p.rocq-runtime.9.3.0.doc.rocq-runtime.tactics.Gentactic)

Sourcetype ('raw, 'glob) tag

val equal : 
  ('raw1, 'glob1) tag ->
  ('raw2, 'glob2) tag ->
  ('raw1 * 'glob1, 'raw2 * 'glob2) Util.eq option

Sourceval repr : (_, _) tag -> string

Sourcetype any_tag =

| Any : (_, _) tag -> any_tag

Sourceval name : string -> any_tag option

Sourcetype raw_generic_tactic =

| Raw : ('raw, _) tag * 'raw -> raw_generic_tactic

Sourcetype glob_generic_tactic =

| Glb : (_, 'glb) tag * 'glb -> glob_generic_tactic

Sourceval make : string -> ('raw, 'glb) tag

Each declared tag must be registered using all the following register functions (except when the callback cannot be called ie when the value type at that level is empty).

Sourceval empty : (Util.Empty.t, Util.Empty.t) tag

Sourceval of_raw : ('raw, _) tag -> 'raw -> raw_generic_tactic

Source

val register_print : 
  ('raw, 'glb) tag ->
  'raw Genprint.printer ->
  'glb Genprint.printer ->
  unit

Source

val print_raw : 
  Environ.env ->
  Evd.evar_map ->
  ?level:Constrexpr.entry_relative_level ->
  raw_generic_tactic ->
  Pp.t

Source

val print_glob : 
  Environ.env ->
  Evd.evar_map ->
  ?level:Constrexpr.entry_relative_level ->
  glob_generic_tactic ->
  Pp.t

Sourceval register_subst : (_, 'glb) tag -> 'glb Gensubst.subst_fun -> unit

Source

val subst : 
  Mod_subst.substitution ->
  glob_generic_tactic ->
  glob_generic_tactic

Source

val register_intern : 
  ('raw, 'glb) tag ->
  ('raw, 'glb) Genintern.intern_fun ->
  unit

Source

val intern : 
  ?strict:bool ->
  Environ.env ->
  ?ltacvars:Names.Id.Set.t ->
  raw_generic_tactic ->
  glob_generic_tactic

strict is default true

Source

val register_interp : 
  (_, 'glb) tag ->
  (Geninterp.Val.t Names.Id.Map.t -> 'glb -> unit Proofview.tactic) ->
  unit

Source

val interp : 
  ?lfun:Geninterp.Val.t Names.Id.Map.t ->
  glob_generic_tactic ->
  unit Proofview.tactic

Sourceval wit_generic_tactic : raw_generic_tactic Genarg.vernac_genarg_type

Sourcemodule Map (A : sig ... end) : sig ... end