diff options
| author | Gaëtan Gilbert | 2019-02-08 16:42:15 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-02-08 16:52:50 +0100 |
| commit | 93dc998702e7c3ba13d3bc0250446dcad5fd027d (patch) | |
| tree | ea0a3413f15dbd1b3867c913791d3cfbbe59f54b /pretyping/typeclasses_errors.mli | |
| parent | 8c1c7601674f150a969223c67f3e963141b07b4f (diff) | |
Change Primitive message: "is registered" -> "is declared".
"registered" sounds like it existed before the command.
This could use assumption_message which is currently the same, but I
don't think it has the right semantic.
Diffstat (limited to 'pretyping/typeclasses_errors.mli')
0 files changed, 0 insertions, 0 deletions