diff options
| -rw-r--r-- | library/declaremods.ml | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/library/declaremods.ml b/library/declaremods.ml index f66656d09..7f607a51c 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 |