documentation interfaces

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@244 85f007b7-540e-0410-9357-904b9bb8a0f7

11 files changed, 37 insertions, 9 deletions

diff --git a/toplevel/class.mli b/toplevel/class.mli
index 094b2ecc2..f916db079 100644
--- a/toplevel/class.mli
+++ b/toplevel/class.mli
@@ -1,10 +1,14 @@
 
 (* $Id$ *)
 
+(*i*)
 open Names
 open Term
 open Classops
 open Declare
+(*i*)
+
+(* Classes and coercions. *)
 
 val try_add_new_coercion : identifier -> strength -> unit
 val try_add_new_coercion_subclass : identifier -> strength -> unit
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 6a0a2e2a9..6fb0018dd 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -78,7 +78,8 @@ let abstraction_definition ident arity com =
 
 let parameter_def_var ident c =
   let c = constr_of_com1 true Evd.empty (Global.env()) c in
-  declare_parameter (id_of_string ident) c
+  declare_parameter (id_of_string ident) c;
+  if is_verbose() then message ((string_of_id ident) ^ " is assumed")
     
 let hypothesis_def_var is_refining ident n c =
   let warning () = 
@@ -94,6 +95,7 @@ let hypothesis_def_var is_refining ident n c =
         if Lib.is_section_p disch_sp then begin
           declare_variable (id_of_string ident)
              (constr_of_com1 true Evd.empty (Global.env()) c,n,false);
+	  if is_verbose() then message ((string_of_id ident) ^ " is assumed");
           if is_refining then 
             mSGERRNL [< 'sTR"Warning: Variable "; 'sTR ident; 
                         'sTR" is not visible from current goals" >]
diff --git a/toplevel/command.mli b/toplevel/command.mli
index 0ba5af296..8b99e1657 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -7,6 +7,9 @@ open Term
 open Declare
 (*i*)
 
+(* Declaration functions. The following functions take ASTs, transform them
+   into [constr] and then call the corresponding functions of [Declare]. *)
+
 val definition_body : identifier -> strength -> Coqast.t -> unit
 
 val definition_body_red : identifier -> strength -> Coqast.t 
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 01cfeb4e2..3de2b086f 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -1,8 +1,6 @@
 
 (* $Id$ *)
 
-(* The Coq main module. *)
-
 open Pp
 open Util
 open System
@@ -15,7 +13,6 @@ let print_header () =
   Printf.printf "Welcome to Coq %s (%s)\n" Coq_config.version Coq_config.date;
   flush stdout
 
-let batch_mode = ref false
 let set_batch_mode () = batch_mode := true
 
 let remove_top_ml () = Mltop.remove ()
diff --git a/toplevel/coqtop.mli b/toplevel/coqtop.mli
new file mode 100644
index 000000000..3a97b3b92
--- /dev/null
+++ b/toplevel/coqtop.mli
@@ -0,0 +1,9 @@
+
+(* $Id$ *)
+
+(* 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
diff --git a/toplevel/discharge.mli b/toplevel/discharge.mli
index 34b8bd1c7..3ff39c1f3 100644
--- a/toplevel/discharge.mli
+++ b/toplevel/discharge.mli
@@ -1,4 +1,9 @@
 
 (* $Id$ *)
 
+(* This module implements the discharge mechanism. It provides a function to
+   close the last opened section. That function calls [Lib.close_section] and
+   then re-introduce all the discharged versions of the objects that were
+   defined in the section. *)
+
 val close_section : bool -> string -> unit
diff --git a/toplevel/doc.tex b/toplevel/doc.tex
index bd1d1774d..845d5901d 100644
--- a/toplevel/doc.tex
+++ b/toplevel/doc.tex
@@ -4,3 +4,7 @@
 
 \ocwsection \label{toplevel}
 This chapter describes the highest modules of the \Coq\ system.
+They are organized as follows:
+
+\bigskip
+\begin{center}\epsfig{file=pretyping.dep.ps,width=\linewidth}\end{center}
diff --git a/toplevel/mltop.mli b/toplevel/mltop.mli
index 72f9d3aa8..817bc0531 100644
--- a/toplevel/mltop.mli
+++ b/toplevel/mltop.mli
@@ -1,7 +1,8 @@
 
 (* $Id$ *)
 
-(* If there is a toplevel under Coq *)
+(* If there is a toplevel under Coq, it is described by the following 
+   record. *)
 type toplevel = {
   load_obj : string -> unit;
   use_file : string -> unit;
diff --git a/toplevel/protectedtoplevel.mli b/toplevel/protectedtoplevel.mli
index c09fac3e0..f618c517f 100644
--- a/toplevel/protectedtoplevel.mli
+++ b/toplevel/protectedtoplevel.mli
@@ -5,6 +5,8 @@
 open Pp
 (*i*)
 
+(* A protected toplevel (used in Pcoq). *)
+
 val break_happened : bool ref
 val global_request_id : int ref
 val output_results_nl : std_ppcmds -> unit
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index a50dcfdf5..a0a4848f4 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -783,8 +783,7 @@ let _ =
                        hypothesis_def_var (refining()) (string_of_id s) 
 			 stre c;
                        if coe then
-			 Class.try_add_new_coercion s stre;
-		       message ((string_of_id s) ^ " is assumed"))
+			 Class.try_add_new_coercion s stre)
                     sl)
 	       slcl
        | _ -> bad_vernac_args "VARIABLE")
@@ -800,8 +799,7 @@ let _ =
 	       (fun (sl,c) ->
 		  List.iter 
 		    (fun s -> 
-		       parameter_def_var (string_of_id s) c;
-		       message ((string_of_id s) ^ " is assumed"))
+		       parameter_def_var (string_of_id s) c)
 		    sl)
                slcl
        | _ -> bad_vernac_args "PARAMETER")
diff --git a/toplevel/vernacentries.mli b/toplevel/vernacentries.mli
index 573bfccc2..0f793bbb9 100644
--- a/toplevel/vernacentries.mli
+++ b/toplevel/vernacentries.mli
@@ -7,6 +7,9 @@ open Term
 open Vernacinterp
 (*i*)
 
+(* Vernacular entries. This module registers almost all the vernacular entries,
+   by side-effects using [Vernacinterp.vinterp_add]. *)
+
 val join_binders : ('a list * 'b) list -> ('a * 'b) list
 val add : string -> (vernac_arg list -> unit -> unit) -> unit
 val show_script : unit -> unit