diff options
| author | Hugo Herbelin | 2019-11-13 20:54:52 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-05-06 17:04:11 +0200 |
| commit | 986bfd1ff69231f1b17efda2fa5d13b88a39caee (patch) | |
| tree | 0868872b9517fe66cb9388dd2c871f8a61e1e2fa /plugins | |
| parent | 259162be000a8a66bf4f551be64d6a5d61edce05 (diff) | |
Mention keywords from g_ltac.mlg used in Ltac.
Diffstat (limited to 'plugins')
0 files changed, 0 insertions, 0 deletions