package rocq-runtime

  1. Overview
  2. Docs
package rocq-runtime
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module GenConstrSource

Sourcetype ('raw, 'glb) tag

Tags for extensible terms. The raw type is contained in constrexpr, and the glb type in glob terms.

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

Create a new tag. Tags should be registered with GlobEnv.register_constr_interp0, Genintern.register_intern_constr, Gensubst.register_constr_subst and Genprint.register_constr_print.

Also optionally

  • Genintern.register_ntn_subst0 (to be used in notations)
  • Genintern.register_intern_pat and Genintern.register_interp_pat (to be used in tactic patterns)
Sourceval eq : ('raw1, 'glb1) tag -> ('raw2, 'glb2) tag -> ('raw1 * 'glb1, 'raw2 * 'glb2) Util.eq option
Sourceval repr : (_, _) tag -> string
Sourcetype any_tag =
  1. | Any : (_, _) tag -> any_tag
Sourceval name : string -> any_tag option
Sourcetype raw =
  1. | Raw : ('raw, _) tag * 'raw -> raw
Sourcetype glb =
  1. | Glb : (_, 'glb) tag * 'glb -> glb
Sourcemodule Register (M : sig ... end) : sig ... end