diff options
| author | Théo Zimmermann | 2019-05-20 23:17:56 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2019-05-20 23:17:56 +0200 |
| commit | 59d0ac70a475b80d28e5d0ef4764515532d47533 (patch) | |
| tree | 2d077b3c83144ec531d70549f139394b334ee9f2 /dev | |
| parent | a5304d0a613141dd5008410034ae4b104f0fc06a (diff) | |
Minor Ltac2 documentation fix: type parameters are optional.
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions