corrections pour ocamlweb

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

5 files changed, 26 insertions, 18 deletions

diff --git a/.depend b/.depend
index 7b4bee928..f91880e20 100644
--- a/.depend
+++ b/.depend
@@ -45,6 +45,7 @@ parsing/coqast.cmi: lib/dyn.cmi
 parsing/g_minicoq.cmi: kernel/names.cmi lib/pp.cmi kernel/sign.cmi \
     kernel/term.cmi 
 parsing/pcoq.cmi: parsing/coqast.cmi 
+proofs/pfedit.cmi: lib/pp.cmi 
 proofs/proof_trees.cmi: parsing/coqast.cmi kernel/names.cmi kernel/term.cmi 
 toplevel/errors.cmi: parsing/coqast.cmi lib/pp.cmi 
 toplevel/himsg.cmi: kernel/environ.cmi kernel/names.cmi lib/pp.cmi \
@@ -153,8 +154,12 @@ kernel/typing.cmx: kernel/constant.cmx kernel/environ.cmx kernel/generic.cmx \
     kernel/typing.cmi 
 kernel/univ.cmo: kernel/names.cmi lib/pp.cmi lib/util.cmi kernel/univ.cmi 
 kernel/univ.cmx: kernel/names.cmx lib/pp.cmx lib/util.cmx kernel/univ.cmi 
+lib/bstack.cmo: lib/util.cmi lib/bstack.cmi 
+lib/bstack.cmx: lib/util.cmx lib/bstack.cmi 
 lib/dyn.cmo: lib/util.cmi lib/dyn.cmi 
 lib/dyn.cmx: lib/util.cmx lib/dyn.cmi 
+lib/edit.cmo: lib/bstack.cmi lib/pp.cmi lib/util.cmi lib/edit.cmi 
+lib/edit.cmx: lib/bstack.cmx lib/pp.cmx lib/util.cmx lib/edit.cmi 
 lib/hashcons.cmo: lib/hashcons.cmi 
 lib/hashcons.cmx: lib/hashcons.cmi 
 lib/options.cmo: lib/options.cmi 
@@ -259,12 +264,14 @@ toplevel/toplevel.cmx: parsing/ast.cmx toplevel/errors.cmx toplevel/mltop.cmx \
     lib/options.cmx parsing/pcoq.cmi proofs/pfedit.cmi lib/pp.cmx \
     toplevel/protectedtoplevel.cmx lib/util.cmx toplevel/vernac.cmx \
     toplevel/vernacinterp.cmi toplevel/toplevel.cmi 
-toplevel/vernac.cmo: parsing/ast.cmi library/discharge.cmi \
-    library/library.cmi parsing/pcoq.cmi proofs/pfedit.cmi lib/pp.cmi \
-    lib/system.cmi toplevel/vernacinterp.cmi toplevel/vernac.cmi 
-toplevel/vernac.cmx: parsing/ast.cmx library/discharge.cmi \
-    library/library.cmx parsing/pcoq.cmi proofs/pfedit.cmi lib/pp.cmx \
-    lib/system.cmx toplevel/vernacinterp.cmi toplevel/vernac.cmi 
+toplevel/vernac.cmo: parsing/ast.cmi parsing/coqast.cmi library/lib.cmi \
+    library/library.cmi lib/options.cmi parsing/pcoq.cmi proofs/pfedit.cmi \
+    lib/pp.cmi lib/system.cmi lib/util.cmi toplevel/vernacinterp.cmi \
+    toplevel/vernac.cmi 
+toplevel/vernac.cmx: parsing/ast.cmx parsing/coqast.cmx library/lib.cmx \
+    library/library.cmx lib/options.cmx parsing/pcoq.cmi proofs/pfedit.cmi \
+    lib/pp.cmx lib/system.cmx lib/util.cmx toplevel/vernacinterp.cmi \
+    toplevel/vernac.cmi 
 parsing/g_basevernac.cmo: parsing/ast.cmi parsing/coqast.cmi parsing/pcoq.cmi \
     toplevel/vernac.cmi 
 parsing/g_basevernac.cmx: parsing/ast.cmx parsing/coqast.cmx parsing/pcoq.cmi \
