diff options
| author | Théo Zimmermann | 2021-01-28 21:22:44 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2021-01-28 21:22:44 +0100 |
| commit | f7d37e69a3df1e049e0bee5d3a58ef2e7cf87af9 (patch) | |
| tree | eac7c7d3f6a125290ea41a2cbd8e93445933a379 /dev/bench | |
| parent | a54a5b83becd3ef7feef1352b56d10a3d74be85f (diff) | |
Replace : term with : type in open binders.
And update the doc_grammar files.
Diffstat (limited to 'dev/bench')
0 files changed, 0 insertions, 0 deletions