diff options
| author | Pierre-Marie Pédrot | 2021-03-10 12:17:32 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2021-03-10 12:20:27 +0100 |
| commit | aba594ca194390bb00f8ef60ef8a5eef6694fc07 (patch) | |
| tree | 2106e5937035b46bb8cea34a127e6903c0151561 /dev/base_include | |
| parent | 14d391651041291995c435cc8669e0f4a3146abb (diff) | |
Regenerate the Ltac2 syntax for documentation.
Diffstat (limited to 'dev/base_include')
0 files changed, 0 insertions, 0 deletions