package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
type interpretable

Tactic interpreters have to register their interpretation function

type 'a tactic_interpreter = private
  1. | Interpreter of 'a -> interpretable
val register_tactic_interpreter : string -> ('a -> unit Proofview.tactic) -> 'a tactic_interpreter

'a should be marshallable if ever used with par:. Must be called no more than once per process with a particular string: make sure to use partial application.

val solve : pstate:Declare.Proof.t -> Goal_select.t -> info:int option -> interpretable -> with_end_tac:bool -> Declare.Proof.t

Entry point for toplevel tactic expression execution. It calls Proof.solve after having interpreted the tactic, and after the tactic runs it unfocus as much as needed to put a goal under focus.

type parallel_solver = pstate:Declare.Proof.t -> info:int option -> interpretable -> abstract:bool -> with_end_tac:bool -> Declare.Proof.t

par: tac runs tac on all goals, possibly in parallel using a worker pool. If tac is abstract tac1, then abstract is passed explicitly to the solver and tac1 passed to worker since it is up to master to opacify the sub proofs produced by the workers.

val solve_parallel : parallel_solver

Entry point when the goal selector is par:

val set_par_implementation : parallel_solver -> unit

By default par: is implemented with all: (sequential). The STM and LSP document manager provide "more parallel" implementations

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct