blob: ef8b4b376b26b55a6c637d3d497fbee192cdaefa (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(*i $Id: coqtop.mli,v 1.5.4.1 2004/07/16 19:31:47 herbelin Exp $ i*)
(* The Coq main module. The following function [start] will parse the
command line, print the banner, initialize the load path, load the input
state, load the files given on the command line, load the ressource file,
produce the output state if any, and finally will launch [Toplevel.loop]. *)
val start : unit -> unit
(* [init_ide] is to be used by the Coq IDE.
It does everything [start] does, except launching the toplevel loop.
It returns the list of Coq files given on the command line. *)
val init_ide : unit -> string list
|
