Test-suite: output of Search

Fix the ordering of the results in the output of Search to correspond
to the "priority" ordering.

3 files changed, 120 insertions, 120 deletions

diff --git a/test-suite/output/Search.out b/test-suite/output/Search.out
index c17b285bc..81fda176e 100644
--- a/test-suite/output/Search.out
+++ b/test-suite/output/Search.out
@@ -1,108 +1,108 @@
 le_n: forall n : nat, n <= n
+le_0_n: forall n : nat, 0 <= n
 le_S: forall n m : nat, n <= m -> n <= S m
+le_n_S: forall n m : nat, n <= m -> S n <= S m
+le_pred: forall n m : nat, n <= m -> Nat.pred n <= Nat.pred m
+le_S_n: forall n m : nat, S n <= S m -> n <= m
+min_l: forall n m : nat, n <= m -> Nat.min n m = n
+max_r: forall n m : nat, n <= m -> Nat.max n m = m
+min_r: forall n m : nat, m <= n -> Nat.min n m = m
+max_l: forall n m : nat, m <= n -> Nat.max n m = n
 le_ind:
   forall (n : nat) (P : nat -> Prop),
   P n ->
   (forall m : nat, n <= m -> P m -> P (S m)) ->
   forall n0 : nat, n <= n0 -> P n0
-le_pred: forall n m : nat, n <= m -> Nat.pred n <= Nat.pred m
-le_S_n: forall n m : nat, S n <= S m -> n <= m
-le_0_n: forall n : nat, 0 <= n
-le_n_S: forall n m : nat, n <= m -> S n <= S m
-max_l: forall n m : nat, m <= n -> Nat.max n m = n
-max_r: forall n m : nat, n <= m -> Nat.max n m = m
-min_l: forall n m : nat, n <= m -> Nat.min n m = n
-min_r: forall n m : nat, m <= n -> Nat.min n m = m
-true: bool
 false: bool
-bool_rect: forall P : bool -> Type, P true -> P false -> forall b : bool, P b
-bool_ind: forall P : bool -> Prop, P true -> P false -> forall b : bool, P b
-bool_rec: forall P : bool -> Set, P true -> P false -> forall b : bool, P b
-andb: bool -> bool -> bool
-orb: bool -> bool -> bool
-implb: bool -> bool -> bool
-xorb: bool -> bool -> bool
+true: bool
+is_true: bool -> Prop
 negb: bool -> bool
-andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true
-andb_true_intro:
-  forall b1 b2 : bool, b1 = true /\ b2 = true -> (b1 && b2)%bool = true
 eq_true: bool -> Prop
-eq_true_rect:
-  forall P : bool -> Type, P true -> forall b : bool, eq_true b -> P b
-eq_true_ind:
-  forall P : bool -> Prop, P true -> forall b : bool, eq_true b -> P b
+implb: bool -> bool -> bool
+orb: bool -> bool -> bool
+andb: bool -> bool -> bool
+xorb: bool -> bool -> bool
+Nat.even: nat -> bool
+Nat.odd: nat -> bool
+BoolSpec: Prop -> Prop -> bool -> Prop
+Nat.eqb: nat -> nat -> bool
+Nat.testbit: nat -> nat -> bool
+Nat.ltb: nat -> nat -> bool
+Nat.leb: nat -> nat -> bool
+Nat.bitwise: (bool -> bool -> bool) -> nat -> nat -> nat -> nat
+bool_ind: forall P : bool -> Prop, P true -> P false -> forall b : bool, P b
+bool_rec: forall P : bool -> Set, P true -> P false -> forall b : bool, P b
 eq_true_rec:
   forall P : bool -> Set, P true -> forall b : bool, eq_true b -> P b
-is_true: bool -> Prop
-eq_true_ind_r:
-  forall (P : bool -> Prop) (b : bool), P b -> eq_true b -> P true
-eq_true_rec_r:
-  forall (P : bool -> Set) (b : bool), P b -> eq_true b -> P true
+eq_true_ind:
+  forall P : bool -> Prop, P true -> forall b : bool, eq_true b -> P b
 eq_true_rect_r:
   forall (P : bool -> Type) (b : bool), P b -> eq_true b -> P true
-BoolSpec: Prop -> Prop -> bool -> Prop
+eq_true_rec_r:
+  forall (P : bool -> Set) (b : bool), P b -> eq_true b -> P true
+eq_true_rect:
+  forall P : bool -> Type, P true -> forall b : bool, eq_true b -> P b
+bool_rect: forall P : bool -> Type, P true -> P false -> forall b : bool, P b
+eq_true_ind_r:
+  forall (P : bool -> Prop) (b : bool), P b -> eq_true b -> P true
+andb_true_intro:
+  forall b1 b2 : bool, b1 = true /\ b2 = true -> (b1 && b2)%bool = true
+andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true
 BoolSpec_ind:
   forall (P Q : Prop) (P0 : bool -> Prop),
   (P -> P0 true) ->
   (Q -> P0 false) -> forall b : bool, BoolSpec P Q b -> P0 b
