diff options
| author | Hugo Herbelin | 2020-05-11 17:41:58 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2020-05-15 18:21:58 +0200 |
| commit | 34237bb07fa8663d3d9e8ca4f9459f46841fd43d (patch) | |
| tree | bb514dfb7bd2e432264e5c7c502cfc2566df31a2 /test-suite/output/SearchPattern.out | |
| parent | 023d189aa201c8d5c71bc7de3e98725273d01b4f (diff) | |
Search: Displaying the "use About" notice only when really needed.
Diffstat (limited to 'test-suite/output/SearchPattern.out')
| -rw-r--r-- | test-suite/output/SearchPattern.out | 15 |
1 files changed, 1 insertions, 14 deletions
diff --git a/test-suite/output/SearchPattern.out b/test-suite/output/SearchPattern.out index 13d0a9e55b..80b03e8a0b 100644 --- a/test-suite/output/SearchPattern.out +++ b/test-suite/output/SearchPattern.out @@ -21,7 +21,6 @@ Hexadecimal.uint_beq: Hexadecimal.uint -> Hexadecimal.uint -> bool Decimal.decimal_beq: Decimal.decimal -> Decimal.decimal -> bool Decimal.int_beq: Decimal.int -> Decimal.int -> bool Decimal.uint_beq: Decimal.uint -> Decimal.uint -> bool -(use "About" for full details on implicit arguments) Nat.two: nat Nat.zero: nat Nat.one: nat @@ -61,8 +60,6 @@ Nat.sqrt_iter: nat -> nat -> nat -> nat -> nat Nat.log2_iter: nat -> nat -> nat -> nat -> nat length: forall [A : Type], list A -> nat Nat.bitwise: (bool -> bool -> bool) -> nat -> nat -> nat -> nat -(use "About" for full details on implicit arguments) -(use "About" for full details on implicit arguments) Nat.div2: nat -> nat Nat.sqrt: nat -> nat Nat.log2: nat -> nat @@ -92,29 +89,19 @@ Nat.of_hex_uint_acc: Hexadecimal.uint -> nat -> nat Nat.sqrt_iter: nat -> nat -> nat -> nat -> nat Nat.log2_iter: nat -> nat -> nat -> nat -> nat Nat.bitwise: (bool -> bool -> bool) -> nat -> nat -> nat -> nat -(use "About" for full details on implicit arguments) mult_n_Sm: forall n m : nat, n * m + n = n * S m -(use "About" for full details on implicit arguments) 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 -(use "About" for full details on implicit arguments) +(use "About" for full details on the implicit arguments of eq_refl) 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 -(use "About" for full details on implicit arguments) -(use "About" for full details on implicit arguments) h: n <> newdef n -(use "About" for full details on implicit arguments) h: n <> newdef n -(use "About" for full details on implicit arguments) h: P n -(use "About" for full details on implicit arguments) h': ~ P n -(use "About" for full details on implicit arguments) h: P n -(use "About" for full details on implicit arguments) h: P n -(use "About" for full details on implicit arguments) |