diff options
| author | Gaëtan Gilbert | 2021-03-23 18:47:23 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2021-03-24 11:23:56 +0100 |
| commit | 9583c0eb1771302e091880f598884b98eaec9742 (patch) | |
| tree | f93c06f638197b07c6c570d9130101e254c6c6ff /vernac | |
| parent | d3f78cad1532f000106ed0c0b8be2ac384ce1d3a (diff) | |
Mention label name in signature mismatch error when constant expected
Fix #13987
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/himsg.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/vernac/himsg.ml b/vernac/himsg.ml index bff0359782..21a25ab78c 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -924,7 +924,9 @@ let explain_not_match_error = function | InductiveFieldExpected _ -> strbrk "an inductive definition is expected" | DefinitionFieldExpected -> - strbrk "a definition is expected" + strbrk "a definition is expected. Hint: you can rename the \ + inductive or constructor and add a definition mapping the \ + old name to the new name" | ModuleFieldExpected -> strbrk "a module is expected" | ModuleTypeFieldExpected -> |