Changé le nom du module Errors (errors.mli, errors.ml) en Cerrors parce

qu'il entre en conflit avec le module Errors ajouté dans OCaml courant
(future version OCaml 3.05).


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

11 files changed, 41 insertions, 41 deletions

diff --git a/.depend b/.depend
index 77449ac257..e34be00fb2 100644
--- a/.depend
+++ b/.depend
@@ -211,7 +211,7 @@ toplevel/command.cmi: parsing/coqast.cmi library/declare.cmi \
     pretyping/tacred.cmi kernel/term.cmi 
 toplevel/coqinit.cmi: kernel/names.cmi 
 toplevel/discharge.cmi: kernel/names.cmi 
-toplevel/errors.cmi: parsing/coqast.cmi lib/pp.cmi 
+toplevel/cerrors.cmi: parsing/coqast.cmi lib/pp.cmi 
 toplevel/fhimsg.cmi: kernel/environ.cmi kernel/names.cmi lib/pp.cmi \
     kernel/sign.cmi kernel/term.cmi kernel/type_errors.cmi 
 toplevel/himsg.cmi: pretyping/cases.cmi kernel/environ.cmi \
@@ -320,13 +320,13 @@ config/coq_config.cmx: config/coq_config.cmi
 dev/db_printers.cmo: kernel/names.cmi lib/pp.cmi 
 dev/db_printers.cmx: kernel/names.cmx lib/pp.cmx 
 dev/top_printers.cmo: parsing/ast.cmi proofs/clenv.cmi kernel/environ.cmi \
-    toplevel/errors.cmi pretyping/evd.cmi library/nameops.cmi \
+    toplevel/cerrors.cmi pretyping/evd.cmi library/nameops.cmi \
     kernel/names.cmi library/nametab.cmi lib/pp.cmi parsing/printer.cmi \
     proofs/proof_trees.cmi proofs/refiner.cmi kernel/sign.cmi lib/system.cmi \
     proofs/tacmach.cmi kernel/term.cmi parsing/termast.cmi \
     pretyping/termops.cmi kernel/univ.cmi 
 dev/top_printers.cmx: parsing/ast.cmx proofs/clenv.cmx kernel/environ.cmx \
-    toplevel/errors.cmx pretyping/evd.cmx library/nameops.cmx \
+    toplevel/cerrors.cmx pretyping/evd.cmx library/nameops.cmx \
     kernel/names.cmx library/nametab.cmx lib/pp.cmx parsing/printer.cmx \
     proofs/proof_trees.cmx proofs/refiner.cmx kernel/sign.cmx lib/system.cmx \
     proofs/tacmach.cmx kernel/term.cmx parsing/termast.cmx \
@@ -1404,13 +1404,13 @@ toplevel/coqinit.cmx: config/coq_config.cmx toplevel/mltop.cmx \
     lib/system.cmx toplevel/toplevel.cmx toplevel/vernac.cmx \
     toplevel/coqinit.cmi 
 toplevel/coqtop.cmo: config/coq_config.cmi toplevel/coqinit.cmi \
-    toplevel/errors.cmi library/lib.cmi library/library.cmi \
+    toplevel/cerrors.cmi library/lib.cmi library/library.cmi \
     toplevel/mltop.cmi library/nameops.cmi kernel/names.cmi \
     library/nametab.cmi lib/options.cmi lib/pp.cmi lib/profile.cmi \
     library/states.cmi lib/system.cmi toplevel/toplevel.cmi \
     toplevel/usage.cmi lib/util.cmi toplevel/vernac.cmi toplevel/coqtop.cmi 
 toplevel/coqtop.cmx: config/coq_config.cmx toplevel/coqinit.cmx \
-    toplevel/errors.cmx library/lib.cmx library/library.cmx \
+    toplevel/cerrors.cmx library/lib.cmx library/library.cmx \
     toplevel/mltop.cmx library/nameops.cmx kernel/names.cmx \
     library/nametab.cmx lib/options.cmx lib/pp.cmx lib/profile.cmx \
     library/states.cmx lib/system.cmx toplevel/toplevel.cmx \
