`ComTactic`

`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