diff options
| author | Pierre Courtieu | 2020-12-24 17:16:12 +0100 |
|---|---|---|
| committer | Pierre Courtieu | 2021-01-15 10:30:38 +0100 |
| commit | 9d153549fd8075160f05013b865939fbe8d59aeb (patch) | |
| tree | 2f31d3c0344749a02564990908c858f3f8805478 /doc | |
| parent | 0d731606bee81b2d73895a23b69e84796ea7e4e7 (diff) | |
Preventive support of "goal instead of "subgoal" in coq messages.
Coq team is currently considering changing all messages containing
"subgoal[s]" into "goal[s]". This commit allows for both.
I make this change as early as possible, even if this chage may not
land in coq's master, so that we support this as early as possible.
I don't see how this could break anything but again the earliest the
best.
Diffstat (limited to 'doc')
0 files changed, 0 insertions, 0 deletions