diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-05-13 22:00:02 +0200 |
|---|---|---|
| committer |  Jason Gross <jasongross9@gmail.com> | 2018-05-14 19:30:05 -0400 |
| commit | 251ea49a661aef7c075ace80867006183ab0cdea (patch) | |
| tree | d854e455d27d471407451752a68ed57ab9b6e8f2 /crypto-defects.md | |
| parent | 2f2941ee50099011ec0ae212e9e9dc5c5513ea9c (diff) | |
Compatibility after Coq PR#262.
Coq PR#262 makes the inference of return clauses more uniform and
general but unification is sometimes not strong enough to deal with
this generality. See #5107 for details.
One reduces the search space for a return clause by forbidding it to
be obtained by small inversion.
Diffstat (limited to 'crypto-defects.md')
0 files changed, 0 insertions, 0 deletions