From 6417a9e72feb39b87f0b456186100b11d1c87d5f Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Sun, 25 Oct 2015 16:40:32 +0100
Subject: Declaremods: replace two anomalies by user errors (fix #3974 and
 #3975)

 As shown by the code snippets in these bug reports, I've been too
 hasty in considering these situations as anomalies in commit 466c4cb
 (at least the one at the last line of consistency_checks). So let's turn
 these anomalies back to regular user errors, as they were before this commit.
---
 library/declaremods.ml | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/library/declaremods.ml b/library/declaremods.ml
index f66656d09a..7f607a51c9 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -166,12 +166,14 @@ let consistency_checks exists dir dirinfo =
     let globref =
       try Nametab.locate_dir (qualid_of_dirpath dir)
       with Not_found ->
-        anomaly (pr_dirpath dir ++ str " should already exist!")
+        errorlabstrm "consistency_checks"
+          (pr_dirpath dir ++ str " should already exist!")
     in
     assert (eq_global_dir_reference globref dirinfo)
   else
     if Nametab.exists_dir dir then
-      anomaly (pr_dirpath dir ++ str " already exists")
+      errorlabstrm "consistency_checks"
+        (pr_dirpath dir ++ str " already exists")
 
 let compute_visibility exists i =
   if exists then Nametab.Exactly i else Nametab.Until i
-- 
cgit v1.2.3