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 /kernel/mod_typing.ml | |
| 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.
Diffstat (limited to 'kernel/mod_typing.ml')
0 files changed, 0 insertions, 0 deletions