Module PvernacSource

Sourcetype proof_mode
Sourcemodule Vernac_ : sig ... end
Sourcemodule Unsafe : sig ... end
Sourceval main_entry : proof_mode option -> Vernacexpr.vernac_control option Pcoq.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.

Sourceval register_proof_mode : string -> Vernacexpr.vernac_expr Pcoq.Entry.t -> proof_mode
Sourceval lookup_proof_mode : string -> proof_mode option
Sourceval proof_mode_to_string : proof_mode -> string