-Nat.eqb: nat -> nat -> bool
-Nat.leb: nat -> nat -> bool
-Nat.ltb: nat -> nat -> bool
-Nat.even: nat -> bool
-Nat.odd: nat -> bool
-Nat.testbit: nat -> nat -> bool
-Nat.bitwise: (bool -> bool -> bool) -> nat -> nat -> nat -> nat
 bool_choice:
   forall (S : Set) (R1 R2 : S -> Prop),
   (forall x : S, {R1 x} + {R2 x}) ->
   {f : S -> bool | forall x : S, f x = true /\ R1 x \/ f x = false /\ R2 x}
-eq_S: forall x y : nat, x = y -> S x = S y
-f_equal_nat: forall (B : Type) (f : nat -> B) (x y : nat), x = y -> f x = f y
-f_equal_pred: forall x y : nat, x = y -> Nat.pred x = Nat.pred y
+mult_n_O: forall n : nat, 0 = n * 0
+plus_O_n: forall n : nat, 0 + n = n
+plus_n_O: forall n : nat, n = n + 0
+n_Sn: forall n : nat, n <> S n
 pred_Sn: forall n : nat, n = Nat.pred (S n)
+O_S: forall n : nat, 0 <> S n
+f_equal_pred: forall x y : nat, x = y -> Nat.pred x = Nat.pred y
+eq_S: forall x y : nat, x = y -> S x = S y
 eq_add_S: forall n m : nat, S n = S m -> n = m
+min_r: forall n m : nat, m <= n -> Nat.min n m = m
+min_l: forall n m : nat, n <= m -> Nat.min n m = n
+max_r: forall n m : nat, n <= m -> Nat.max n m = m
+max_l: forall n m : nat, m <= n -> Nat.max n m = n
+plus_Sn_m: forall n m : nat, S n + m = S (n + m)
+plus_n_Sm: forall n m : nat, S (n + m) = n + S m
+f_equal_nat: forall (B : Type) (f : nat -> B) (x y : nat), x = y -> f x = f y
 not_eq_S: forall n m : nat, n <> m -> S n <> S m
-O_S: forall n : nat, 0 <> S n
-n_Sn: forall n : nat, n <> S n
+mult_n_Sm: forall n m : nat, n * m + n = n * S m
 f_equal2_plus:
   forall x1 y1 x2 y2 : nat, x1 = y1 -> x2 = y2 -> x1 + x2 = y1 + y2
+f_equal2_mult:
+  forall x1 y1 x2 y2 : nat, x1 = y1 -> x2 = y2 -> x1 * x2 = y1 * y2
 f_equal2_nat:
   forall (B : Type) (f : nat -> nat -> B) (x1 y1 x2 y2 : nat),
   x1 = y1 -> x2 = y2 -> f x1 x2 = f y1 y2
-plus_n_O: forall n : nat, n = n + 0
-plus_O_n: forall n : nat, 0 + n = n
-plus_n_Sm: forall n m : nat, S (n + m) = n + S m
-plus_Sn_m: forall n m : nat, S n + m = S (n + m)
-f_equal2_mult:
-  forall x1 y1 x2 y2 : nat, x1 = y1 -> x2 = y2 -> x1 * x2 = y1 * y2
-mult_n_O: forall n : nat, 0 = n * 0
-mult_n_Sm: forall n m : nat, n * m + n = n * S m
-max_l: forall n m : nat, m <= n -> Nat.max n m = n
-max_r: forall n m : nat, n <= m -> Nat.max n m = m
-min_l: forall n m : nat, n <= m -> Nat.min n m = n
-min_r: forall n m : nat, m <= n -> Nat.min n m = m
-andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true
 andb_true_intro:
   forall b1 b2 : bool, b1 = true /\ b2 = true -> (b1 && b2)%bool = true
+andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true
 bool_choice:
   forall (S : Set) (R1 R2 : S -> Prop),
   (forall x : S, {R1 x} + {R2 x}) ->
   {f : S -> bool | forall x : S, f x = true /\ R1 x \/ f x = false /\ R2 x}
-andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true
 andb_true_intro:
   forall b1 b2 : bool, b1 = true /\ b2 = true -> (b1 && b2)%bool = true
 andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true
-h': newdef n <> n
+andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true
 h: n <> newdef n
 h': newdef n <> n
 h: n <> newdef n
+h': newdef n <> n
 h: n <> newdef n
 h: n <> newdef n
