diff options
| author | Hugo Herbelin | 2020-06-01 17:39:47 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2021-04-06 17:40:53 +0200 |
| commit | 2ee505630756676ded9f8eb6511ad642c80179ee (patch) | |
| tree | 0fa3f7ec475ee5e8412e63caf5a412f8656ac7af /doc/plugin_tutorial/tuto3/_CoqProject | |
| parent | 524eb4e7dcb18d622ebb99648862e5d08a972117 (diff) | |
Uniformizing the "already exists" messages
Diffstat (limited to 'doc/plugin_tutorial/tuto3/_CoqProject')
0 files changed, 0 insertions, 0 deletions