diff options
| author |  Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
|---|---|---|
| committer | Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
| commit | 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 (patch) | |
| tree | 631ad791a7685edafeb1fb2e8faeedc8379318ae /toplevel/coqtop.mli | |
| parent | da178a880e3ace820b41d38b191d3785b82991f5 (diff) | |
Imported Upstream snapshot 8.3~beta0+13298
Diffstat (limited to 'toplevel/coqtop.mli')
| -rw-r--r-- | toplevel/coqtop.mli | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/toplevel/coqtop.mli b/toplevel/coqtop.mli index b5a1106c..87f4bdeb 100644 --- a/toplevel/coqtop.mli +++ b/toplevel/coqtop.mli @@ -6,17 +6,17 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: coqtop.mli 5920 2004-07-16 20:01:26Z herbelin $ i*) +(*i $Id$ i*) (* The Coq main module. The following function [start] will parse the - command line, print the banner, initialize the load path, load the input + 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. +(* [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 |