-h': ~ P n
 h: P n
 h': ~ P n
 h: P n
 h': ~ P n
 h: P n
+h': ~ P n
 h: P n
 h: P n
diff --git a/test-suite/output/SearchHead.out b/test-suite/output/SearchHead.out
index 0d5924ec6..7038eac22 100644
--- a/test-suite/output/SearchHead.out
+++ b/test-suite/output/SearchHead.out
@@ -1,39 +1,39 @@
 le_n: forall n : nat, n <= n
+le_0_n: forall n : nat, 0 <= n
 le_S: forall n m : nat, n <= m -> n <= S m
 le_pred: forall n m : nat, n <= m -> Nat.pred n <= Nat.pred m
-le_S_n: forall n m : nat, S n <= S m -> n <= m
-le_0_n: forall n : nat, 0 <= n
 le_n_S: forall n m : nat, n <= m -> S n <= S m
-true: bool
+le_S_n: forall n m : nat, S n <= S m -> n <= m
 false: bool
-andb: bool -> bool -> bool
-orb: bool -> bool -> bool
+true: bool
+negb: bool -> bool
 implb: bool -> bool -> bool
+orb: bool -> bool -> bool
+andb: bool -> bool -> bool
 xorb: bool -> bool -> bool
-negb: bool -> bool
-Nat.eqb: nat -> nat -> bool
-Nat.leb: nat -> nat -> bool
-Nat.ltb: nat -> nat -> bool
 Nat.even: nat -> bool
 Nat.odd: nat -> bool
+Nat.leb: nat -> nat -> bool
+Nat.ltb: nat -> nat -> bool
 Nat.testbit: nat -> nat -> bool
-eq_S: forall x y : nat, x = y -> S x = S y
-f_equal_pred: forall x y : nat, x = y -> Nat.pred x = Nat.pred y
+Nat.eqb: nat -> nat -> bool
+mult_n_O: forall n : nat, 0 = n * 0
+plus_O_n: forall n : nat, 0 + n = n
+plus_n_O: forall n : nat, n = n + 0
 pred_Sn: forall n : nat, n = Nat.pred (S n)
+f_equal_pred: forall x y : nat, x = y -> Nat.pred x = Nat.pred y
 eq_add_S: forall n m : nat, S n = S m -> n = m
-f_equal2_plus:
-  forall x1 y1 x2 y2 : nat, x1 = y1 -> x2 = y2 -> x1 + x2 = y1 + y2
-plus_n_O: forall n : nat, n = n + 0
-plus_O_n: forall n : nat, 0 + n = n
+eq_S: forall x y : nat, x = y -> S x = S y
+max_r: forall n m : nat, n <= m -> Nat.max n m = m
+max_l: forall n m : nat, m <= n -> Nat.max n m = n
+min_r: forall n m : nat, m <= n -> Nat.min n m = m
+min_l: forall n m : nat, n <= m -> Nat.min n m = n
 plus_n_Sm: forall n m : nat, S (n + m) = n + S m
 plus_Sn_m: forall n m : nat, S n + m = S (n + m)
+mult_n_Sm: forall n m : nat, n * m + n = n * S m
+f_equal2_plus:
+  forall x1 y1 x2 y2 : nat, x1 = y1 -> x2 = y2 -> x1 + x2 = y1 + y2
 f_equal2_mult:
   forall x1 y1 x2 y2 : nat, x1 = y1 -> x2 = y2 -> x1 * x2 = y1 * y2
-mult_n_O: forall n : nat, 0 = n * 0
-mult_n_Sm: forall n m : nat, n * m + n = n * S m
-max_l: forall n m : nat, m <= n -> Nat.max n m = n
-max_r: forall n m : nat, n <= m -> Nat.max n m = m
-min_l: forall n m : nat, n <= m -> Nat.min n m = n
-min_r: forall n m : nat, m <= n -> Nat.min n m = m
 h: newdef n
 h: P n
diff --git a/test-suite/output/SearchPattern.out b/test-suite/output/SearchPattern.out
index f3c12effc..45ff5e73b 100644
--- a/test-suite/output/SearchPattern.out
+++ b/test-suite/output/SearchPattern.out
@@ -1,77 +1,77 @@
-true: bool
 false: bool
-andb: bool -> bool -> bool
-orb: bool -> bool -> bool
+true: bool
+negb: bool -> bool
 implb: bool -> bool -> bool
+orb: bool -> bool -> bool
+andb: bool -> bool -> bool
 xorb: bool -> bool -> bool
-negb: bool -> bool
-Nat.eqb: nat -> nat -> bool
-Nat.leb: nat -> nat -> bool
-Nat.ltb: nat -> nat -> bool
 Nat.even: nat -> bool
 Nat.odd: nat -> bool
