A new mechanism to handle errors.

Instead of the monolitic Cerrors, I introduce a lightweight Errors module
whose error message can be expanded by module introducing exceptions.

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

9 files changed, 16 insertions, 16 deletions

diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 4f32bbd99d..21ee325398 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -36,7 +36,7 @@ let do_observe_tac s tac g =
  with e ->
    let goal = begin try (Printer.pr_goal g) with _ -> assert false end in
    msgnl (str "observation "++ s++str " raised exception " ++
-	    Cerrors.explain_exn e ++ str " on goal " ++ goal );
+	    Errors.print e ++ str " on goal " ++ goal );
    raise e;;
 
 let observe_tac_stream s tac g =
@@ -608,7 +608,7 @@ let my_orelse tac1 tac2 g =
   try
     tac1 g
   with e ->
-(*     observe (str "using snd tac since : " ++ Cerrors.explain_exn e); *)
+(*     observe (str "using snd tac since : " ++ Errors.print e); *)
     tac2 g
 
 let instanciate_hyps_with_args (do_prove:identifier list -> tactic) hyps args_id =
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index 39f4cf07f3..53ddfb9670 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -180,12 +180,12 @@ let warning_error names e =
 	Pp.msg_warning
 	  (str "Cannot define graph(s) for " ++
 	     h 1 (prlist_with_sep (fun _ -> str","++spc ()) Libnames.pr_reference names) ++
-	     if do_observe () then (spc () ++ Cerrors.explain_exn e) else mt ())
+	     if do_observe () then (spc () ++ Errors.print e) else mt ())
     | Defining_principle e ->
 	Pp.msg_warning
 	  (str "Cannot define principle(s) for "++
 	     h 1 (prlist_with_sep (fun _ -> str","++spc ()) Libnames.pr_reference names) ++
-	     if do_observe () then Cerrors.explain_exn e else mt ())
+	     if do_observe () then Errors.print e else mt ())
     | _ -> raise e
 
 
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 394417abb1..6d4e8929aa 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -1404,7 +1404,7 @@ let do_build_inductive
 	  str "while trying to define"++ spc () ++
 	    Ppvernac.pr_vernac (Vernacexpr.VernacInductive(Decl_kinds.Finite,false,repacked_rel_inds))
 	    ++ fnl () ++
-	    Cerrors.explain_exn e
+	    Errors.print e
 	in
  	observe msg;
 	raise e
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index dd48765fb5..d98960a489 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -254,14 +254,14 @@ let derive_inversion fix_names =
     with e ->
       msg_warning
 	(str "Cannot built inversion information" ++
-	   if do_observe () then Cerrors.explain_exn e else mt ())
+	   if do_observe () then Errors.print e else mt ())
   with _ -> ()
 
 let warning_error names e =
   let e_explain e =
     match e with
-      | ToShow e -> spc () ++ Cerrors.explain_exn e
-      | _ -> if do_observe () then (spc () ++ Cerrors.explain_exn e) else mt ()
+      | ToShow e -> spc () ++ Errors.print e
+      | _ -> if do_observe () then (spc () ++ Errors.print e) else mt ()
   in
   match e with
     | Building_graph e ->
@@ -279,8 +279,8 @@ let warning_error names e =
 let error_error names e =
   let e_explain e =
     match e with
-      | ToShow e -> spc () ++ Cerrors.explain_exn e
-      | _ -> if do_observe () then (spc () ++ Cerrors.explain_exn e) else mt ()
+      | ToShow e -> spc () ++ Errors.print e
+      | _ -> if do_observe () then (spc () ++ Errors.print e) else mt ()
   in
   match e with
     | Building_graph e ->
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 426b496dd1..1b7a190298 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -64,7 +64,7 @@ let do_observe_tac s tac g =
     let v = tac g in msgnl (goal ++ fnl () ++ s ++(str " ")++(str "finished")); v
   with e ->
     msgnl (str "observation "++ s++str " raised exception " ++
-	     Cerrors.explain_exn e ++ str " on goal " ++ goal );
+	     Errors.print e ++ str " on goal " ++ goal );
     raise e;;
 
 
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 11fbc01baf..5b689625bc 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -75,7 +75,7 @@ let rec print_debug_queue b e =
     begin
       let lmsg,goal = Stack.pop debug_queue in 
       if b then 
-	msgnl (lmsg ++ (str " raised exception " ++ Cerrors.explain_exn e) ++ str " on goal " ++ goal)
+	msgnl (lmsg ++ (str " raised exception " ++ Errors.print e) ++ str " on goal " ++ goal)
       else
 	begin
 	  msgnl (str " from " ++ lmsg ++ str " on goal " ++ goal);
@@ -1433,7 +1433,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
       with e ->
 	begin
 	  if Tacinterp.get_debug () <> Tactic_debug.DebugOff
-	  then pperrnl (str "Cannot create equation Lemma " ++ Cerrors.explain_exn e)
+	  then pperrnl (str "Cannot create equation Lemma " ++ Errors.print e)
 	  else anomaly "Cannot create equation Lemma"
 	  ;
 (* 	  ignore(try Vernacentries.vernac_reset_name (Util.dummy_loc,functional_id) with _ -> ()); *)
diff --git a/plugins/subtac/g_subtac.ml4 b/plugins/subtac/g_subtac.ml4
index c42f13b045..ca1240e5f1 100644
--- a/plugins/subtac/g_subtac.ml4
+++ b/plugins/subtac/g_subtac.ml4
@@ -90,7 +90,7 @@ VERNAC COMMAND EXTEND Subtac
 
 let try_catch_exn f e =
   try f e
-  with exn -> errorlabstrm "Program" (Cerrors.explain_exn exn)
+  with exn -> errorlabstrm "Program" (Errors.print exn)
 
 let subtac_obligation e = try_catch_exn Subtac_obligations.subtac_obligation e
 let next_obligation e = try_catch_exn Subtac_obligations.next_obligation e
diff --git a/plugins/subtac/subtac.ml b/plugins/subtac/subtac.ml
index fbdaa8d3b1..710149ae4f 100644
--- a/plugins/subtac/subtac.ml
+++ b/plugins/subtac/subtac.ml
@@ -224,5 +224,5 @@ let subtac (loc, command) =
      Loc.Exc_located (loc, e') as e) -> raise e
 
   | e -> 
-      (*       msg_warning (str "Uncaught exception: " ++ Cerrors.explain_exn e); *)
+      (*       msg_warning (str "Uncaught exception: " ++ Errors.print e); *)
       raise e
diff --git a/plugins/subtac/subtac_obligations.ml b/plugins/subtac/subtac_obligations.ml
index 76cc7644d6..5c2f24a673 100644
--- a/plugins/subtac/subtac_obligations.ml
+++ b/plugins/subtac/subtac_obligations.ml
@@ -482,7 +482,7 @@ let rec solve_obligation prg num tac =
 		let obls = Array.copy obls in
 		let _ = obls.(num) <- obl in
 		let res = try update_obls prg obls (pred rem)
-		  with e -> pperror (Cerrors.explain_exn e)
+		  with e -> pperror (Errors.print e)
 		in
 		  match res with
 		  | Remain n when n > 0 ->