diff options
| author | Pierre-Marie Pédrot | 2016-09-14 14:45:56 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-09-14 16:25:50 +0200 |
| commit | 5b1a15b5c561ed02335050f45ad123f8d548cee4 (patch) | |
| tree | d5227f3f8b5f90d2a82651804813cb37b17b2177 /dev/base_include | |
| parent | 5466267afa78cac5479a503338fbc57d77f05458 (diff) | |
Allowing to extend the Print Grammar command generically.
We also move the Ltac-specific grammar to its folder.
Diffstat (limited to 'dev/base_include')
0 files changed, 0 insertions, 0 deletions