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

5 files changed, 16 insertions, 8 deletions

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
diff --git a/library/declare.ml b/library/declare.ml
index dce84ff043..a83a7b4b0c 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -56,7 +56,7 @@ let cache_variable ((sp,_),o) =
   | Inr (id,(p,d,mk)) ->
   (* Constr raisonne sur les noms courts *)
   if variable_exists id then
-    errorlabstrm "cache_variable" (pr_id id ++ str " already exists");
+    alreadydeclared (pr_id id ++ str " already exists");
   let impl,opaq,cst = match d with (* Fails if not well-typed *)
     | SectionLocalAssum (ty, impl) ->
         let cst = Global.push_named_assum (id,ty) in
@@ -98,8 +98,7 @@ type constant_declaration = constant_entry * logical_kind
 (* section (if Remark or Fact) is needed to access a construction *)
 let load_constant i ((sp,kn),(_,_,kind)) =
   if Nametab.exists_cci sp then
-    errorlabstrm "cache_constant"
-      (pr_id (basename sp) ++ str " already exists");
+    alreadydeclared (pr_id (basename sp) ++ str " already exists");
   let con = Global.constant_of_delta (constant_of_kn kn) in
   Nametab.push (Nametab.Until i) sp (ConstRef con);
   add_constant_kind con kind
@@ -113,7 +112,7 @@ let cache_constant ((sp,kn),(cdt,dhyps,kind)) =
   let id = basename sp in
   let _,dir,_ = repr_kn kn in
   if variable_exists id or Nametab.exists_cci sp then
-    errorlabstrm "cache_constant" (pr_id id ++ str " already exists");
+    alreadydeclared (pr_id id ++ str " already exists");
   let kn' = Global.add_constant dir id cdt in
   assert (kn' = constant_of_kn kn);
   Nametab.push (Nametab.Until 1) sp (ConstRef (constant_of_kn kn));
@@ -210,11 +209,10 @@ let inductive_names sp kn mie =
 
 let check_exists_inductive (sp,_) =
   (if variable_exists (basename sp) then
-    errorlabstrm ""
-      (pr_id (basename sp) ++ str " already exists"));
+    alreadydeclared (pr_id (basename sp) ++ str " already exists"));
   if Nametab.exists_cci sp then
     let (_,id) = repr_path sp in
-    errorlabstrm "" (pr_id id ++ str " already exists")
+    alreadydeclared (pr_id id ++ str " already exists")
 
 let load_inductive i ((sp,kn),(_,mie)) =
   let names = inductive_names sp kn mie in
diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml
index 0186c69825..130b0b591a 100644
--- a/toplevel/cerrors.ml
+++ b/toplevel/cerrors.ml
@@ -140,6 +140,8 @@ let rec explain_exn_default_aux anomaly_string report_fn = function
 	       else
 		 (mt ())) ++
 	       report_fn ())
+  | AlreadyDeclared msg ->
+      hov 0 (msg ++ str ".")
   | reraise ->
       hov 0 (anomaly_string () ++ str "Uncaught exception " ++
 	       str (Printexc.to_string reraise) ++ report_fn ())
diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml
index 03a3ecac4f..b8f2986f3f 100644
--- a/toplevel/indschemes.ml
+++ b/toplevel/indschemes.ml
@@ -152,7 +152,9 @@ let try_declare_scheme what f internal names kn =
     | UndefinedCst s ->
 	alarm what internal
 	  (strbrk "Required constant " ++ str s ++ str " undefined.")
-    | _ ->
+    | AlreadyDeclared msg ->
+        alarm what internal (msg ++ str ".")
+    | _ -> 
 	alarm what internal
 	  (str "Unknown exception during scheme creation.")