diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-10-26 15:55:15 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-10-26 15:55:15 +0100 |
| commit | aff038fbbe5ade8d58a895b3d2f6e32267c5184c (patch) | |
| tree | 0598bda5a6432894e4fec9ac071cf9ad544d3ee2 /library | |
| parent | 010775eba60ea89645792b48a0686ff15c4ebcb5 (diff) | |
| parent | 6417a9e72feb39b87f0b456186100b11d1c87d5f (diff) | |
Merge branch 'v8.5'
Diffstat (limited to 'library')
| -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 |