From edcf0d8b8bff399443ddf4cd436185c33bf59829 Mon Sep 17 00:00:00 2001
From: aspiwack
Date: Fri, 13 May 2011 17:57:41 +0000
Subject: 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
---
 dev/printers.mllib  | 1 +
 dev/top_printers.ml | 4 ++--
 2 files changed, 3 insertions(+), 2 deletions(-)

(limited to 'dev')

diff --git a/dev/printers.mllib b/dev/printers.mllib
index 65283a843a..7b2d08c2af 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -7,6 +7,7 @@ Flags
 Segmenttree
 Unicodetable
 Util
+Errors
 Bigint
 Hashcons
 Dyn
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 681cb0634e..547ca0475a 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -414,7 +414,7 @@ let _ =
            (fun () -> in_current_context constr_display c)
        | _ -> failwith "Vernac extension: cannot occur")
   with
-    e -> Pp.pp (Cerrors.explain_exn e)
+    e -> Pp.pp (Errors.print e)
 let _ =
   extend_vernac_command_grammar "PrintConstr" None
     [[GramTerminal "PrintConstr";
@@ -431,7 +431,7 @@ let _ =
            (fun () -> in_current_context print_pure_constr c)
        | _ -> failwith "Vernac extension: cannot occur")
   with
-    e -> Pp.pp (Cerrors.explain_exn e)
+    e -> Pp.pp (Errors.print e)
 let _ =
   extend_vernac_command_grammar "PrintPureConstr" None
     [[GramTerminal "PrintPureConstr";
-- 
cgit v1.2.3