@@ -1433,16 +1433,16 @@ toplevel/discharge.cmx: toplevel/class.cmx pretyping/classops.cmx \
     lib/pp.cmx toplevel/recordobj.cmx pretyping/recordops.cmx \
     kernel/reduction.cmx kernel/sign.cmx library/summary.cmx kernel/term.cmx \
     kernel/typeops.cmx kernel/univ.cmx lib/util.cmx toplevel/discharge.cmi 
-toplevel/errors.cmo: parsing/ast.cmi pretyping/cases.cmi toplevel/himsg.cmi \
+toplevel/cerrors.cmo: parsing/ast.cmi pretyping/cases.cmi toplevel/himsg.cmi \
     kernel/indtypes.cmi parsing/lexer.cmi proofs/logic.cmi \
     library/nametab.cmi lib/options.cmi lib/pp.cmi \
     pretyping/pretype_errors.cmi proofs/tacmach.cmi kernel/type_errors.cmi \
-    kernel/univ.cmi lib/util.cmi toplevel/errors.cmi 
-toplevel/errors.cmx: parsing/ast.cmx pretyping/cases.cmx toplevel/himsg.cmx \
+    kernel/univ.cmi lib/util.cmi toplevel/cerrors.cmi 
+toplevel/cerrors.cmx: parsing/ast.cmx pretyping/cases.cmx toplevel/himsg.cmx \
     kernel/indtypes.cmx parsing/lexer.cmx proofs/logic.cmx \
     library/nametab.cmx lib/options.cmx lib/pp.cmx \
     pretyping/pretype_errors.cmx proofs/tacmach.cmx kernel/type_errors.cmx \
-    kernel/univ.cmx lib/util.cmx toplevel/errors.cmi 
+    kernel/univ.cmx lib/util.cmx toplevel/cerrors.cmi 
 toplevel/fhimsg.cmo: kernel/environ.cmi parsing/g_minicoq.cmi \
     kernel/names.cmi lib/pp.cmi kernel/reduction.cmi kernel/sign.cmi \
     kernel/term.cmi kernel/type_errors.cmi lib/util.cmi toplevel/fhimsg.cmi 
@@ -1489,11 +1489,11 @@ toplevel/mltop.cmo: library/lib.cmi library/libobject.cmi library/library.cmi \
 toplevel/mltop.cmx: library/lib.cmx library/libobject.cmx library/library.cmx \
     kernel/names.cmx lib/options.cmx lib/pp.cmx library/summary.cmx \
     lib/system.cmx lib/util.cmx toplevel/vernacinterp.cmx toplevel/mltop.cmi 
-toplevel/protectedtoplevel.cmo: toplevel/errors.cmi \
+toplevel/protectedtoplevel.cmo: toplevel/cerrors.cmi \
     toplevel/line_oriented_parser.cmi parsing/pcoq.cmi lib/pp.cmi \
     toplevel/vernac.cmi toplevel/vernacinterp.cmi \
     toplevel/protectedtoplevel.cmi 
-toplevel/protectedtoplevel.cmx: toplevel/errors.cmx \
+toplevel/protectedtoplevel.cmx: toplevel/cerrors.cmx \
     toplevel/line_oriented_parser.cmx parsing/pcoq.cmx lib/pp.cmx \
     toplevel/vernac.cmx toplevel/vernacinterp.cmx \
     toplevel/protectedtoplevel.cmi 
@@ -1525,11 +1525,11 @@ toplevel/recordobj.cmx: pretyping/classops.cmx library/declare.cmx \
     library/lib.cmx library/nameops.cmx kernel/names.cmx library/nametab.cmx \
     lib/pp.cmx pretyping/recordops.cmx kernel/term.cmx pretyping/termops.cmx \
     lib/util.cmx toplevel/recordobj.cmi 
