package rocq-runtime

You can search for identifiers within the package.

in-package search v0.2.0

The Rocq Prover -- Core Binaries and Tools

Install

dune-project

Dependency

sha256=a45280ab4fbaac7540b136a6b073b4a6db15739ec1e149bded43fa6f4fc25f20

Generic tactic expressions. Internally implemented using Genarg.

Sourcetype raw_generic_tactic

Sourcetype glob_generic_tactic

Sourceval of_raw_genarg : Genarg.raw_generic_argument -> raw_generic_tactic

The genarg must have registrations for all the following APIs.

Sourceval of_glob_genarg : Genarg.glob_generic_argument -> glob_generic_tactic

The 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.t

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

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

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

strict is default true

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

Sourceval to_raw_genarg : raw_generic_tactic -> Genarg.raw_generic_argument

For serlib