diff options
Diffstat (limited to 'test-suite/output')
-rw-r--r-- | test-suite/output/Arguments.out | 17 | ||||
-rw-r--r-- | test-suite/output/ArgumentsScope.out | 14 | ||||
-rw-r--r-- | test-suite/output/Arguments_renaming.out | 23 | ||||
-rw-r--r-- | test-suite/output/Cases.out | 9 | ||||
-rw-r--r-- | test-suite/output/Errors.out | 8 | ||||
-rw-r--r-- | test-suite/output/Implicit.out | 1 | ||||
-rw-r--r-- | test-suite/output/Notations.out | 22 | ||||
-rw-r--r-- | test-suite/output/PrintInfos.out | 9 | ||||
-rw-r--r-- | test-suite/output/TranspModtype.out | 8 | ||||
-rw-r--r-- | test-suite/output/inference.out | 2 | ||||
-rw-r--r-- | test-suite/output/names.out | 1 | ||||
-rw-r--r-- | test-suite/output/rewrite-2172.out | 2 | ||||
-rw-r--r-- | test-suite/output/simpl.v | 6 |
13 files changed, 29 insertions, 93 deletions
diff --git a/test-suite/output/Arguments.out b/test-suite/output/Arguments.out index 629a1ab6..2c7b04c6 100644 --- a/test-suite/output/Arguments.out +++ b/test-suite/output/Arguments.out @@ -1,13 +1,11 @@ Nat.sub : nat -> nat -> nat -Nat.sub is not universe polymorphic Argument scopes are [nat_scope nat_scope] The reduction tactics unfold Nat.sub but avoid exposing match constructs Nat.sub is transparent Expands to: Constant Coq.Init.Nat.sub Nat.sub : nat -> nat -> nat -Nat.sub is not universe polymorphic Argument scopes are [nat_scope nat_scope] The reduction tactics unfold Nat.sub when applied to 1 argument but avoid exposing match constructs @@ -15,7 +13,6 @@ Nat.sub is transparent Expands to: Constant Coq.Init.Nat.sub Nat.sub : nat -> nat -> nat -Nat.sub is not universe polymorphic Argument scopes are [nat_scope nat_scope] The reduction tactics unfold Nat.sub when the 1st argument evaluates to a constructor and @@ -24,7 +21,6 @@ Nat.sub is transparent Expands to: Constant Coq.Init.Nat.sub Nat.sub : nat -> nat -> nat -Nat.sub is not universe polymorphic Argument scopes are [nat_scope nat_scope] The reduction tactics unfold Nat.sub when the 1st and 2nd arguments evaluate to a constructor and when applied to 2 arguments @@ -32,7 +28,6 @@ Nat.sub is transparent Expands to: Constant Coq.Init.Nat.sub Nat.sub : nat -> nat -> nat -Nat.sub is not universe polymorphic Argument scopes are [nat_scope nat_scope] The reduction tactics unfold Nat.sub when the 1st and 2nd arguments evaluate to a constructor @@ -42,7 +37,6 @@ pf : forall D1 C1 : Type, (D1 -> C1) -> forall D2 C2 : Type, (D2 -> C2) -> D1 * D2 -> C1 * C2 -pf is not universe polymorphic Arguments D2, C2 are implicit Arguments D1, C1 are implicit and maximally inserted Argument scopes are [foo_scope type_scope _ _ _ _ _] @@ -51,7 +45,6 @@ pf is transparent Expands to: Constant Top.pf fcomp : forall A B C : Type, (B -> C) -> (A -> B) -> A -> C -fcomp is not universe polymorphic Arguments A, B, C are implicit and maximally inserted Argument scopes are [type_scope type_scope type_scope _ _ _] The reduction tactics unfold fcomp when applied to 6 arguments @@ -59,20 +52,17 @@ fcomp is transparent Expands to: Constant Top.fcomp volatile : nat -> nat -volatile is not universe polymorphic Argument scope is [nat_scope] The reduction tactics always unfold volatile volatile is transparent Expands to: Constant Top.volatile f : T1 -> T2 -> nat -> unit -> nat -> nat -f is not universe polymorphic Argument scopes are [_ _ nat_scope _ nat_scope] f is transparent Expands to: Constant Top.S1.S2.f f : T1 -> T2 -> nat -> unit -> nat -> nat -f is not universe polymorphic Argument scopes are [_ _ nat_scope _ nat_scope] The reduction tactics unfold f when the 3rd, 4th and 5th arguments evaluate to a constructor @@ -80,7 +70,6 @@ f is transparent Expands to: Constant Top.S1.S2.f f : forall T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat -f is not universe polymorphic Argument T2 is implicit Argument scopes are [type_scope _ _ nat_scope _ nat_scope] The reduction tactics unfold f when the 4th, 5th and @@ -89,7 +78,6 @@ f is transparent Expands to: Constant Top.S1.f f : forall T1 T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat -f is not universe polymorphic Arguments T1, T2 are implicit Argument scopes are [type_scope type_scope _ _ nat_scope _ nat_scope] The reduction tactics unfold f when the 5th, 6th and @@ -102,7 +90,6 @@ Expands to: Constant Top.f : Prop f : forall T1 T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat -f is not universe polymorphic The reduction tactics unfold f when the 5th, 6th and 7th arguments evaluate to a constructor f is transparent @@ -110,8 +97,8 @@ Expands to: Constant Top.f forall w : r, w 3 true = tt : Prop The command has indeed failed with message: -=> Error: Unknown interpretation for notation "$". +Error: Unknown interpretation for notation "$". w 3 true = tt : Prop The command has indeed failed with message: -=> Error: Extra argument _. +Error: Extra argument _. diff --git a/test-suite/output/ArgumentsScope.out b/test-suite/output/ArgumentsScope.out index 71d5fc78..6643c142 100644 --- a/test-suite/output/ArgumentsScope.out +++ b/test-suite/output/ArgumentsScope.out @@ -1,70 +1,56 @@ a : bool -> bool -a is not universe polymorphic Argument scope is [bool_scope] Expands to: Variable a b : bool -> bool -b is not universe polymorphic Argument scope is [bool_scope] Expands to: Variable b negb'' : bool -> bool -negb'' is not universe polymorphic Argument scope is [bool_scope] negb'' is transparent Expands to: Constant Top.A.B.negb'' negb' : bool -> bool -negb' is not universe polymorphic Argument scope is [bool_scope] negb' is transparent Expands to: Constant Top.A.negb' negb : bool -> bool -negb is not universe polymorphic Argument scope is [bool_scope] negb is transparent Expands to: Constant Coq.Init.Datatypes.negb a : bool -> bool -a is not universe polymorphic Expands to: Variable a b : bool -> bool -b is not universe polymorphic Expands to: Variable b negb : bool -> bool -negb is not universe polymorphic negb is transparent Expands to: Constant Coq.Init.Datatypes.negb negb' : bool -> bool -negb' is not universe polymorphic negb' is transparent Expands to: Constant Top.A.negb' negb'' : bool -> bool -negb'' is not universe polymorphic negb'' is transparent Expands to: Constant Top.A.B.negb'' a : bool -> bool -a is not universe polymorphic Expands to: Variable a negb : bool -> bool -negb is not universe polymorphic negb is transparent Expands to: Constant Coq.Init.Datatypes.negb negb' : bool -> bool -negb' is not universe polymorphic negb' is transparent Expands to: Constant Top.negb' negb'' : bool -> bool -negb'' is not universe polymorphic negb'' is transparent Expands to: Constant Top.negb'' diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out index c29f5649..1e3cc37d 100644 --- a/test-suite/output/Arguments_renaming.out +++ b/test-suite/output/Arguments_renaming.out @@ -1,8 +1,8 @@ The command has indeed failed with message: -=> Error: To rename arguments the "rename" flag must be specified. +Error: To rename arguments the "rename" flag must be specified. Argument A renamed to B. The command has indeed failed with message: -=> Error: To rename arguments the "rename" flag must be specified. +Error: To rename arguments the "rename" flag must be specified. Argument A renamed to T. @eq_refl : forall (B : Type) (y : B), y = y @@ -20,7 +20,6 @@ For eq: Argument scopes are [type_scope _ _] For eq_refl: Argument scopes are [type_scope _] eq_refl : forall (A : Type) (x : A), x = x -eq_refl is not universe polymorphic Arguments are renamed to B, y When applied to no arguments: Arguments B, y are implicit and maximally inserted @@ -36,7 +35,6 @@ For myEq: Argument scopes are [type_scope _ _] For myrefl: Argument scopes are [type_scope _ _] myrefl : forall (B : Type) (x : A), B -> myEq B x x -myrefl is not universe polymorphic Arguments are renamed to C, x, _ Argument C is implicit and maximally inserted Argument scopes are [type_scope _ _] @@ -49,13 +47,11 @@ fix myplus (T : Type) (t : T) (n m : nat) {struct n} : nat := end : forall T : Type, T -> nat -> nat -> nat -myplus is not universe polymorphic Arguments are renamed to Z, t, n, m Argument Z is implicit and maximally inserted Argument scopes are [type_scope _ nat_scope nat_scope] myplus : forall T : Type, T -> nat -> nat -> nat -myplus is not universe polymorphic Arguments are renamed to Z, t, n, m Argument Z is implicit and maximally inserted Argument scopes are [type_scope _ nat_scope nat_scope] @@ -74,7 +70,6 @@ For myEq: Argument scopes are [type_scope type_scope _ _] For myrefl: Argument scopes are [type_scope type_scope _ _] myrefl : forall (A B : Type) (x : A), B -> myEq A B x x -myrefl is not universe polymorphic Arguments are renamed to A, C, x, _ Argument C is implicit and maximally inserted Argument scopes are [type_scope type_scope _ _] @@ -89,13 +84,11 @@ fix myplus (T : Type) (t : T) (n m : nat) {struct n} : nat := end : forall T : Type, T -> nat -> nat -> nat -myplus is not universe polymorphic Arguments are renamed to Z, t, n, m Argument Z is implicit and maximally inserted Argument scopes are [type_scope _ nat_scope nat_scope] myplus : forall T : Type, T -> nat -> nat -> nat -myplus is not universe polymorphic Arguments are renamed to Z, t, n, m Argument Z is implicit and maximally inserted Argument scopes are [type_scope _ nat_scope nat_scope] @@ -106,15 +99,15 @@ Expands to: Constant Top.myplus @myplus : forall Z : Type, Z -> nat -> nat -> nat The command has indeed failed with message: -=> Error: All arguments lists must declare the same names. +Error: All arguments lists must declare the same names. The command has indeed failed with message: -=> Error: The following arguments are not declared: x. +Error: The following arguments are not declared: x. The command has indeed failed with message: -=> Error: Arguments names must be distinct. +Error: Arguments names must be distinct. The command has indeed failed with message: -=> Error: Argument z cannot be declared implicit. +Error: Argument z cannot be declared implicit. The command has indeed failed with message: -=> Error: Extra argument y. +Error: Extra argument y. The command has indeed failed with message: -=> Error: To rename arguments the "rename" flag must be specified. +Error: To rename arguments the "rename" flag must be specified. Argument A renamed to R. diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out index d5903483..09f032d4 100644 --- a/test-suite/output/Cases.out +++ b/test-suite/output/Cases.out @@ -6,8 +6,6 @@ fix F (t : t) : P t := end : forall P : t -> Type, (let x := t in forall x0 : x, P x0 -> P (k x0)) -> forall t : t, P t - -t_rect is not universe polymorphic = fun d : TT => match d with | @CTT _ _ b => b end @@ -26,7 +24,6 @@ match Nat.eq_dec x y with end : forall (x y : nat) (P : nat -> Type), P x -> P y -> P y -proj is not universe polymorphic Argument scopes are [nat_scope nat_scope _ _ _] foo = fix foo (A : Type) (l : list A) {struct l} : option A := @@ -37,7 +34,6 @@ fix foo (A : Type) (l : list A) {struct l} : option A := end : forall A : Type, list A -> option A -foo is not universe polymorphic Argument scopes are [type_scope list_scope] uncast = fun (A : Type) (x : I A) => match x with @@ -45,12 +41,9 @@ fun (A : Type) (x : I A) => match x with end : forall A : Type, I A -> A -uncast is not universe polymorphic Argument scopes are [type_scope _] foo' = if A 0 then true else false : bool - -foo' is not universe polymorphic f = fun H : B => match H with @@ -61,5 +54,3 @@ match H with else fun _ : P false => Logic.I) x end : B -> True - -f is not universe polymorphic diff --git a/test-suite/output/Errors.out b/test-suite/output/Errors.out index bcc37b63..6354ad46 100644 --- a/test-suite/output/Errors.out +++ b/test-suite/output/Errors.out @@ -1,7 +1,7 @@ The command has indeed failed with message: -=> Error: The field t is missing in Top.M. +The field t is missing in Top.M. The command has indeed failed with message: -=> Error: Unable to unify "nat" with "True". +Unable to unify "nat" with "True". The command has indeed failed with message: -=> In nested Ltac calls to "f" and "apply x", last call failed. -Error: Unable to unify "nat" with "True". +In nested Ltac calls to "f" and "apply x", last call failed. +Unable to unify "nat" with "True". diff --git a/test-suite/output/Implicit.out b/test-suite/output/Implicit.out index 0b0f501f..3b65003c 100644 --- a/test-suite/output/Implicit.out +++ b/test-suite/output/Implicit.out @@ -5,7 +5,6 @@ ex_intro (P:=fun _ : nat => True) (x:=0) I d2 = fun x : nat => d1 (y:=x) : forall x x0 : nat, x0 = x -> x0 = x -d2 is not universe polymorphic Arguments x, x0 are implicit Argument scopes are [nat_scope nat_scope _] map id (1 :: nil) diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out index 60ee72b3..6efd671a 100644 --- a/test-suite/output/Notations.out +++ b/test-suite/output/Notations.out @@ -41,29 +41,29 @@ fun x : nat => ifn x is succ n then n else 0 -4 : Z The command has indeed failed with message: -=> Error: x should not be bound in a recursive pattern of the right-hand side. +Error: x should not be bound in a recursive pattern of the right-hand side. The command has indeed failed with message: -=> Error: in the right-hand side, y and z should appear in +Error: in the right-hand side, y and z should appear in term position as part of a recursive pattern. The command has indeed failed with message: -=> Error: The reference w was not found in the current environment. +The reference w was not found in the current environment. The command has indeed failed with message: -=> Error: in the right-hand side, y and z should appear in +Error: in the right-hand side, y and z should appear in term position as part of a recursive pattern. The command has indeed failed with message: -=> Error: z is expected to occur in binding position in the right-hand side. +Error: z is expected to occur in binding position in the right-hand side. The command has indeed failed with message: -=> Error: as y is a non-closed binder, no such "," is allowed to occur. +Error: as y is a non-closed binder, no such "," is allowed to occur. The command has indeed failed with message: -=> Error: Cannot find where the recursive pattern starts. +Error: Cannot find where the recursive pattern starts. The command has indeed failed with message: -=> Error: Cannot find where the recursive pattern starts. +Error: Cannot find where the recursive pattern starts. The command has indeed failed with message: -=> Error: Cannot find where the recursive pattern starts. +Error: Cannot find where the recursive pattern starts. The command has indeed failed with message: -=> Error: Cannot find where the recursive pattern starts. +Error: Cannot find where the recursive pattern starts. The command has indeed failed with message: -=> Error: Both ends of the recursive pattern are the same. +Error: Both ends of the recursive pattern are the same. SUM (nat * nat) nat : Set FST (0; 1) diff --git a/test-suite/output/PrintInfos.out b/test-suite/output/PrintInfos.out index 0457c860..ba076f05 100644 --- a/test-suite/output/PrintInfos.out +++ b/test-suite/output/PrintInfos.out @@ -25,7 +25,6 @@ For eq: Argument scopes are [type_scope _ _] For eq_refl: Argument scopes are [type_scope _] eq_refl : forall (A : Type) (x : A), x = x -eq_refl is not universe polymorphic When applied to no arguments: Arguments A, x are implicit and maximally inserted When applied to 1 argument: @@ -46,11 +45,9 @@ fix add (n m : nat) {struct n} : nat := end : nat -> nat -> nat -Nat.add is not universe polymorphic Argument scopes are [nat_scope nat_scope] Nat.add : nat -> nat -> nat -Nat.add is not universe polymorphic Argument scopes are [nat_scope nat_scope] Nat.add is transparent Expands to: Constant Coq.Init.Nat.add @@ -58,7 +55,6 @@ Nat.add : nat -> nat -> nat plus_n_O : forall n : nat, n = n + 0 -plus_n_O is not universe polymorphic Argument scope is [nat_scope] plus_n_O is opaque Expands to: Constant Coq.Init.Peano.plus_n_O @@ -80,13 +76,11 @@ For le_n: Argument scope is [nat_scope] For le_S: Argument scopes are [nat_scope nat_scope _] comparison : Set -comparison is not universe polymorphic Expands to: Inductive Coq.Init.Datatypes.comparison Inductive comparison : Set := Eq : comparison | Lt : comparison | Gt : comparison bar : foo -bar is not universe polymorphic Expanded type for implicit arguments bar : forall x : nat, x = 0 @@ -94,14 +88,12 @@ Argument x is implicit and maximally inserted Expands to: Constant Top.bar *** [ bar : foo ] -bar is not universe polymorphic Expanded type for implicit arguments bar : forall x : nat, x = 0 Argument x is implicit and maximally inserted bar : foo -bar is not universe polymorphic Expanded type for implicit arguments bar : forall x : nat, x = 0 @@ -109,7 +101,6 @@ Argument x is implicit and maximally inserted Expands to: Constant Top.bar *** [ bar : foo ] -bar is not universe polymorphic Expanded type for implicit arguments bar : forall x : nat, x = 0 diff --git a/test-suite/output/TranspModtype.out b/test-suite/output/TranspModtype.out index 67b65d4b..f94ed642 100644 --- a/test-suite/output/TranspModtype.out +++ b/test-suite/output/TranspModtype.out @@ -1,15 +1,7 @@ TrM.A = M.A : Set - -TrM.A is not universe polymorphic OpM.A = M.A : Set - -OpM.A is not universe polymorphic TrM.B = M.B : Set - -TrM.B is not universe polymorphic *** [ OpM.B : Set ] - -OpM.B is not universe polymorphic diff --git a/test-suite/output/inference.out b/test-suite/output/inference.out index d69baaec..b1952aec 100644 --- a/test-suite/output/inference.out +++ b/test-suite/output/inference.out @@ -4,8 +4,6 @@ fun e : option L => match e with | None => None end : option L -> option L - -P is not universe polymorphic fun (m n p : nat) (H : S m <= S n + p) => le_S_n m (n + p) H : forall m n p : nat, S m <= S n + p -> m <= n + p fun n : nat => let x := A n in ?y ?y0:T n diff --git a/test-suite/output/names.out b/test-suite/output/names.out index 2892dfd5..9471b892 100644 --- a/test-suite/output/names.out +++ b/test-suite/output/names.out @@ -1,5 +1,4 @@ The command has indeed failed with message: -=> Error: In environment y : nat The term "a y" has type "{y0 : nat | y = y0}" diff --git a/test-suite/output/rewrite-2172.out b/test-suite/output/rewrite-2172.out index 30385072..27b0dc1b 100644 --- a/test-suite/output/rewrite-2172.out +++ b/test-suite/output/rewrite-2172.out @@ -1,2 +1,2 @@ The command has indeed failed with message: -=> Error: Unable to find an instance for the variable E. +Unable to find an instance for the variable E. diff --git a/test-suite/output/simpl.v b/test-suite/output/simpl.v index 89638eed..5f1926f1 100644 --- a/test-suite/output/simpl.v +++ b/test-suite/output/simpl.v @@ -4,10 +4,10 @@ Goal forall x, 0+x = 1+x. intro x. simpl (_ + x). Show. -Undo 2. +Undo. simpl (_ + x) at 2. Show. -Undo 2. +Undo. simpl (0 + _). Show. -Undo 2. +Undo. |