-toplevel/toplevel.cmo: parsing/ast.cmi toplevel/errors.cmi library/lib.cmi \
+toplevel/toplevel.cmo: parsing/ast.cmi toplevel/cerrors.cmi library/lib.cmi \
     toplevel/mltop.cmi kernel/names.cmi lib/options.cmi parsing/pcoq.cmi \
     proofs/pfedit.cmi lib/pp.cmi toplevel/protectedtoplevel.cmi lib/util.cmi \
     toplevel/vernac.cmi toplevel/vernacinterp.cmi toplevel/toplevel.cmi 
-toplevel/toplevel.cmx: parsing/ast.cmx toplevel/errors.cmx library/lib.cmx \
+toplevel/toplevel.cmx: parsing/ast.cmx toplevel/cerrors.cmx library/lib.cmx \
     toplevel/mltop.cmx kernel/names.cmx lib/options.cmx parsing/pcoq.cmx \
     proofs/pfedit.cmx lib/pp.cmx toplevel/protectedtoplevel.cmx lib/util.cmx \
     toplevel/vernac.cmx toplevel/vernacinterp.cmx toplevel/toplevel.cmi 
@@ -1970,7 +1970,7 @@ contrib/interface/centaur.cmo: contrib/interface/ascent.cmi parsing/ast.cmi \
     toplevel/command.cmi parsing/coqast.cmi contrib/interface/ctast.cmo \
     contrib/interface/dad.cmi contrib/interface/debug_tac.cmi \
     kernel/declarations.cmi library/declare.cmi kernel/environ.cmi \
-    toplevel/errors.cmi pretyping/evd.cmi library/global.cmi \
+    toplevel/cerrors.cmi pretyping/evd.cmi library/global.cmi \
     contrib/interface/history.cmi library/lib.cmi library/libobject.cmi \
     library/library.cmi toplevel/line_oriented_parser.cmi toplevel/mltop.cmi \
     contrib/interface/name_to_ast.cmi library/nameops.cmi kernel/names.cmi \
@@ -1989,7 +1989,7 @@ contrib/interface/centaur.cmx: contrib/interface/ascent.cmi parsing/ast.cmx \
     toplevel/command.cmx parsing/coqast.cmx contrib/interface/ctast.cmx \
     contrib/interface/dad.cmx contrib/interface/debug_tac.cmx \
     kernel/declarations.cmx library/declare.cmx kernel/environ.cmx \
-    toplevel/errors.cmx pretyping/evd.cmx library/global.cmx \
+    toplevel/cerrors.cmx pretyping/evd.cmx library/global.cmx \
     contrib/interface/history.cmx library/lib.cmx library/libobject.cmx \
     library/library.cmx toplevel/line_oriented_parser.cmx toplevel/mltop.cmx \
     contrib/interface/name_to_ast.cmx library/nameops.cmx kernel/names.cmx \
@@ -2024,11 +2024,11 @@ contrib/interface/dad.cmx: parsing/astterm.cmx contrib/interface/ctast.cmx \
     parsing/termast.cmx pretyping/typing.cmx lib/util.cmx \
     toplevel/vernacinterp.cmx contrib/interface/dad.cmi 
 contrib/interface/debug_tac.cmo: parsing/ast.cmi parsing/coqast.cmi \
-    toplevel/errors.cmi lib/pp.cmi parsing/printer.cmi proofs/proof_trees.cmi \
+    toplevel/cerrors.cmi lib/pp.cmi parsing/printer.cmi proofs/proof_trees.cmi \
     proofs/proof_type.cmi proofs/tacinterp.cmi proofs/tacmach.cmi \
     lib/util.cmi contrib/interface/debug_tac.cmi 
 contrib/interface/debug_tac.cmx: parsing/ast.cmx parsing/coqast.cmx \
-    toplevel/errors.cmx lib/pp.cmx parsing/printer.cmx proofs/proof_trees.cmx \
+    toplevel/cerrors.cmx lib/pp.cmx parsing/printer.cmx proofs/proof_trees.cmx \
     proofs/proof_type.cmx proofs/tacinterp.cmx proofs/tacmach.cmx \
     lib/util.cmx contrib/interface/debug_tac.cmi 
 contrib/interface/history.cmo: contrib/interface/paths.cmi \
