diff options
| author | Pierre-Marie Pédrot | 2021-03-25 15:39:40 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2021-03-25 15:39:40 +0100 |
| commit | e96e5ef09d4a009780a8267c9289a1b5cf077653 (patch) | |
| tree | b9f386e9a07bf046ee0df801212d42c8e45b52ab /vernac | |
| parent | d328a04d5e533a8591dfb3f2fa3d0e0852037f33 (diff) | |
| parent | 9583c0eb1771302e091880f598884b98eaec9742 (diff) | |
Merge PR #13988: Mention label name in signature mismatch error when constant expected
Reviewed-by: ppedrot
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 -> |