diff options
author | 2018-07-21 11:29:31 +0200 | |
---|---|---|
committer | 2018-07-21 11:29:31 +0200 | |
commit | c56110635536a63117127be8ad07aaff0dc26a0a (patch) | |
tree | 6880c2bf0ebbf496e374f8a1476bb59d5e615dec /toplevel/metasyntax.mli | |
parent | d8cd9ba6d56d32eb8aa383bca9198a18517e82d3 (diff) | |
parent | b2bdaad8567e3ca91e036268a042129b6ce6f987 (diff) |
Merge PR #8086: Improved chapter 'The tactic language' of the Reference Manual.
Diffstat (limited to 'toplevel/metasyntax.mli')
0 files changed, 0 insertions, 0 deletions