diff options
| author | Clément Pit-Claudel | 2019-05-23 14:48:52 -0400 |
|---|---|---|
| committer | Clément Pit-Claudel | 2019-05-23 14:48:52 -0400 |
| commit | 5cfdc20560392c2125dbcee31cfd308d5346b428 (patch) | |
| tree | b5cfa5cf2bc2c3c8aa0195e8d27629b5cf2627c1 /tools | |
| parent | ad6e002b2d938217edb55da027ae380a6e4eff92 (diff) | |
| parent | a9697975825e408f80b488c5a7420615568b660e (diff) | |
Merge PR #10195: Minor Ltac2 documentation fix: type parameters are optional.
Reviewed-by: cpitclaudel
Reviewed-by: ppedrot
Diffstat (limited to 'tools')
0 files changed, 0 insertions, 0 deletions