aboutsummaryrefslogtreecommitdiff
path: root/contrib/interface
diff options
context:
space:
mode:
authorddr2002-02-20 11:06:07 +0000
committerddr2002-02-20 11:06:07 +0000
commitb7aa648034f73c390ba2b49c8d47c3c8277002ef (patch)
tree2bfd901db9221993c3373400bc19caf21b07e823 /contrib/interface
parent0a248d2fe0bb77952c94da34ca097996c0add227 (diff)
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
Diffstat (limited to 'contrib/interface')
-rw-r--r--contrib/interface/centaur.ml2
-rw-r--r--contrib/interface/debug_tac.ml2
-rw-r--r--contrib/interface/parse.ml18
3 files changed, 11 insertions, 11 deletions
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))