package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
type interpretable
type !'a tactic_interpreter = private
  1. | Interpreter of 'a -> interpretable
val register_tactic_interpreter : string -> ('a -> unit Proofview.tactic) -> 'a tactic_interpreter
val solve : pstate:Declare.Proof.t -> Goal_select.t -> info:int option -> interpretable -> with_end_tac:bool -> Declare.Proof.t
type parallel_solver = pstate:Declare.Proof.t -> info:int option -> interpretable -> abstract:bool -> with_end_tac:bool -> Declare.Proof.t
val solve_parallel : parallel_solver
val set_par_implementation : parallel_solver -> unit