diff options
| author | coqbot-app[bot] | 2021-01-28 21:25:59 +0000 |
|---|---|---|
| committer | GitHub | 2021-01-28 21:25:59 +0000 |
| commit | 4ae11ea2bf09fcdf44b1226a45761a2aed34a445 (patch) | |
| tree | f75555ca01275dc1b5331dda71247a04ad141499 /dev/bench | |
| parent | ed29e0913742c307175846557ed8390a8da771e3 (diff) | |
| parent | f7d37e69a3df1e049e0bee5d3a58ef2e7cf87af9 (diff) | |
Merge PR #13799: Replace : term with : type in open binders.
Reviewed-by: jfehrle
Diffstat (limited to 'dev/bench')
0 files changed, 0 insertions, 0 deletions