aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/coqtop.mli
diff options
context:
space:
mode:
authorGravatar glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7>2009-09-17 15:58:14 +0000
committerGravatar glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7>2009-09-17 15:58:14 +0000
commit61ccbc81a2f3b4662ed4a2bad9d07d2003dda3a2 (patch)
tree961cc88c714aa91a0276ea9fbf8bc53b2b9d5c28 /toplevel/coqtop.mli
parent6d3fbdf36c6a47b49c2a4b16f498972c93c07574 (diff)
Delete trailing whitespaces in all *.{v,ml*} files
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel/coqtop.mli')
-rw-r--r--toplevel/coqtop.mli6
1 files changed, 3 insertions, 3 deletions
diff --git a/toplevel/coqtop.mli b/toplevel/coqtop.mli
index 6f3edf57f..87f4bdeb5 100644
--- a/toplevel/coqtop.mli
+++ b/toplevel/coqtop.mli
@@ -9,14 +9,14 @@
(*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