diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-06-01 14:36:09 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2018-02-20 19:12:35 -0500 |
| commit | 2fb9e915a8095701c3758cba0d6238b4db8212fa (patch) | |
| tree | aa5c194f2cc9b0502186a738deafbfbfd070aef5 /theories | |
| parent | db77b92f7cc426aa9fb784be3b07b4097d81ae0d (diff) | |
Update SearchPattern.out for numeral notations
There is more churn than there should be because SearchPattern uses a
non-local sorting algorithm; the comparison function considers many
constants equal in priority and leaves it up to the heap structure to
break ties, which seems wrong. This has been reported as
[bug #5573](https://coq.inria.fr/bugs/show_bug.cgi?id=5573).
Diffstat (limited to 'theories')
0 files changed, 0 insertions, 0 deletions