1
(************************************************************************)
2
(* v * The Coq Proof Assistant / The Coq Development Team *)
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
4
(* \VV/ **************************************************************)
5
(* // * This file is distributed under the terms of the *)
6
(* * GNU Lesser General Public License Version 2.1 *)
7
(************************************************************************)
9
(*i $Id: vernac.mli 5920 2004-07-16 20:01:26Z herbelin $ i*)
11
(* Parsing of vernacular. *)
13
(* Read a vernac command on the specified input (parse only).
14
Raises [End_of_file] if EOF (or Ctrl-D) is reached. *)
16
val parse_phrase : Pcoq.Gram.parsable * in_channel option ->
17
Util.loc * Vernacexpr.vernac_expr
19
(* Reads and executes vernac commands from a stream.
20
The boolean [just_parsing] disables interpretation of commands. *)
22
exception DuringCommandInterp of Util.loc * exn
23
exception End_of_input
25
val just_parsing : bool ref
26
val raw_do_vernac : Pcoq.Gram.parsable -> unit
29
val set_xml_start_library : (unit -> unit) -> unit
30
val set_xml_end_library : (unit -> unit) -> unit
32
(* Load a vernac file, verbosely or not. Errors are annotated with file
35
val load_vernac : bool -> string -> unit
38
(* Compile a vernac file, verbosely or not (f is assumed without .v suffix) *)
40
val compile : bool -> string -> unit
42
(* Interpret a vernac AST *)
45
(Vernacexpr.vernac_expr -> unit) ->
46
Util.loc * Vernacexpr.vernac_expr -> unit