package rocq-runtime

  1. Overview
  2. Docs

Module GentacticSource

Generic tactic expressions.

Sourcetype ('raw, 'glob) tag
Sourceval equal : ('raw1, 'glob1) tag -> ('raw2, 'glob2) tag -> ('raw1 * 'glob1, 'raw2 * 'glob2) Util.eq option
Sourceval repr : (_, _) tag -> string
Sourcetype any_tag =
  1. | Any : (_, _) tag -> any_tag
Sourceval name : string -> any_tag option
Sourcetype raw_generic_tactic =
  1. | Raw : ('raw, _) tag * 'raw -> raw_generic_tactic
Sourcetype glob_generic_tactic =
  1. | 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 of_raw : ('raw, _) tag -> 'raw -> raw_generic_tactic
Sourceval register_print : ('raw, 'glb) tag -> 'raw Genprint.printer -> 'glb Genprint.printer -> unit
Sourceval register_subst : (_, 'glb) tag -> 'glb Gensubst.subst_fun -> unit
Sourceval register_intern : ('raw, 'glb) tag -> ('raw, 'glb) Genintern.intern_fun -> unit
Sourceval intern : ?strict:bool -> Environ.env -> ?ltacvars:Names.Id.Set.t -> raw_generic_tactic -> glob_generic_tactic

strict is default true

Sourceval register_interp : (_, 'glb) tag -> (Geninterp.Val.t Names.Id.Map.t -> 'glb -> unit Proofview.tactic) -> unit
Sourcemodule Map (A : sig ... end) : sig ... end