From 7c9f70309b0d21c0d4775bd9da00bdb72e8c1a9e Mon Sep 17 00:00:00 2001
From: vsiles
Date: Tue, 27 Apr 2010 13:38:38 +0000
Subject: Added a new exception for already declared Schemes, so that we can
 return the right error message when trying to declare a scheme twice.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12965 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 lib/util.ml  | 3 +++
 lib/util.mli | 3 +++
 2 files changed, 6 insertions(+)

(limited to 'lib')

diff --git a/lib/util.ml b/lib/util.ml
index f3b7c99e90..ce98d32349 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -22,6 +22,9 @@ let errorlabstrm l pps = raise (UserError(l,pps))
 
 exception AnomalyOnError of string * exn
 
+exception AlreadyDeclared of std_ppcmds (* for already declared Schemes *)
+let alreadydeclared pps = raise (AlreadyDeclared(pps))
+
 let todo s = prerr_string ("TODO: "^s^"\n")
 
 exception Timeout
diff --git a/lib/util.mli b/lib/util.mli
index 80f2fda380..810e6f0c77 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -26,6 +26,9 @@ exception UserError of string * std_ppcmds
 val error : string -> 'a
 val errorlabstrm : string -> std_ppcmds -> 'a
 
+exception AlreadyDeclared of std_ppcmds
+val alreadydeclared : std_ppcmds -> 'a
+
 exception AnomalyOnError of string * exn
 
 (* [todo] is for running of an incomplete code its implementation is
-- 
cgit v1.2.3