diff options
Diffstat (limited to 'test-suite/output')
25 files changed, 332 insertions, 59 deletions
diff --git a/test-suite/output/Arguments.out b/test-suite/output/Arguments.out index f889da4e98..8cf0797b17 100644 --- a/test-suite/output/Arguments.out +++ b/test-suite/output/Arguments.out @@ -39,7 +39,7 @@ The reduction tactics unfold Nat.sub when the 1st and Nat.sub is transparent Expands to: Constant Coq.Init.Nat.sub pf : -forall D1 C1 : Type, +forall {D1 C1 : Type}, (D1 -> C1) -> forall D2 C2 : Type, (D2 -> C2) -> D1 * D2 -> C1 * C2 pf is not universe polymorphic @@ -47,7 +47,7 @@ Arguments pf {D1}%foo_scope {C1}%type_scope _ [D2 C2] : simpl never The reduction tactics never unfold pf pf is transparent Expands to: Constant Arguments.pf -fcomp : forall A B C : Type, (B -> C) -> (A -> B) -> A -> C +fcomp : forall {A B C : Type}, (B -> C) -> (A -> B) -> A -> C fcomp is not universe polymorphic Arguments fcomp {A B C}%type_scope _ _ _ / @@ -75,7 +75,7 @@ The reduction tactics unfold f when the 3rd, 4th and 5th arguments evaluate to a constructor f is transparent Expands to: Constant Arguments.S1.S2.f -f : forall T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat +f : forall [T2 : Type], T1 -> T2 -> nat -> unit -> nat -> nat f is not universe polymorphic Arguments f [T2]%type_scope _ _ !_%nat_scope !_ !_%nat_scope @@ -83,7 +83,7 @@ The reduction tactics unfold f when the 4th, 5th and 6th arguments evaluate to a constructor f is transparent Expands to: Constant Arguments.S1.f -f : forall T1 T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat +f : forall [T1 T2 : Type], T1 -> T2 -> nat -> unit -> nat -> nat f is not universe polymorphic Arguments f [T1 T2]%type_scope _ _ !_%nat_scope !_ !_%nat_scope diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out index 26ebd8efc3..abc7f0f88e 100644 --- a/test-suite/output/Arguments_renaming.out +++ b/test-suite/output/Arguments_renaming.out @@ -15,7 +15,7 @@ Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x Arguments eq {A}%type_scope Arguments eq_refl {B}%type_scope {y}, [B] _ -eq_refl : forall (A : Type) (x : A), x = x +eq_refl : forall {A : Type} {x : A}, x = x eq_refl is not universe polymorphic Arguments eq_refl {B}%type_scope {y}, [B] _ @@ -24,7 +24,7 @@ Inductive myEq (B : Type) (x : A) : A -> Prop := myrefl : B -> myEq B x x Arguments myEq _%type_scope Arguments myrefl {C}%type_scope x : rename -myrefl : forall (B : Type) (x : A), B -> myEq B x x +myrefl : forall {B : Type} (x : A), B -> myEq B x x myrefl is not universe polymorphic Arguments myrefl {C}%type_scope x : rename @@ -38,7 +38,7 @@ fix myplus (T : Type) (t : T) (n m : nat) {struct n} : nat := : forall T : Type, T -> nat -> nat -> nat Arguments myplus {Z}%type_scope !t (!n m)%nat_scope : rename -myplus : forall T : Type, T -> nat -> nat -> nat +myplus : forall {T : Type}, T -> nat -> nat -> nat myplus is not universe polymorphic Arguments myplus {Z}%type_scope !t (!n m)%nat_scope : rename @@ -53,7 +53,7 @@ Inductive myEq (A B : Type) (x : A) : A -> Prop := Arguments myEq (_ _)%type_scope Arguments myrefl A%type_scope {C}%type_scope x : rename -myrefl : forall (A B : Type) (x : A), B -> myEq A B x x +myrefl : forall (A : Type) {B : Type} (x : A), B -> myEq A B x x myrefl is not universe polymorphic Arguments myrefl A%type_scope {C}%type_scope x : rename @@ -69,7 +69,7 @@ fix myplus (T : Type) (t : T) (n m : nat) {struct n} : nat := : forall T : Type, T -> nat -> nat -> nat Arguments myplus {Z}%type_scope !t (!n m)%nat_scope : rename -myplus : forall T : Type, T -> nat -> nat -> nat +myplus : forall {T : Type}, T -> nat -> nat -> nat myplus is not universe polymorphic Arguments myplus {Z}%type_scope !t (!n m)%nat_scope : rename diff --git a/test-suite/output/FloatExtraction.out b/test-suite/output/FloatExtraction.out index cfd6633752..dd8189c56f 100644 --- a/test-suite/output/FloatExtraction.out +++ b/test-suite/output/FloatExtraction.out @@ -1,3 +1,17 @@ +File "stdin", line 25, characters 8-12: +Warning: The constant 0.01 is not a binary64 floating-point value. A closest +value will be used and unambiguously printed 0.01. [inexact-float,parsing] +File "stdin", line 25, characters 20-25: +Warning: The constant -0.01 is not a binary64 floating-point value. A closest +value will be used and unambiguously printed -0.01. [inexact-float,parsing] +File "stdin", line 25, characters 27-35: +Warning: The constant 1.7e+308 is not a binary64 floating-point value. A +closest value will be used and unambiguously printed 1.6999999999999999e+308. +[inexact-float,parsing] +File "stdin", line 25, characters 37-46: +Warning: The constant -1.7e-308 is not a binary64 floating-point value. A +closest value will be used and unambiguously printed +-1.7000000000000002e-308. [inexact-float,parsing] (** val infinity : Float64.t **) diff --git a/test-suite/output/FloatExtraction.v b/test-suite/output/FloatExtraction.v index f296e8e871..7ff8958c0f 100644 --- a/test-suite/output/FloatExtraction.v +++ b/test-suite/output/FloatExtraction.v @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/output/FloatSyntax.out b/test-suite/output/FloatSyntax.out index 668a55977d..7941d2e647 100644 --- a/test-suite/output/FloatSyntax.out +++ b/test-suite/output/FloatSyntax.out @@ -4,8 +4,16 @@ : float (-2.5)%float : float +File "stdin", line 9, characters 6-13: +Warning: The constant 2.5e123 is not a binary64 floating-point value. A +closest value will be used and unambiguously printed 2.4999999999999999e+123. +[inexact-float,parsing] 2.4999999999999999e+123%float : float +File "stdin", line 10, characters 7-16: +Warning: The constant -2.5e-123 is not a binary64 floating-point value. A +closest value will be used and unambiguously printed +-2.5000000000000001e-123. [inexact-float,parsing] (-2.5000000000000001e-123)%float : float (2 + 2)%float @@ -18,14 +26,34 @@ : float -2.5 : float +File "stdin", line 19, characters 6-13: +Warning: The constant 2.5e123 is not a binary64 floating-point value. A +closest value will be used and unambiguously printed 2.4999999999999999e+123. +[inexact-float,parsing] 2.4999999999999999e+123 : float +File "stdin", line 20, characters 7-16: +Warning: The constant -2.5e-123 is not a binary64 floating-point value. A +closest value will be used and unambiguously printed +-2.5000000000000001e-123. [inexact-float,parsing] -2.5000000000000001e-123 : float 2 + 2 : float 2.5 + 2.5 : float +File "stdin", line 24, characters 6-11: +Warning: The constant 1e309 is not a binary64 floating-point value. A closest +value will be used and unambiguously printed infinity. +[inexact-float,parsing] +infinity + : float +File "stdin", line 25, characters 6-12: +Warning: The constant -1e309 is not a binary64 floating-point value. A +closest value will be used and unambiguously printed neg_infinity. +[inexact-float,parsing] +neg_infinity + : float 2 : nat 2%float diff --git a/test-suite/output/FloatSyntax.v b/test-suite/output/FloatSyntax.v index 85f611352c..eca712db10 100644 --- a/test-suite/output/FloatSyntax.v +++ b/test-suite/output/FloatSyntax.v @@ -21,6 +21,9 @@ Check (-2.5e-123). Check (2 + 2). Check (2.5 + 2.5). +Check 1e309. +Check -1e309. + Open Scope nat_scope. Check 2. diff --git a/test-suite/output/Inductive.out b/test-suite/output/Inductive.out index ff2556c5dc..e6c2806433 100644 --- a/test-suite/output/Inductive.out +++ b/test-suite/output/Inductive.out @@ -1,6 +1,10 @@ The command has indeed failed with message: -Last occurrence of "list'" must have "A" as 1st argument in - "A -> list' A -> list' (A * A)%type". +In environment +list' : Set -> Set +A : Set +a : A +l : list' A +Unable to unify "list' (A * A)%type" with "list' A". Inductive foo (A : Type) (x : A) (y : A := x) : Prop := Foo : foo A x Arguments foo _%type_scope diff --git a/test-suite/output/MExtraction.v b/test-suite/output/MExtraction.v index 357afb51eb..22268daa83 100644 --- a/test-suite/output/MExtraction.v +++ b/test-suite/output/MExtraction.v @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/output/NoAxiomFromR.v b/test-suite/output/NoAxiomFromR.v index 9cf6879699..7abbe29452 100644 --- a/test-suite/output/NoAxiomFromR.v +++ b/test-suite/output/NoAxiomFromR.v @@ -5,6 +5,6 @@ Inductive TT : Set := Lemma lem4 : forall (n m : nat), S m <= m -> C (S m) <> C n -> False. -Proof. firstorder. Qed. +Proof. firstorder lia. Qed. Print Assumptions lem4. diff --git a/test-suite/output/NumeralNotations.out b/test-suite/output/NumeralNotations.out index 113384e9cf..060877707b 100644 --- a/test-suite/output/NumeralNotations.out +++ b/test-suite/output/NumeralNotations.out @@ -218,3 +218,19 @@ let v : ty := Build_ty Set set in v : ty : ty let v : ty := Build_ty Type type in v : ty : ty +1 + : nat +(-1000)%Z + : Z +0 + : Prop ++0 + : bool +-0 + : bool +00 + : nat * nat +1000 + : Prop +1_000 + : list nat diff --git a/test-suite/output/NumeralNotations.v b/test-suite/output/NumeralNotations.v index 22aff36d67..47e1b127cb 100644 --- a/test-suite/output/NumeralNotations.v +++ b/test-suite/output/NumeralNotations.v @@ -457,3 +457,33 @@ Module Test20. Check let v := 4%kt in v : ty. Check let v := 5%kt in v : ty. End Test20. + +Module Test21. + + Check 00001. + Check (-1_000)%Z. + +End Test21. + +Module Test22. + +Notation "0" := False. +Notation "+0" := true. +Notation "-0" := false. +Notation "00" := (0%nat, 0%nat). +Check 0. +Check +0. +Check -0. +Check 00. + +Notation "1000" := True. +Notation "1_000" := (cons 1 nil). +Check 1000. +Check 1_000. + +(* To do: preserve parsing of -0: +Require Import ZArith. +Check (-0)%Z. +*) + +End Test22. diff --git a/test-suite/output/PatternsInBinders.out b/test-suite/output/PatternsInBinders.out index 4f09f00c56..bdfa8afb6a 100644 --- a/test-suite/output/PatternsInBinders.out +++ b/test-suite/output/PatternsInBinders.out @@ -4,7 +4,7 @@ fun '(x, y) => (y, x) : A * B -> B * A forall '(x, y), swap (x, y) = (y, x) : Prop -proj_informative = fun '(exist _ x _) => x : A +proj_informative = fun '(exist _ x _) => x : {x : A | P x} -> A foo = fun '(Bar n b tt p) => if b then n + p else n - p : Foo -> nat @@ -29,8 +29,7 @@ exists '(x, y) '(z, w), swap (x, y) = (z, w) ∀ '(x, y), swap (x, y) = (y, x) : Prop both_z = -fun pat : nat * nat => -let '(n, p) as x := pat return (F x) in (Z n, Z p) : F (n, p) +fun pat : nat * nat => let '(n, p) as x := pat return (F x) in (Z n, Z p) : forall pat : nat * nat, F pat fun '(x, y) '(z, t) => swap (x, y) = (z, t) : A * B -> B * A -> Prop diff --git a/test-suite/output/PrintInfos.out b/test-suite/output/PrintInfos.out index 71d162c314..8fb267e343 100644 --- a/test-suite/output/PrintInfos.out +++ b/test-suite/output/PrintInfos.out @@ -1,4 +1,4 @@ -existT : forall (A : Type) (P : A -> Type) (x : A), P x -> {x : A & P x} +existT : forall [A : Type] (P : A -> Type) (x : A), P x -> {x : A & P x} existT is template universe polymorphic on sigT.u0 sigT.u1 Arguments existT [A]%type_scope _%function_scope @@ -8,19 +8,19 @@ Inductive sigT (A : Type) (P : A -> Type) : Type := Arguments sigT [A]%type_scope _%type_scope Arguments existT [A]%type_scope _%function_scope -existT : forall (A : Type) (P : A -> Type) (x : A), P x -> {x : A & P x} +existT : forall [A : Type] (P : A -> Type) (x : A), P x -> {x : A & P x} Argument A is implicit Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x Arguments eq {A}%type_scope Arguments eq_refl {A}%type_scope {x}, [A] _ -eq_refl : forall (A : Type) (x : A), x = x +eq_refl : forall {A : Type} {x : A}, x = x eq_refl is not universe polymorphic Arguments eq_refl {A}%type_scope {x}, [A] _ Expands to: Constructor Coq.Init.Logic.eq_refl -eq_refl : forall (A : Type) (x : A), x = x +eq_refl : forall {A : Type} {x : A}, x = x When applied to no arguments: Arguments A, x are implicit and maximally inserted @@ -65,14 +65,14 @@ bar : foo bar is not universe polymorphic Expanded type for implicit arguments -bar : forall x : nat, x = 0 +bar : forall {x : nat}, x = 0 Arguments bar {x} Expands to: Constant PrintInfos.bar *** [ bar : foo ] Expanded type for implicit arguments -bar : forall x : nat, x = 0 +bar : forall {x : nat}, x = 0 Arguments bar {x} Module Coq.Init.Peano diff --git a/test-suite/output/QArithSyntax.out b/test-suite/output/QArithSyntax.out index 6bc04f1cef..fe6a1d25c6 100644 --- a/test-suite/output/QArithSyntax.out +++ b/test-suite/output/QArithSyntax.out @@ -1,14 +1,14 @@ -eq_refl : 102e-2 = 102e-2 - : 102e-2 = 102e-2 -eq_refl : 102e-1 = 102e-1 - : 102e-1 = 102e-1 +eq_refl : 1.02 = 1.02 + : 1.02 = 1.02 +eq_refl : 10.2 = 10.2 + : 10.2 = 10.2 eq_refl : 1020 = 1020 : 1020 = 1020 eq_refl : 102 = 102 : 102 = 102 -eq_refl : 102e-2 = 102e-2 - : 102e-2 = 102e-2 +eq_refl : 1.02 = 1.02 + : 1.02 = 1.02 eq_refl : -1e-4 = -1e-4 : -1e-4 = -1e-4 -eq_refl : -50e-2 = -50e-2 - : -50e-2 = -50e-2 +eq_refl : -0.50 = -0.50 + : -0.50 = -0.50 diff --git a/test-suite/output/RealSyntax.out b/test-suite/output/RealSyntax.out index 2b14ca7069..1685964b0f 100644 --- a/test-suite/output/RealSyntax.out +++ b/test-suite/output/RealSyntax.out @@ -2,19 +2,21 @@ : R (-31)%R : R -15e-1%R +1.5%R : R -eq_refl : 102e-2 = 102e-2 - : 102e-2 = 102e-2 -eq_refl : 102e-1 = 102e-1 - : 102e-1 = 102e-1 +15%R + : R +eq_refl : 1.02 = 1.02 + : 1.02 = 1.02 +eq_refl : 10.2 = 10.2 + : 10.2 = 10.2 eq_refl : 102e1 = 102e1 : 102e1 = 102e1 eq_refl : 102 = 102 : 102 = 102 -eq_refl : 102e-2 = 102e-2 - : 102e-2 = 102e-2 +eq_refl : 1.02 = 1.02 + : 1.02 = 1.02 eq_refl : -1e-4 = -1e-4 : -1e-4 = -1e-4 -eq_refl : -50e-2 = -50e-2 - : -50e-2 = -50e-2 +eq_refl : -0.50 = -0.50 + : -0.50 = -0.50 diff --git a/test-suite/output/RealSyntax.v b/test-suite/output/RealSyntax.v index 7be8b18ac8..e5f9d06316 100644 --- a/test-suite/output/RealSyntax.v +++ b/test-suite/output/RealSyntax.v @@ -3,6 +3,7 @@ Check 32%R. Check (-31)%R. Check 1.5_%R. +Check 1_.5_e1_%R. Open Scope R_scope. diff --git a/test-suite/output/Search.out b/test-suite/output/Search.out index ffba1d35cc..9d8e830d64 100644 --- a/test-suite/output/Search.out +++ b/test-suite/output/Search.out @@ -18,6 +18,7 @@ le_sind: P n -> (forall m : nat, n <= m -> P m -> P (S m)) -> forall n0 : nat, n <= n0 -> P n0 +(use "About" for full details on implicit arguments) false: bool true: bool eq_true: bool -> Prop @@ -37,7 +38,7 @@ Nat.leb: nat -> nat -> bool Nat.bitwise: (bool -> bool -> bool) -> nat -> nat -> nat -> nat bool_rec: forall P : bool -> Set, 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 + forall (P : bool -> Prop) [b : bool], P b -> eq_true b -> P true eq_true_rec: forall P : bool -> Set, P true -> forall b : bool, eq_true b -> P b bool_ind: forall P : bool -> Prop, P true -> P false -> forall b : bool, P b @@ -49,9 +50,9 @@ bool_rect: forall P : bool -> Type, P true -> P false -> forall b : bool, P b eq_true_ind: forall P : bool -> Prop, P true -> forall b : bool, eq_true b -> P b eq_true_rec_r: - forall (P : bool -> Set) (b : bool), P b -> eq_true b -> P true + forall (P : bool -> Set) [b : bool], P b -> eq_true b -> P true eq_true_rect_r: - forall (P : bool -> Type) (b : bool), P b -> eq_true b -> P true + forall (P : bool -> Type) [b : bool], P b -> eq_true b -> P true bool_sind: forall P : bool -> SProp, P true -> P false -> forall b : bool, P b Byte.to_bits: @@ -62,13 +63,13 @@ Byte.of_bits: Byte.byte 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 + forall [b1 b2 : bool], b1 = true /\ b2 = true -> (b1 && b2)%bool = true BoolSpec_sind: - forall (P Q : Prop) (P0 : bool -> SProp), + forall [P Q : Prop] (P0 : bool -> SProp), (P -> P0 true) -> (Q -> P0 false) -> forall b : bool, BoolSpec P Q b -> P0 b BoolSpec_ind: - forall (P Q : Prop) (P0 : bool -> Prop), + forall [P Q : Prop] (P0 : bool -> Prop), (P -> P0 true) -> (Q -> P0 false) -> forall b : bool, BoolSpec P Q b -> P0 b Byte.to_bits_of_bits: @@ -76,9 +77,10 @@ Byte.to_bits_of_bits: b : bool * (bool * (bool * (bool * (bool * (bool * (bool * bool)))))), Byte.to_bits (Byte.of_bits b) = b bool_choice: - forall (S : Set) (R1 R2 : S -> Prop), + 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} +(use "About" for full details on implicit arguments) 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 @@ -104,25 +106,35 @@ f_equal2_mult: 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 +(use "About" for full details on implicit arguments) andb_true_intro: - forall b1 b2 : bool, b1 = true /\ b2 = true -> (b1 && b2)%bool = true + 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 [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} +(use "About" for full details on implicit arguments) andb_true_intro: - forall b1 b2 : bool, b1 = true /\ b2 = true -> (b1 && b2)%bool = true + 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 +(use "About" for full details on implicit arguments) andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true +(use "About" for full details on implicit arguments) h: n <> newdef n h': newdef n <> n +(use "About" for full details on implicit arguments) h: n <> newdef n h': newdef n <> n +(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: n <> newdef n h': newdef n <> n +(use "About" for full details on implicit arguments) +(use "About" for full details on implicit arguments) The command has indeed failed with message: No such goal. The command has indeed failed with message: @@ -131,9 +143,14 @@ The command has indeed failed with message: Query commands only support the single numbered goal selector. h: P n h': ~ P n +(use "About" for full details on implicit arguments) h: P n h': ~ P n +(use "About" for full details on implicit arguments) h: P n 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) diff --git a/test-suite/output/SearchHead.out b/test-suite/output/SearchHead.out index 7038eac22c..5627e4bd3c 100644 --- a/test-suite/output/SearchHead.out +++ b/test-suite/output/SearchHead.out @@ -4,6 +4,7 @@ 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_n_S: forall n m : nat, n <= m -> S n <= S m le_S_n: forall n m : nat, S n <= S m -> n <= m +(use "About" for full details on implicit arguments) false: bool true: bool negb: bool -> bool @@ -17,6 +18,7 @@ Nat.leb: nat -> nat -> bool Nat.ltb: nat -> nat -> bool Nat.testbit: nat -> nat -> bool Nat.eqb: nat -> nat -> bool +(use "About" for full details on implicit arguments) 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 @@ -35,5 +37,8 @@ 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 +(use "About" for full details on implicit arguments) h: newdef n +(use "About" for full details on implicit arguments) h: P n +(use "About" for full details on implicit arguments) diff --git a/test-suite/output/SearchPattern.out b/test-suite/output/SearchPattern.out index 4cd0ffb1dc..36fc1a5914 100644 --- a/test-suite/output/SearchPattern.out +++ b/test-suite/output/SearchPattern.out @@ -11,6 +11,7 @@ Nat.leb: nat -> nat -> bool Nat.ltb: nat -> nat -> bool Nat.testbit: nat -> nat -> bool Nat.eqb: nat -> nat -> bool +(use "About" for full details on implicit arguments) Nat.two: nat Nat.one: nat Nat.zero: nat @@ -44,8 +45,10 @@ Nat.tail_addmul: nat -> nat -> nat -> nat Nat.of_uint_acc: Decimal.uint -> nat -> nat Nat.sqrt_iter: nat -> nat -> nat -> nat -> nat Nat.log2_iter: nat -> nat -> nat -> nat -> nat -length: forall A : Type, list A -> 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 @@ -74,18 +77,29 @@ 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 +(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 +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 -conj: forall A B : Prop, A -> B -> A /\ B -pair: forall A B : Type, A -> B -> A * B +(use "About" for full details on implicit arguments) +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) diff --git a/test-suite/output/SearchRewrite.out b/test-suite/output/SearchRewrite.out index 5edea5dff6..3c0880b20c 100644 --- a/test-suite/output/SearchRewrite.out +++ b/test-suite/output/SearchRewrite.out @@ -1,5 +1,10 @@ plus_n_O: forall n : nat, n = n + 0 +(use "About" for full details on implicit arguments) plus_O_n: forall n : nat, 0 + n = n +(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: n = newdef n +(use "About" for full details on implicit arguments) diff --git a/test-suite/output/allBytes.out b/test-suite/output/allBytes.out new file mode 100644 index 0000000000..8d188c4c45 --- /dev/null +++ b/test-suite/output/allBytes.out @@ -0,0 +1 @@ +!"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~ diff --git a/test-suite/output/allBytes.v b/test-suite/output/allBytes.v new file mode 100644 index 0000000000..01a5161ef4 --- /dev/null +++ b/test-suite/output/allBytes.v @@ -0,0 +1,121 @@ +(* Taken from bedrock2 *) + +(* Note: not an utf8 file *) + +Require Import Coq.ZArith.BinInt Coq.Lists.List. +Require Coq.Init.Byte Coq.Strings.Byte Coq.Strings.String. + +Definition allBytes: list Byte.byte := + map (fun nn => match Byte.of_N (BinNat.N.of_nat nn) with + | Some b => b + | None => Byte.x00 (* won't happen *) + end) + (seq 32 95). + +Notation "a b" := (@cons Byte.byte a b) + (only printing, right associativity, at level 3, format "a b"). + +Notation "" := (@nil Byte.byte) + (only printing, right associativity, at level 3, format ""). + +Notation " " := (Byte.x20) (only printing). +Notation "'!'" := (Byte.x21) (only printing). +Notation "'""'" := (Byte.x22) (only printing). +Notation "'#'" := (Byte.x23) (only printing). +Notation "'$'" := (Byte.x24) (only printing). +Notation "'%'" := (Byte.x25) (only printing). +Notation "'&'" := (Byte.x26) (only printing). +Notation "'''" := (Byte.x27) (only printing). +Notation "'('" := (Byte.x28) (only printing). +Notation "')'" := (Byte.x29) (only printing). +Notation "'*'" := (Byte.x2a) (only printing). +Notation "'+'" := (Byte.x2b) (only printing). +Notation "','" := (Byte.x2c) (only printing). +Notation "'-'" := (Byte.x2d) (only printing). +Notation "'.'" := (Byte.x2e) (only printing). +Notation "'/'" := (Byte.x2f) (only printing). +Notation "'0'" := (Byte.x30) (only printing). +Notation "'1'" := (Byte.x31) (only printing). +Notation "'2'" := (Byte.x32) (only printing). +Notation "'3'" := (Byte.x33) (only printing). +Notation "'4'" := (Byte.x34) (only printing). +Notation "'5'" := (Byte.x35) (only printing). +Notation "'6'" := (Byte.x36) (only printing). +Notation "'7'" := (Byte.x37) (only printing). +Notation "'8'" := (Byte.x38) (only printing). +Notation "'9'" := (Byte.x39) (only printing). +Notation "':'" := (Byte.x3a) (only printing). +Notation "';'" := (Byte.x3b) (only printing). +Notation "'<'" := (Byte.x3c) (only printing). +Notation "'='" := (Byte.x3d) (only printing). +Notation "'>'" := (Byte.x3e) (only printing). +Notation "'?'" := (Byte.x3f) (only printing). +Notation "'@'" := (Byte.x40) (only printing). +Notation "'A'" := (Byte.x41) (only printing). +Notation "'B'" := (Byte.x42) (only printing). +Notation "'C'" := (Byte.x43) (only printing). +Notation "'D'" := (Byte.x44) (only printing). +Notation "'E'" := (Byte.x45) (only printing). +Notation "'F'" := (Byte.x46) (only printing). +Notation "'G'" := (Byte.x47) (only printing). +Notation "'H'" := (Byte.x48) (only printing). +Notation "'I'" := (Byte.x49) (only printing). +Notation "'J'" := (Byte.x4a) (only printing). +Notation "'K'" := (Byte.x4b) (only printing). +Notation "'L'" := (Byte.x4c) (only printing). +Notation "'M'" := (Byte.x4d) (only printing). +Notation "'N'" := (Byte.x4e) (only printing). +Notation "'O'" := (Byte.x4f) (only printing). +Notation "'P'" := (Byte.x50) (only printing). +Notation "'Q'" := (Byte.x51) (only printing). +Notation "'R'" := (Byte.x52) (only printing). +Notation "'S'" := (Byte.x53) (only printing). +Notation "'T'" := (Byte.x54) (only printing). +Notation "'U'" := (Byte.x55) (only printing). +Notation "'V'" := (Byte.x56) (only printing). +Notation "'W'" := (Byte.x57) (only printing). +Notation "'X'" := (Byte.x58) (only printing). +Notation "'Y'" := (Byte.x59) (only printing). +Notation "'Z'" := (Byte.x5a) (only printing). +Notation "'['" := (Byte.x5b) (only printing). +Notation "'\'" := (Byte.x5c) (only printing). +Notation "']'" := (Byte.x5d) (only printing). +Notation "'^'" := (Byte.x5e) (only printing). +Notation "'_'" := (Byte.x5f) (only printing). +Notation "'`'" := (Byte.x60) (only printing). +Notation "'a'" := (Byte.x61) (only printing). +Notation "'b'" := (Byte.x62) (only printing). +Notation "'c'" := (Byte.x63) (only printing). +Notation "'d'" := (Byte.x64) (only printing). +Notation "'e'" := (Byte.x65) (only printing). +Notation "'f'" := (Byte.x66) (only printing). +Notation "'g'" := (Byte.x67) (only printing). +Notation "'h'" := (Byte.x68) (only printing). +Notation "'i'" := (Byte.x69) (only printing). +Notation "'j'" := (Byte.x6a) (only printing). +Notation "'k'" := (Byte.x6b) (only printing). +Notation "'l'" := (Byte.x6c) (only printing). +Notation "'m'" := (Byte.x6d) (only printing). +Notation "'n'" := (Byte.x6e) (only printing). +Notation "'o'" := (Byte.x6f) (only printing). +Notation "'p'" := (Byte.x70) (only printing). +Notation "'q'" := (Byte.x71) (only printing). +Notation "'r'" := (Byte.x72) (only printing). +Notation "'s'" := (Byte.x73) (only printing). +Notation "'t'" := (Byte.x74) (only printing). +Notation "'u'" := (Byte.x75) (only printing). +Notation "'v'" := (Byte.x76) (only printing). +Notation "'w'" := (Byte.x77) (only printing). +Notation "'x'" := (Byte.x78) (only printing). +Notation "'y'" := (Byte.x79) (only printing). +Notation "'z'" := (Byte.x7a) (only printing). +Notation "'{'" := (Byte.x7b) (only printing). +Notation "'|'" := (Byte.x7c) (only printing). +Notation "'}'" := (Byte.x7d) (only printing). +Notation "'~'" := (Byte.x7e) (only printing). + +Global Set Printing Width 300. + +Goal False. + let cc := eval cbv in allBytes in idtac cc. +Abort. diff --git a/test-suite/output/clear.out b/test-suite/output/clear.out new file mode 100644 index 0000000000..42e3abf26f --- /dev/null +++ b/test-suite/output/clear.out @@ -0,0 +1,5 @@ +1 subgoal + + z := 0 : nat + ============================ + True diff --git a/test-suite/output/clear.v b/test-suite/output/clear.v new file mode 100644 index 0000000000..d584cf752e --- /dev/null +++ b/test-suite/output/clear.v @@ -0,0 +1,8 @@ +Module Wish11692. + +(* Support for let-in in clear dependent *) + +Goal forall x : Prop, let z := 0 in let z' : (fun _ => True) x := I in let y := x in y -> True. +Proof. intros x z z' y H. clear dependent x. Show. exact I. Qed. + +End Wish11692. diff --git a/test-suite/output/ssr_explain_match.v b/test-suite/output/ssr_explain_match.v index 4a840fe20c..5c5a4e9e7b 100644 --- a/test-suite/output/ssr_explain_match.v +++ b/test-suite/output/ssr_explain_match.v @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) |