diff --git a/Makefile b/Makefile
index bc7a67eb1..42784478f 100644
--- a/Makefile
+++ b/Makefile
@@ -32,7 +32,8 @@ CAMLP4OBJS=gramlib.cma
 CONFIG=config/coq_config.cmo
 
 LIB=lib/pp_control.cmo lib/pp.cmo lib/util.cmo \
-    lib/hashcons.cmo lib/dyn.cmo lib/system.cmo lib/options.cmo
+    lib/hashcons.cmo lib/dyn.cmo lib/system.cmo lib/options.cmo \
+    lib/bstack.cmo lib/edit.cmo
 
 KERNEL=kernel/names.cmo kernel/generic.cmo kernel/univ.cmo kernel/term.cmo \
        kernel/sign.cmo kernel/evd.cmo kernel/constant.cmo \
diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml
index dcad19bed..643433e0c 100644
--- a/toplevel/toplevel.ml
+++ b/toplevel/toplevel.ml
@@ -40,8 +40,8 @@ let resynch_buffer ibuf =
         ibuf.start <- ibuf.start + ll
     | _ -> ()
 
-(* Read a char in an input channel, displaying a prompt af every
-   begining of line. *)
+(* Read a char in an input channel, displaying a prompt at every
+   beginning of line. *)
 
 let prompt_char ic ibuf count =
   let bol = match ibuf.bols with
@@ -125,8 +125,7 @@ let print_highlight_location ib (bp,ep) =
 let print_location_in_file s fname (bp,ep) =
   let errstrm = [< 'sTR"Error while reading "; 'sTR s; 'sTR" :"; 'fNL;
                    'sTR"File "; 'sTR ("\""^fname^"\"") >] in
-  if (bp,ep) = Ast.dummy_loc
-  then 
+  if (bp,ep) = Ast.dummy_loc then 
     [< errstrm; 'sTR", unknown location."; 'fNL >]
   else
     let ic = open_in fname in
@@ -241,8 +240,8 @@ let rec discard_to_dot () =
 
 
 (* If the error occured while parsing, we read the input until a dot token
- * in encountered.
- *)
+ * in encountered. *)
+
 let process_error = function
   | DuringCommandInterp _ as e -> e
   | e ->
@@ -266,7 +265,8 @@ let do_vernac () =
   begin 
     try 
       raw_do_vernac top_buffer.tokens
-    with e -> mSGNL (print_toplevel_error (process_error e)) 
+    with e -> 
+      mSGNL (print_toplevel_error (process_error e)) 
   end;
   flush_all()
 
diff --git a/toplevel/toplevel.mli b/toplevel/toplevel.mli
index 3d04fc625..22caa2a9f 100644
--- a/toplevel/toplevel.mli
+++ b/toplevel/toplevel.mli
@@ -25,7 +25,7 @@ val top_buffer : input_buffer
 val set_prompt : (unit -> string) -> unit
 
 (* Toplevel error explanation, dealing with locations, Drop, Ctrl-D
-  May raise only the following exceptions: Drop and End_of_input,
+  May raise only the following exceptions: [Drop] and [End_of_input],
   meaning we get out of the Coq loop *)
 
 val print_toplevel_error : exn -> std_ppcmds
diff --git a/toplevel/vernac.mli b/toplevel/vernac.mli
index 401598781..0c65b8693 100644
--- a/toplevel/vernac.mli
+++ b/toplevel/vernac.mli
@@ -3,18 +3,18 @@
 
 (* Parsing of vernacular. *)
 
-(* Like Exc_located, but specifies the outermost file read, the input buffer
+(* Like [Exc_located], but specifies the outermost file read, the input buffer
    associated to the location of the error, and the error itself. *)
 
 exception Error_in_file of string * (string * Coqast.loc) * exn
 
 (* Read a vernac command on the specified input (parse only).
-   Raises End_of_file if EOF (or Ctrl-D) is reached. *)
+   Raises [End_of_file] if EOF (or Ctrl-D) is reached. *)
 
 val parse_phrase : Pcoq.Gram.parsable * in_channel option -> Coqast.t
 
 (* Reads and executes vernac commands from a stream.
-   The boolean just_parsing disables interpretation of commands. *)
+   The boolean [just_parsing] disables interpretation of commands. *)
 
 exception DuringCommandInterp of Coqast.loc * exn
 exception End_of_input