package coq-core

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
val fs_intern : Library.Intern.t

Regular intern using the filesystem

val interp : intern:Library.Intern.t -> ?verbosely:bool -> st:Vernacstate.t -> Vernacexpr.vernac_control -> Vernacstate.t

The main interpretation function of vernacular expressions

val interp_entry : ?verbosely:bool -> st:Vernacstate.t -> Synterp.vernac_control_entry -> Vernacstate.Interp.t

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

OCaml

Innovation. Community. Security.