@@ -2054,14 +2054,14 @@ contrib/interface/name_to_ast.cmx: parsing/ast.cmx pretyping/classops.cmx \
     pretyping/syntax_def.cmx kernel/term.cmx parsing/termast.cmx lib/util.cmx \
     contrib/interface/name_to_ast.cmi 
 contrib/interface/parse.cmo: contrib/interface/ascent.cmi \
-    config/coq_config.cmi contrib/interface/ctast.cmo toplevel/errors.cmi \
+    config/coq_config.cmi contrib/interface/ctast.cmo toplevel/cerrors.cmi \
     parsing/esyntax.cmi library/libobject.cmi library/library.cmi \
     contrib/interface/line_parser.cmi toplevel/metasyntax.cmi \
     library/nameops.cmi kernel/names.cmi library/nametab.cmi parsing/pcoq.cmi \
     lib/pp.cmi lib/system.cmi lib/util.cmi contrib/interface/vtp.cmi \
     contrib/interface/xlate.cmi 
 contrib/interface/parse.cmx: contrib/interface/ascent.cmi \
-    config/coq_config.cmx contrib/interface/ctast.cmx toplevel/errors.cmx \
+    config/coq_config.cmx contrib/interface/ctast.cmx toplevel/cerrors.cmx \
     parsing/esyntax.cmx library/libobject.cmx library/library.cmx \
     contrib/interface/line_parser.cmx toplevel/metasyntax.cmx \
     library/nameops.cmx kernel/names.cmx library/nametab.cmx parsing/pcoq.cmx \
diff --git a/Makefile b/Makefile
index b48cca2db2..7be6b4c2c9 100644
--- a/Makefile
+++ b/Makefile
@@ -122,7 +122,7 @@ TACTICS=tactics/dn.cmo tactics/termdn.cmo tactics/btermdn.cmo \
         tactics/tacticals.cmo tactics/tactics.cmo tactics/tacentries.cmo \
         tactics/hiddentac.cmo tactics/elim.cmo
 
-TOPLEVEL=toplevel/himsg.cmo toplevel/errors.cmo \
+TOPLEVEL=toplevel/himsg.cmo toplevel/cerrors.cmo \
          toplevel/metasyntax.cmo toplevel/command.cmo toplevel/class.cmo \
          toplevel/record.cmo toplevel/recordobj.cmo \
          toplevel/discharge.cmo toplevel/vernacinterp.cmo toplevel/mltop.cmo \
@@ -189,7 +189,7 @@ PARSERREQUIRES=config/coq_config.cmo lib/pp_control.cmo lib/pp.cmo \
 	proofs/proof_trees.cmo proofs/logic.cmo proofs/refiner.cmo \
 	proofs/evar_refiner.cmo proofs/tacmach.cmo toplevel/himsg.cmo \
 	parsing/g_natsyntax.cmo parsing/g_zsyntax.cmo parsing/g_rsyntax.cmo \
-	toplevel/errors.cmo
+	toplevel/cerrors.cmo
 
 ML4FILES += contrib/correctness/psyntax.ml4 contrib/field/field.ml4
 
diff --git a/contrib/interface/centaur.ml b/contrib/interface/centaur.ml
index 1cd2070479..6f5281d565 100644
--- a/contrib/interface/centaur.ml
+++ b/contrib/interface/centaur.ml
@@ -102,7 +102,7 @@ let ctf_acknowledge_command request_id command_count opt_exn =
     int goal_index ++ fnl () ++
     str !current_proof_name ++ fnl() ++
     (match opt_exn with
-      Some e -> Errors.explain_exn e
+      Some e -> Cerrors.explain_exn e
     | None -> mt ()) ++ fnl() ++ str "E-n-d---M-e-s-s-a-g-e" ++ fnl ());;
 
 let ctf_undoResults = ctf_header "undo_results";;
