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 | |
| 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).
| -rw-r--r-- | test-suite/output/SearchPattern.out | 43 |
1 files changed, 26 insertions, 17 deletions
diff --git a/test-suite/output/SearchPattern.out b/test-suite/output/SearchPattern.out index 45ff5e73b..b0ac9ea29 100644 --- a/test-suite/output/SearchPattern.out +++ b/test-suite/output/SearchPattern.out @@ -12,32 +12,37 @@ Nat.ltb: nat -> nat -> bool Nat.testbit: nat -> nat -> bool Nat.eqb: nat -> nat -> bool Nat.two: nat -Nat.zero: nat Nat.one: nat +Nat.zero: nat O: nat -Nat.double: nat -> nat -Nat.sqrt: nat -> nat Nat.div2: nat -> nat Nat.log2: nat -> nat +Nat.succ: nat -> nat +Nat.sqrt: nat -> nat Nat.pred: nat -> nat +Nat.double: nat -> nat Nat.square: nat -> nat S: nat -> nat -Nat.succ: nat -> nat Nat.ldiff: nat -> nat -> nat -Nat.add: nat -> nat -> nat -Nat.lor: nat -> nat -> nat -Nat.lxor: nat -> nat -> nat +Nat.tail_add: nat -> nat -> nat Nat.land: nat -> nat -> nat -Nat.mul: nat -> nat -> nat -Nat.sub: nat -> nat -> nat -Nat.max: nat -> nat -> nat +Nat.tail_mul: nat -> nat -> nat Nat.div: nat -> nat -> nat -Nat.pow: nat -> nat -> nat -Nat.min: nat -> nat -> nat -Nat.modulo: nat -> nat -> nat +Nat.lor: nat -> nat -> nat Nat.gcd: nat -> nat -> nat -Nat.sqrt_iter: nat -> nat -> nat -> nat -> nat +Nat.modulo: nat -> nat -> nat +Nat.max: nat -> nat -> nat +Nat.sub: nat -> nat -> nat +Nat.mul: nat -> nat -> nat +Nat.lxor: nat -> nat -> nat +Nat.add: nat -> nat -> nat +Nat.min: nat -> nat -> nat +Nat.pow: nat -> nat -> nat +Nat.of_uint: Decimal.uint -> nat +Nat.tail_addmul: nat -> nat -> nat -> nat +Nat.of_uint_acc: Decimal.uint -> nat -> nat Nat.log2_iter: nat -> nat -> nat -> nat -> nat +Nat.sqrt_iter: nat -> nat -> nat -> nat -> nat length: forall A : Type, list A -> nat Nat.bitwise: (bool -> bool -> bool) -> nat -> nat -> nat -> nat Nat.div2: nat -> nat @@ -53,14 +58,18 @@ Nat.pow: nat -> nat -> nat Nat.land: nat -> nat -> nat Nat.lxor: nat -> nat -> nat Nat.div: nat -> nat -> nat -Nat.mul: nat -> nat -> nat -Nat.min: nat -> nat -> nat +Nat.lor: nat -> nat -> nat +Nat.tail_mul: nat -> nat -> nat Nat.modulo: nat -> nat -> nat Nat.sub: nat -> nat -> nat -Nat.lor: nat -> nat -> nat +Nat.mul: nat -> nat -> nat Nat.gcd: nat -> nat -> nat Nat.max: nat -> nat -> nat +Nat.tail_add: nat -> nat -> nat Nat.add: nat -> nat -> nat +Nat.min: nat -> nat -> nat +Nat.tail_addmul: nat -> nat -> nat -> nat +Nat.of_uint_acc: Decimal.uint -> nat -> nat Nat.log2_iter: nat -> nat -> nat -> nat -> nat Nat.sqrt_iter: nat -> nat -> nat -> nat -> nat Nat.bitwise: (bool -> bool -> bool) -> nat -> nat -> nat -> nat |