diff options
| author | Jim Fehrle | 2020-06-23 14:06:50 -0700 |
|---|---|---|
| committer | Jim Fehrle | 2020-07-08 11:36:27 -0700 |
| commit | fa3d479cbf3f84a231fe8587c321df03538b18e7 (patch) | |
| tree | 8e1beffb2922635ab6546014a4559a2989c0b3f4 /plugins/syntax/float_syntax.ml | |
| parent | b291704713f762cf93e5fda012f297ddd895b5fd (diff) | |
Add tags in prodn indicating productions that are from plugins,
filtered-only show Ltac2 tags outside of ltac2.rst
Diffstat (limited to 'plugins/syntax/float_syntax.ml')
0 files changed, 0 insertions, 0 deletions