Module Pvernac

type proof_mode
module Vernac_ : sig ... end
module Unsafe : sig ... end
val main_entry : proof_mode option -> Vernacexpr.vernac_control option Procq.Entry.t

The main entry: reads an optional vernac command

Grammar entry for tactics: proof mode(s). By default Coq's grammar has an empty entry (non-terminal) for tactics. A plugin can register its non-terminal by providing a name and a grammar entry.

For example the Ltac plugin register the "Classic" grammar entry for parsing its tactics.

type proof_mode_entry =
| ProofMode : {
command_entry : Vernacexpr.vernac_expr Procq.Entry.t;
wit_tactic_expr : ('raw, _, unit) Genarg.genarg_type;
tactic_expr_entry : 'raw Procq.Entry.t;
} -> proof_mode_entry
val register_proof_mode : string -> proof_mode_entry -> proof_mode
val lookup_proof_mode : string -> proof_mode option
val proof_mode_to_string : proof_mode -> string
val list_proof_modes : unit -> proof_mode_entry CString.Map.t
val get_default_proof_mode : unit -> proof_mode
val proof_mode_opt_name : string list