package coq

  1. Overview
  2. Docs
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module VernacinterpSource

Sourceval interp : ?verbosely:bool -> st:Vernacstate.t -> Vernacexpr.vernac_control -> Vernacstate.t

The main interpretation function of vernacular expressions

Execute a Qed but with a proof_object which may contain a delayed proof and won't be forced

Sourceval with_fail : st:Vernacstate.t -> (unit -> 'a) -> unit

with_fail ~st f runs f () and expects it to fail, otherwise it fails.

Sourceval test_mode : bool ref

Flag set when the test-suite is called. Its only effect to display verbose information for Fail

Sourceval get_default_proof_mode : unit -> Pvernac.proof_mode

Default proof mode set by `start_proof`

Sourceval proof_mode_opt_name : string list
OCaml

Innovation. Community. Security.