+Nat.leb: nat -> nat -> bool
+Nat.ltb: nat -> nat -> bool
 Nat.testbit: nat -> nat -> bool
-O: nat
-S: nat -> nat
-length: forall A : Type, list A -> nat
+Nat.eqb: nat -> nat -> bool
+Nat.two: nat
 Nat.zero: nat
 Nat.one: nat
-Nat.two: nat
-Nat.succ: nat -> nat
+O: nat
+Nat.double: nat -> nat
+Nat.sqrt: nat -> nat
+Nat.div2: nat -> nat
+Nat.log2: nat -> nat
 Nat.pred: nat -> nat
+Nat.square: nat -> nat
+S: nat -> nat
+Nat.succ: nat -> nat
+Nat.ldiff: nat -> nat -> nat
 Nat.add: nat -> nat -> nat
-Nat.double: nat -> nat
+Nat.lor: nat -> nat -> nat
+Nat.lxor: nat -> nat -> nat
+Nat.land: nat -> nat -> nat
 Nat.mul: nat -> nat -> nat
 Nat.sub: nat -> nat -> nat
 Nat.max: nat -> nat -> nat
-Nat.min: nat -> nat -> nat
-Nat.pow: nat -> nat -> nat
 Nat.div: nat -> nat -> nat
+Nat.pow: nat -> nat -> nat
+Nat.min: nat -> nat -> nat
 Nat.modulo: nat -> nat -> nat
 Nat.gcd: nat -> nat -> nat
-Nat.square: nat -> nat
 Nat.sqrt_iter: nat -> nat -> nat -> nat -> nat
-Nat.sqrt: nat -> nat
 Nat.log2_iter: nat -> nat -> nat -> nat -> nat
-Nat.log2: nat -> nat
-Nat.div2: nat -> nat
+length: forall A : Type, list A -> nat
 Nat.bitwise: (bool -> bool -> bool) -> nat -> nat -> nat -> nat
-Nat.land: nat -> nat -> nat
-Nat.lor: nat -> nat -> nat
+Nat.div2: nat -> nat
+Nat.sqrt: nat -> nat
+Nat.log2: nat -> nat
+Nat.double: nat -> nat
+Nat.pred: nat -> nat
+Nat.square: nat -> nat
+Nat.succ: nat -> nat
+S: nat -> nat
 Nat.ldiff: nat -> nat -> nat
+Nat.pow: nat -> nat -> nat
+Nat.land: nat -> nat -> nat
 Nat.lxor: nat -> nat -> nat
-S: nat -> nat
-Nat.succ: nat -> nat
-Nat.pred: nat -> nat
-Nat.add: nat -> nat -> nat
-Nat.double: nat -> nat
+Nat.div: nat -> nat -> nat
 Nat.mul: nat -> nat -> nat
-Nat.sub: nat -> nat -> nat
-Nat.max: nat -> nat -> nat
 Nat.min: nat -> nat -> nat
-Nat.pow: nat -> nat -> nat
-Nat.div: nat -> nat -> nat
 Nat.modulo: nat -> nat -> nat
+Nat.sub: nat -> nat -> nat
+Nat.lor: nat -> nat -> nat
 Nat.gcd: nat -> nat -> nat
-Nat.square: nat -> nat
-Nat.sqrt_iter: nat -> nat -> nat -> nat -> nat
-Nat.sqrt: nat -> nat
+Nat.max: nat -> nat -> nat
+Nat.add: nat -> nat -> nat
 Nat.log2_iter: nat -> nat -> nat -> nat -> nat
-Nat.log2: nat -> nat
-Nat.div2: nat -> nat
+Nat.sqrt_iter: nat -> nat -> nat -> nat -> nat
 Nat.bitwise: (bool -> bool -> bool) -> nat -> nat -> nat -> nat
-Nat.land: nat -> nat -> nat
-Nat.lor: nat -> nat -> nat
-Nat.ldiff: nat -> nat -> nat
-Nat.lxor: nat -> nat -> nat
 mult_n_Sm: forall n m : nat, n * m + n = n * S m
-identity_refl: forall (A : Type) (a : A), identity a a
 iff_refl: forall A : Prop, A <-> A
+le_n: forall n : nat, n <= n
+identity_refl: forall (A : Type) (a : A), identity a a
 eq_refl: forall (A : Type) (x : A), x = x
 Nat.divmod: nat -> nat -> nat -> nat -> nat * nat
-le_n: forall n : nat, n <= n
-pair: forall A B : Type, A -> B -> A * B
 conj: forall A B : Prop, A -> B -> A /\ B
+pair: forall A B : Type, A -> B -> A * B
 Nat.divmod: nat -> nat -> nat -> nat -> nat * nat
 h: n <> newdef n
 h: n <> newdef n