summaryrefslogtreecommitdiff
path: root/ide/coqide.mli
blob: f904c730b138bb77ab1bdbf3898d1408c3bae5bf (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
(************************************************************************)
(*  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: coqide.mli 6621 2005-01-21 17:24:37Z herbelin $ i*)

(* The CoqIde main module. The following function [start] will parse the
   command line, 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 the interface. *)

val start : unit -> unit