diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-09-25 19:49:30 +0200 |
|---|---|---|
| committer |  Jason Gross <jasongross9@gmail.com> | 2018-09-26 15:18:06 -0400 |
| commit | 059f186db67852ac17de78dab1987aab77dd4bdb (patch) | |
| tree | c3b8ca1107560023fb15536e9c0b1f173b6885bf /src/Util | |
| parent | 226b85c55a11e57b2b42edfb83c0b39136ed9128 (diff) | |
Compatibility after Coq PR#262 (continued).
This is a second instance of incompatibility induced by PR#262 (see
251ea49a). One fixes it the same, reducing the search space for a
return clause by forbidding it to be obtained by small inversion.
Diffstat (limited to 'src/Util')
0 files changed, 0 insertions, 0 deletions