diff options
| author |  Pierre Letouzey <pierre.letouzey@inria.fr> | 2015-10-25 16:40:32 +0100 |
|---|---|---|
| committer | Pierre Letouzey <pierre.letouzey@inria.fr> | 2015-10-25 16:46:12 +0100 |
| commit | 6417a9e72feb39b87f0b456186100b11d1c87d5f (patch) | |
| tree | 3113152656e5773dcfc8b7d2f6d868f4a57f1f6a | |
| parent | 83e82ef7b42f47d63d3b40b2698695a0e7b2d685 (diff) | |
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.
| -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 |