diff --git a/contrib/interface/debug_tac.ml b/contrib/interface/debug_tac.ml
index 80d9d72018..be469108fb 100644
--- a/contrib/interface/debug_tac.ml
+++ b/contrib/interface/debug_tac.ml
@@ -463,7 +463,7 @@ let descr_first_error = function
 	with
 	  e ->
 	    (msgnl (str "Execution of this tactic raised message " ++ fnl () ++
-		    fnl () ++ Errors.explain_exn e ++ fnl () ++
+		    fnl () ++ Cerrors.explain_exn e ++ fnl () ++
 		    fnl () ++ str "on goal"  ++ fnl () ++
 		    pr_goal (sig_it (strip_some !the_goal)) ++ fnl () ++
 		    str "faulty tactic is" ++ fnl () ++ fnl () ++
diff --git a/contrib/interface/parse.ml b/contrib/interface/parse.ml
index f68628eab6..389fa8cda8 100644
--- a/contrib/interface/parse.ml
+++ b/contrib/interface/parse.ml
@@ -171,7 +171,7 @@ let parse_command_list reqid stream string_list =
         with
         | (Stdpp.Exc_located(l, Stream.Error txt)) as e -> 
           begin
-             msgnl (ctf_SyntaxWarningMessage reqid (Errors.explain_exn e));
+             msgnl (ctf_SyntaxWarningMessage reqid (Cerrors.explain_exn e));
              try
                 discard_to_dot stream;
                 msgnl (str "debug" ++ fnl () ++ int this_pos ++ fnl () ++
@@ -244,11 +244,11 @@ let parse_string_action reqid phylum char_stream string_list =
  | Stdpp.Exc_located(l,Match_failure(_,_,_)) ->
     flush_until_end_of_stream char_stream;
     msgnl (ctf_SyntaxErrorMessage reqid
-              (Errors.explain_exn 
+              (Cerrors.explain_exn 
                  (Stdpp.Exc_located(l,Stream.Error "match failure"))))
  | e ->
     flush_until_end_of_stream char_stream;
-    msgnl (ctf_SyntaxErrorMessage reqid (Errors.explain_exn e));;
+    msgnl (ctf_SyntaxErrorMessage reqid (Cerrors.explain_exn e));;
 
 
 let quiet_parse_string_action char_stream =
@@ -282,7 +282,7 @@ let parse_file_action reqid file_name =
                    msgnl (ctf_SyntaxWarningMessage reqid
 			    (str "Error with file" ++ spc () ++
 			     str file_name ++ fnl () ++
-			     Errors.explain_exn 
+			     Cerrors.explain_exn 
 				 (Stdpp.Exc_located(l,Stream.Error txt))));
 		   (try 
 		      begin
@@ -328,13 +328,13 @@ let parse_file_action reqid file_name =
 	       (ctf_SyntaxErrorMessage reqid
 		  (str "Error with file" ++ spc () ++ str file_name ++ 
 		   fnl () ++
-		     Errors.explain_exn
+		     Cerrors.explain_exn
 		       (Stdpp.Exc_located(l,Stream.Error "match failure"))))
 	 | e ->
 	     msgnl
 	       (ctf_SyntaxErrorMessage reqid
 		  (str "Error with file" ++ spc () ++ str file_name ++
-		   fnl () ++ Errors.explain_exn e));;
+		   fnl () ++ Cerrors.explain_exn e));;
 
 (* This function is taken from Mltop.add_path *)
 
@@ -442,7 +442,7 @@ Libobject.relax true;
    with
      | End_of_file -> ()
      | e ->
-	 (msgnl (Errors.explain_exn e);
+	 (msgnl (Cerrors.explain_exn e);
 	  msgnl (str "could not load the VERNACRC file"));
 	 try
 	   msgnl (str vernacrc)
@@ -459,11 +459,11 @@ Libobject.relax true;
  with
    | End_of_file -> ()
    | e ->
-       msgnl (Errors.explain_exn e);
+       msgnl (Cerrors.explain_exn e);
        msgnl (str "error in your .vernacrc file"));
 msgnl (str "Starting Centaur Specialized Parser Loop");
 try
   coqparser_loop stdin
 with 
   | End_of_file -> ()
-  | e -> msgnl(Errors.explain_exn e))
+  | e -> msgnl(Cerrors.explain_exn e))
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 6d7a6b3675..b179428845 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -23,7 +23,7 @@ open Tacmach
 open Term
 open Termops
 open Clenv
-open Errors
+open Cerrors
 
 let _ = Termast.print_evar_arguments := true
 
diff --git a/toplevel/errors.ml b/toplevel/cerrors.ml
index da9ae4a4de..da9ae4a4de 100644
--- a/toplevel/errors.ml
+++ b/toplevel/cerrors.ml
diff --git a/toplevel/errors.mli b/toplevel/cerrors.mli
index 2207608a87..2207608a87 100644
--- a/toplevel/errors.mli
+++ b/toplevel/cerrors.mli
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index b273034df9..c174877dff 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -206,9 +206,9 @@ let parse_args () =
 	try
 	  Stream.empty s; exit 1
 	with Stream.Failure ->
-	  msgnl (Errors.explain_exn e); exit 1
+	  msgnl (Cerrors.explain_exn e); exit 1
       end
-    | e -> begin msgnl (Errors.explain_exn e); exit 1 end
+    | e -> begin msgnl (Cerrors.explain_exn e); exit 1 end
 
 
 (* To prevent from doing the initialization twice *)
diff --git a/toplevel/protectedtoplevel.ml b/toplevel/protectedtoplevel.ml
index 730b6768db..0e28a8373f 100644
--- a/toplevel/protectedtoplevel.ml
+++ b/toplevel/protectedtoplevel.ml
@@ -55,7 +55,7 @@ let acknowledge_command_ref =
          str "successfully executed " ++ int command_count ++ fnl () ++
            str "error message" ++ fnl () ++
          (match opt_exn with
-           Some e -> Errors.explain_exn e
+           Some e -> Cerrors.explain_exn e
          | None -> (mt ())) ++ fnl () ++
          str "E-n-d---M-e-s-s-a-g-e" ++ fnl ()))
 
