package rocq-runtime

  1. Overview
  2. Docs
The Rocq Prover -- Core Binaries and Tools

Install 

dune-project
 Dependency

rocq-prover.org Readme Edit opam file Versions (6)

Authors

  1. T
    The Rocq development team, INRIA, CNRS, and contributors

Maintainers

  1. T
    The Rocq development team <rocq+rocq-development@discoursemail.com>

Sources

rocq-9.3.0.tar.gz
sha256=3f0fc283e8644394aa9c7a6e3995b6d9ebbe1e6dda712bf431f9c372dcef95ad

doc/rocq-runtime.tactics/Gentactic/index.html

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