diff options
| author | Jason Gross | 2019-11-28 01:23:36 -0500 |
|---|---|---|
| committer | Jason Gross | 2019-11-28 01:23:36 -0500 |
| commit | 59ca9ed0f53b0c0e67a44135fbbf5f9fff616aa4 (patch) | |
| tree | 40584212708745d2c516d775be5e22468bcda47c /dev/base_include | |
| parent | d2a995927ccb01dae73960780c7fa0fed0a37e6d (diff) | |
Relax the pattern complexity test
c.f. discussion at
https://github.com/coq/coq/pull/11177#issuecomment-559139477
Diffstat (limited to 'dev/base_include')
0 files changed, 0 insertions, 0 deletions