summaryrefslogtreecommitdiff
path: root/toplevel/coqtop.mli
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2012-01-12 16:04:54 +0100
committerGravatar Stephane Glondu <steph@glondu.net>2012-01-12 16:04:54 +0100
commit39efc41237ec906226a3a53d7396d51173495204 (patch)
tree87cd58d72d43469d2a2a0a127c1060d7c9e0206b /toplevel/coqtop.mli
parent5fe4ac437bed43547b3695664974f492b55cb553 (diff)
parent97fefe1fcca363a1317e066e7f4b99b9c1e9987b (diff)
Remove non-DFSG contentsupstream/8.4_beta+dfsg
Diffstat (limited to 'toplevel/coqtop.mli')
-rw-r--r--toplevel/coqtop.mli15
1 files changed, 4 insertions, 11 deletions
diff --git a/toplevel/coqtop.mli b/toplevel/coqtop.mli
index ef730915..16d2b874 100644
--- a/toplevel/coqtop.mli
+++ b/toplevel/coqtop.mli
@@ -1,23 +1,16 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: coqtop.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
-(* The Coq main module. The following function [start] will parse the
+(** 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
+val init_toplevel : string list -> unit
+val start : unit -> unit