diff options
| author | Clément Pit-Claudel | 2019-01-24 11:18:25 -0500 |
|---|---|---|
| committer | Clément Pit-Claudel | 2019-01-24 11:18:25 -0500 |
| commit | d79efa598d310b885c3472105d7d376f52dd3e50 (patch) | |
| tree | cbd706aea3ab03d92f582aac869683120d2d72df /plugins/syntax/plugin_base.dune | |
| parent | 1006fd52c03e7d8ea1d0b612df168f21c9b56455 (diff) | |
| parent | 4aa0dddfba559370fefa6fe1a6e7ffa00c2577c3 (diff) | |
Merge PR #9384: Improve the note in the beginning of the Ltac chapter.
Reviewed-by: cpitclaudel
Diffstat (limited to 'plugins/syntax/plugin_base.dune')
0 files changed, 0 insertions, 0 deletions