@@ -151,7 +151,7 @@ let rec parse_one_command_group input_channel =
 let protected_loop input_chan =
   let rec explain_and_restart e =
     begin
-      output_results_nl(Errors.explain_exn e);
+      output_results_nl(Cerrors.explain_exn e);
       rearm_break();
       looprec input_chan;
     end
diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml
index 8bd6ba8e4a..29c0e60551 100644
--- a/toplevel/toplevel.ml
+++ b/toplevel/toplevel.ml
@@ -11,7 +11,7 @@
 open Pp
 open Util
 open Options
-open Errors
+open Cerrors
 open Vernac
 open Pcoq
 open Protectedtoplevel
@@ -124,7 +124,7 @@ let print_highlight_location ib (bp,ep) =
                       str sn ++ str dn) in 
 	  (l1 ++ li ++ ln)
   in 
-  (str"Toplevel input, characters " ++ Errors.print_loc (bp,ep) ++ fnl () ++
+  (str"Toplevel input, characters " ++ Cerrors.print_loc (bp,ep) ++ fnl () ++
      highlight_lines ++ fnl ())
 
 (* Functions to report located errors in a file. *)
@@ -147,7 +147,7 @@ let print_location_in_file s fname (bp,ep) =
       let (line, bol) = line_of_pos 1 0 0 in
       close_in ic;
       (errstrm ++ str", line " ++ int line ++
-         str", characters " ++ Errors.print_loc (bp-bol,ep-bol) ++ fnl ())
+         str", characters " ++ Cerrors.print_loc (bp-bol,ep-bol) ++ fnl ())
     with e -> (close_in ic; (errstrm ++ str", invalid location." ++ fnl ()))
 	
 let print_command_location ib dloc =
@@ -235,7 +235,7 @@ let print_toplevel_error exc =
 	raise Vernacinterp.Quit
     | _ -> 
 	(if is_pervasive_exn exc then (mt ()) else locstrm) ++
-        Errors.explain_exn exc
+        Cerrors.explain_exn exc
 
 (* Read the input stream until a dot is encountered *)
 let parse_to_dot =