diff options
| author | Guillaume Melquiond | 2016-09-28 15:38:33 +0200 |
|---|---|---|
| committer | Guillaume Melquiond | 2016-09-28 15:38:47 +0200 |
| commit | 405acea72a67c31ec8554c1f76d51518a5df769a (patch) | |
| tree | 074fce4630bd752f59a32c2edeb76c0023eb6ab5 /kernel/type_errors.mli | |
| parent | 2c4f3c2bcf93d023b53a9f2ec6b151d4df696c84 (diff) | |
Remove incorrect assertion in cbn (bug #4822).
This assertion checked that two arguments in the same position were equal,
but in fact, since one might have already been reduced, they are only
convertible (which is too costly to check in an assertion).
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions