diff options
Diffstat (limited to 'test-suite/output')
48 files changed, 497 insertions, 177 deletions
diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out index e46774f68a..9fd846ac16 100644 --- a/test-suite/output/Arguments_renaming.out +++ b/test-suite/output/Arguments_renaming.out @@ -11,7 +11,7 @@ eq_refl : ?y = ?y where ?y : [ |- nat] -Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x +Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x. Arguments eq {A}%type_scope _ _ Arguments eq_refl {B}%type_scope {y}, [_] _ @@ -22,7 +22,7 @@ eq_refl is not universe polymorphic Arguments eq_refl {B}%type_scope {y}, [_] _ (where some original arguments have been renamed) Expands to: Constructor Coq.Init.Logic.eq_refl -Inductive myEq (B : Type) (x : A) : A -> Prop := myrefl : B -> myEq B x x +Inductive myEq (B : Type) (x : A) : A -> Prop := myrefl : B -> myEq B x x. Arguments myEq _%type_scope _ _ Arguments myrefl {C}%type_scope x _ @@ -55,7 +55,7 @@ Expands to: Constant Arguments_renaming.Test1.myplus @myplus : forall Z : Type, Z -> nat -> nat -> nat Inductive myEq (A B : Type) (x : A) : A -> Prop := - myrefl : B -> myEq A B x x + myrefl : B -> myEq A B x x. Arguments myEq (_ _)%type_scope _ _ Arguments myrefl A%type_scope {C}%type_scope x _ diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out index 6fd4d37ab4..ea647a990a 100644 --- a/test-suite/output/Cases.out +++ b/test-suite/output/Cases.out @@ -89,7 +89,7 @@ Arguments lem2 _%bool_scope lem3 = fun dd : nat * nat => let (bb, cc) as aa return (aa = aa) := dd in eq_refl : forall k : nat * nat, k = k -1 subgoal +1 goal x : nat n, n0 := match x + 0 with @@ -109,7 +109,7 @@ fun dd : nat * nat => let (bb, cc) as aa return (aa = aa) := dd in eq_refl end : x = x ============================ x + 0 = 0 -1 subgoal +1 goal p : nat a, diff --git a/test-suite/output/CompactContexts.out b/test-suite/output/CompactContexts.out index 9d1d19877e..f0a8019b67 100644 --- a/test-suite/output/CompactContexts.out +++ b/test-suite/output/CompactContexts.out @@ -1,4 +1,4 @@ -1 subgoal +1 goal hP1 : True a : nat b : list nat h : forall x : nat, {y : nat | y > x} diff --git a/test-suite/output/DebugFlags.out b/test-suite/output/DebugFlags.out new file mode 100644 index 0000000000..0385413937 --- /dev/null +++ b/test-suite/output/DebugFlags.out @@ -0,0 +1,44 @@ +File "stdin", line 1, characters 0-16: +Warning: There is no debug flag "cbn". [unknown-debug-flag,option] +Debug: [RAKAM] <<forall A : Type, A -> A -> Prop|>> +Debug: [RAKAM] <><><><><> +Debug: [RAKAM] <<forall A : Type, A -> A -> Prop|>> +Debug: [RAKAM] <><><><><> +Debug: [RAKAM] <<?A -> ?A -> Prop|>> +Debug: [RAKAM] <><><><><> +Debug: [RAKAM] <<?A -> ?A -> Prop|>> +Debug: [RAKAM] <><><><><> +Debug: [RAKAM] <<nat -> nat -> nat|>> +Debug: [RAKAM] <><><><><> +Debug: [RAKAM] <<nat -> nat -> nat|>> +Debug: [RAKAM] <><><><><> +Debug: [RAKAM] <<nat -> nat|>> +Debug: [RAKAM] <><><><><> +Debug: [RAKAM] <<nat -> nat|>> +Debug: [RAKAM] <><><><><> +Debug: [RAKAM] <<nat -> nat|>> +Debug: [RAKAM] <><><><><> +Debug: [RAKAM] <<nat -> nat|>> +Debug: [RAKAM] <><><><><> +Debug: [RAKAM] <<nat -> nat|>> +Debug: [RAKAM] <><><><><> +Debug: [RAKAM] <<nat -> nat|>> +Debug: [RAKAM] <><><><><> +Debug: [RAKAM] <<nat -> nat|>> +Debug: [RAKAM] <><><><><> +Debug: [RAKAM] <<nat -> nat|>> +Debug: [RAKAM] <><><><><> +Debug: [RAKAM] <<nat -> nat|>> +Debug: [RAKAM] <><><><><> +Debug: [RAKAM] <<nat -> nat|>> +Debug: [RAKAM] <><><><><> +Debug: [RAKAM] <<nat -> nat|>> +Debug: [RAKAM] <><><><><> +Debug: [RAKAM] <<nat -> nat|>> +Debug: [RAKAM] <><><><><> +Debug: [RAKAM] <<nat -> Prop|>> +Debug: [RAKAM] <><><><><> +Debug: [RAKAM] <<nat -> Prop|>> +Debug: [RAKAM] <><><><><> +2 + 3 = 0 + : Prop diff --git a/test-suite/output/DebugFlags.v b/test-suite/output/DebugFlags.v new file mode 100644 index 0000000000..32c0f2d24b --- /dev/null +++ b/test-suite/output/DebugFlags.v @@ -0,0 +1,5 @@ +Set Debug "cbn". + +Set Debug "RAKAM". + +Check 2 + 3 = 0. diff --git a/test-suite/output/Function.out b/test-suite/output/Function.out new file mode 100644 index 0000000000..e69de29bb2 --- /dev/null +++ b/test-suite/output/Function.out diff --git a/test-suite/output/Function.v b/test-suite/output/Function.v new file mode 100644 index 0000000000..b3e2a93895 --- /dev/null +++ b/test-suite/output/Function.v @@ -0,0 +1,31 @@ +Require Import FunInd List. + +(* Explanations: This kind of pattern matching displays a legitimate + unused variable warning in v8.13. + +Fixpoint f (l:list nat) : nat := + match l with + | nil => O + | S n :: nil => 1 + | x :: l' => f l' + end. +*) + +(* In v8.13 the same code with "Function" generates a lot more + warnings about variables created automatically by Function. These + are not legitimate. PR #13776 (post v8.13) removes all warnings + about pattern matching variables (and non truly recursive fixpoint) + for "Function". So this should not generate any warning. Note that + this PR removes also the legitimate warnings. It would be better if + this test generate the same warning as the Fixpoint above. This + test would then need to be updated. *) + +(* Ensuring the warning is a warning. *) +Set Warnings "matching-variable". +(* But no warning generated here. *) +Function f (l:list nat) : nat := + match l with + | nil => O + | S n :: nil => 1 + | n :: l' => f l' + end. diff --git a/test-suite/output/Inductive.out b/test-suite/output/Inductive.out index 8e10107673..fc3b6fbd99 100644 --- a/test-suite/output/Inductive.out +++ b/test-suite/output/Inductive.out @@ -5,7 +5,7 @@ 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 +Inductive foo (A : Type) (x : A) (y : A := x) : Prop := Foo : foo A x. Arguments foo _%type_scope _ Arguments Foo _%type_scope _ diff --git a/test-suite/output/InitSyntax.out b/test-suite/output/InitSyntax.out index 02e58775b5..fdd609f5b2 100644 --- a/test-suite/output/InitSyntax.out +++ b/test-suite/output/InitSyntax.out @@ -1,5 +1,5 @@ Inductive sig2 (A : Type) (P Q : A -> Prop) : Type := - exist2 : forall x : A, P x -> Q x -> {x : A | P x & Q x} + exist2 : forall x : A, P x -> Q x -> {x : A | P x & Q x}. Arguments sig2 [A]%type_scope (_ _)%type_scope Arguments exist2 [A]%type_scope (_ _)%function_scope _ _ _ diff --git a/test-suite/output/Int63Syntax.out b/test-suite/output/Int63Syntax.out index ca8e1b58a8..96af456891 100644 --- a/test-suite/output/Int63Syntax.out +++ b/test-suite/output/Int63Syntax.out @@ -15,9 +15,9 @@ 427 : int The command has indeed failed with message: -Cannot interpret this number as a value of type Coq.Numbers.Cyclic.Int63.PrimInt63.int +Cannot interpret this number as a value of type int The command has indeed failed with message: -Cannot interpret this number as a value of type Coq.Numbers.Cyclic.Int63.PrimInt63.int +Cannot interpret this number as a value of type int 0 : int 0 @@ -33,9 +33,11 @@ The reference x was not found in the current environment. add 2 2 : int The command has indeed failed with message: -int63 are only non-negative numbers. +Cannot interpret this number as a value of type int The command has indeed failed with message: overflow in int63 literal: 9223372036854775808 +0x1 + : int 2 : nat 2%int63 @@ -56,3 +58,21 @@ t = 2%i63 : int = 37151199385380486 : int + = 4 + : int + = 4 + : int + = 4 + : int + = add + : int -> int -> int + = 12 + : int + = 12 + : int + = 12 + : int + = 3 + x + : int + = 1 + 2 + x + : int diff --git a/test-suite/output/Int63Syntax.v b/test-suite/output/Int63Syntax.v index 6f1046f7a5..be0ee701af 100644 --- a/test-suite/output/Int63Syntax.v +++ b/test-suite/output/Int63Syntax.v @@ -20,6 +20,11 @@ Fail Check 0x. Check (PrimInt63.add 2 2). Fail Check -1. Fail Check 9223372036854775808. + +Set Printing All. +Check 1%int63. +Unset Printing All. + Open Scope nat_scope. Check 2. (* : nat *) Check 2%int63. @@ -40,3 +45,18 @@ Open Scope int63_scope. Check (2+2). Eval vm_compute in 2+2. Eval vm_compute in 65675757 * 565675998. + +Eval simpl in 2+2. +Eval hnf in 2+2. +Eval cbn in 2+2. +Eval hnf in PrimInt63.add. + +Eval simpl in (2 * 3) + (2 * 3). +Eval hnf in (2 * 3) + (2 * 3). +Eval cbn in (2 * 3) + (2 * 3). + +Section TestNoSimpl. +Variable x : int. +Eval simpl in 1 + 2 + x. +Eval hnf in 1 + 2 + x. +End TestNoSimpl. diff --git a/test-suite/output/Intuition.out b/test-suite/output/Intuition.out index f2bf25ca65..e273307d75 100644 --- a/test-suite/output/Intuition.out +++ b/test-suite/output/Intuition.out @@ -1,4 +1,4 @@ -1 subgoal +1 goal m, n : Z H : (m >= n)%Z diff --git a/test-suite/output/Naming.out b/test-suite/output/Naming.out index 0a989646cf..2daa5a6bb5 100644 --- a/test-suite/output/Naming.out +++ b/test-suite/output/Naming.out @@ -1,23 +1,23 @@ -1 subgoal +1 goal x3 : nat ============================ forall x x1 x4 x0 : nat, (forall x2 x5 : nat, x2 + x1 = x4 + x5) -> x + x1 = x4 + x0 -1 subgoal +1 goal x3, x, x1, x4, x0 : nat H : forall x x3 : nat, x + x1 = x4 + x3 ============================ x + x1 = x4 + x0 -1 subgoal +1 goal x3 : nat ============================ forall x x1 x4 x0 : nat, (forall x2 x5 : nat, x2 + x1 = x4 + x5 -> foo (S x2 + x1)) -> x + x1 = x4 + x0 -> foo (S x) -1 subgoal +1 goal x3 : nat ============================ @@ -27,7 +27,7 @@ forall x6 x7 x8 S0 : nat, x6 + S0 = x7 + x8 + (S x2 + x1)) -> x + x1 = x4 + x0 -> forall x5 x6 x7 S : nat, x5 + S = x6 + x7 + Datatypes.S x -1 subgoal +1 goal x3, x, x1, x4, x0 : nat ============================ @@ -36,7 +36,7 @@ forall x6 x7 x8 S0 : nat, x6 + S0 = x7 + x8 + (S x2 + x1)) -> x + x1 = x4 + x0 -> forall x5 x6 x7 S : nat, x5 + S = x6 + x7 + Datatypes.S x -1 subgoal +1 goal x3, x, x1, x4, x0 : nat H : forall x x3 : nat, @@ -45,7 +45,7 @@ H0 : x + x1 = x4 + x0 ============================ forall x5 x6 x7 S : nat, x5 + S = x6 + x7 + Datatypes.S x -1 subgoal +1 goal x3, x, x1, x4, x0 : nat H : forall x x3 : nat, @@ -55,7 +55,7 @@ x5, x6, x7, S : nat ============================ x5 + S = x6 + x7 + Datatypes.S x -1 subgoal +1 goal x3, a : nat H : a = 0 -> forall a : nat, a = 0 diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out index a9bed49922..cc9e745f6b 100644 --- a/test-suite/output/Notations3.out +++ b/test-suite/output/Notations3.out @@ -6,7 +6,7 @@ : nat * nat * (nat * nat) (0, 2, (2, 2)) : nat * nat * (nat * nat) -pair (pair O (S (S O))) (pair (S (S O)) O) +pair (pair 0 2) (pair 2 0) : prod (prod nat nat) (prod nat nat) << 0, 2, 4 >> : nat * nat * nat * (nat * (nat * nat)) @@ -16,8 +16,7 @@ pair (pair O (S (S O))) (pair (S (S O)) O) : nat * nat * nat * (nat * (nat * nat)) (0, 2, 4, (0, (2, 4))) : nat * nat * nat * (nat * (nat * nat)) -pair (pair (pair O (S (S O))) (S (S (S (S O))))) - (pair (S (S (S (S O)))) (pair (S (S O)) O)) +pair (pair (pair 0 2) 4) (pair 4 (pair 2 0)) : prod (prod (prod nat nat) nat) (prod nat (prod nat nat)) ETA x y : nat, Nat.add : nat -> nat -> nat @@ -174,9 +173,8 @@ forall_non_null x y z t : nat , x = y /\ z = t : nat * (nat * nat) * (nat * nat * nat) * (nat * (nat * nat)) * (nat * nat * nat) pair - (pair - (pair (pair (S (S O)) (pair (S O) O)) (pair (pair O (S (S O))) (S O))) - (pair (S O) (pair (S (S O)) O))) (pair (pair O (S O)) (S (S O))) + (pair (pair (pair 2 (pair 1 0)) (pair (pair 0 2) 1)) (pair 1 (pair 2 0))) + (pair (pair 0 1) 2) : prod (prod (prod (prod nat (prod nat nat)) (prod (prod nat nat) nat)) (prod nat (prod nat nat))) (prod (prod nat nat) nat) @@ -238,7 +236,7 @@ Notation "'exists' ! x .. y , p" := (default interpretation) Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z) : core_scope (default interpretation) -1 subgoal +1 goal ============================ ##@% diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out index 3477a293e3..0b18981f4e 100644 --- a/test-suite/output/Notations4.out +++ b/test-suite/output/Notations4.out @@ -77,18 +77,18 @@ fun x : nat => [x] : nat -> nat ∀ x : nat, x = x : Prop -File "stdin", line 184, characters 0-160: +File "stdin", line 187, characters 0-160: Warning: Notation "∀ _ .. _ , _" was already defined with a different format in scope type_scope. [notation-incompatible-format,parsing] ∀x : nat,x = x : Prop -File "stdin", line 197, characters 0-60: +File "stdin", line 200, characters 0-60: Warning: Notation "_ %%% _" was already defined with a different format. [notation-incompatible-format,parsing] -File "stdin", line 201, characters 0-64: +File "stdin", line 204, characters 0-64: Warning: Notation "_ %%% _" was already defined with a different format. [notation-incompatible-format,parsing] -File "stdin", line 206, characters 0-62: +File "stdin", line 209, characters 0-62: Warning: Lonely notation "_ %%%% _" was already defined with a different format. [notation-incompatible-format,parsing] 3 %% 4 @@ -97,10 +97,10 @@ format. [notation-incompatible-format,parsing] : nat 3 %% 4 : nat -File "stdin", line 234, characters 0-61: +File "stdin", line 237, characters 0-61: Warning: The format modifier is irrelevant for only parsing rules. [irrelevant-format-only-parsing,parsing] -File "stdin", line 238, characters 0-63: +File "stdin", line 241, characters 0-63: Warning: The only parsing modifier has no effect in Reserved Notation. [irrelevant-reserved-notation-only-parsing,parsing] fun x : nat => U (S x) @@ -111,7 +111,7 @@ fun x : nat => V x : forall x : nat, nat * (?T -> ?T) where ?T : [x : nat x0 : ?T |- Type] (x0 cannot be used) -File "stdin", line 255, characters 0-30: +File "stdin", line 258, characters 0-30: Warning: Notation "_ :=: _" was already used. [notation-overridden,parsing] 0 :=: 0 : Prop diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v index ebad12af88..a5ec92fe3c 100644 --- a/test-suite/output/Notations4.v +++ b/test-suite/output/Notations4.v @@ -103,7 +103,10 @@ Module NumberNotations. Delimit Scope test17_scope with test17. Local Set Primitive Projections. Record myint63 := of_int { to_int : int }. - Number Notation myint63 of_int to_int : test17_scope. + Definition parse x := + match x with Pos x => Some (of_int x) | Neg _ => None end. + Definition print x := Pos (to_int x). + Number Notation myint63 parse print : test17_scope. Check let v := 0%test17 in v : myint63. End Test17. End NumberNotations. diff --git a/test-suite/output/NumberNotations.out b/test-suite/output/NumberNotations.out index 60682edec8..df9b39389c 100644 --- a/test-suite/output/NumberNotations.out +++ b/test-suite/output/NumberNotations.out @@ -260,28 +260,28 @@ The command has indeed failed with message: add is not a constructor of an inductive type. The command has indeed failed with message: Missing mapping for constructor Iempty. -File "stdin", line 574, characters 56-61: +File "stdin", line 577, characters 56-61: Warning: Type of I'sum seems incompatible with the type of sum. Expected type is: (I' -> I' -> I') instead of (I -> I' -> I'). This might yield ill typed terms when using the notation. [via-type-mismatch,numbers] -File "stdin", line 579, characters 32-33: +File "stdin", line 582, characters 32-33: Warning: I was already mapped to Set, mapping it also to nat might yield ill typed terms when using the notation. [via-type-remapping,numbers] -File "stdin", line 579, characters 37-42: +File "stdin", line 582, characters 37-42: Warning: Type of Iunit seems incompatible with the type of O. Expected type is: I instead of I. This might yield ill typed terms when using the notation. [via-type-mismatch,numbers] The command has indeed failed with message: 'via' and 'abstract' cannot be used together. -File "stdin", line 659, characters 21-23: +File "stdin", line 662, characters 21-23: Warning: Type of I1 seems incompatible with the type of Fin.F1. Expected type is: (nat -> I) instead of I. This might yield ill typed terms when using the notation. [via-type-mismatch,numbers] -File "stdin", line 659, characters 35-37: +File "stdin", line 662, characters 35-37: Warning: Type of IS seems incompatible with the type of Fin.FS. Expected type is: (nat -> I -> I) instead of (I -> I). This might yield ill typed terms when using the notation. diff --git a/test-suite/output/NumberNotations.v b/test-suite/output/NumberNotations.v index 718da13500..85400c2fd4 100644 --- a/test-suite/output/NumberNotations.v +++ b/test-suite/output/NumberNotations.v @@ -328,7 +328,10 @@ Module Test17. Delimit Scope test17_scope with test17. Local Set Primitive Projections. Record myint63 := of_int { to_int : int }. - Number Notation myint63 of_int to_int : test17_scope. + Definition parse x := + match x with Pos x => Some (of_int x) | Neg _ => None end. + Definition print x := Pos (to_int x). + Number Notation myint63 parse print : test17_scope. Check let v := 0%test17 in v : myint63. End Test17. diff --git a/test-suite/output/Partac.out b/test-suite/output/Partac.out index 889e698fa2..ce5dbdedb4 100644 --- a/test-suite/output/Partac.out +++ b/test-suite/output/Partac.out @@ -1,6 +1,6 @@ The command has indeed failed with message: The term "false" has type "bool" while it is expected to have type "nat". -(for subgoal 1) +(for goal 1) The command has indeed failed with message: The term "0" has type "nat" while it is expected to have type "bool". -(for subgoal 2) +(for goal 2) diff --git a/test-suite/output/PrintInfos.out b/test-suite/output/PrintInfos.out index fe16dba496..03b9e3b527 100644 --- a/test-suite/output/PrintInfos.out +++ b/test-suite/output/PrintInfos.out @@ -4,14 +4,14 @@ existT is template universe polymorphic on sigT.u0 sigT.u1 Arguments existT [A]%type_scope _%function_scope _ _ Expands to: Constructor Coq.Init.Specif.existT Inductive sigT (A : Type) (P : A -> Type) : Type := - existT : forall x : A, P x -> {x : A & P x} + existT : forall x : A, P x -> {x : A & P x}. 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} Argument A is implicit -Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x +Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x. Arguments eq {A}%type_scope _ _ Arguments eq_refl {A}%type_scope {x}, [_] _ @@ -50,7 +50,7 @@ Arguments plus_n_O _%nat_scope plus_n_O is opaque Expands to: Constant Coq.Init.Peano.plus_n_O Inductive le (n : nat) : nat -> Prop := - le_n : n <= n | le_S : forall m : nat, n <= m -> n <= S m + le_n : n <= n | le_S : forall m : nat, n <= m -> n <= S m. Arguments le (_ _)%nat_scope Arguments le_n _%nat_scope @@ -60,7 +60,7 @@ comparison : Set comparison is not universe polymorphic Expands to: Inductive Coq.Init.Datatypes.comparison Inductive comparison : Set := - Eq : comparison | Lt : comparison | Gt : comparison + Eq : comparison | Lt : comparison | Gt : comparison. bar : foo bar is not universe polymorphic @@ -78,7 +78,7 @@ Arguments bar {x} Module Coq.Init.Peano Notation sym_eq := eq_sym Expands to: Notation Coq.Init.Logic.sym_eq -Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x +Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x. Arguments eq {A}%type_scope _ _ Arguments eq_refl {A}%type_scope {x}, {_} _ diff --git a/test-suite/output/PrintModule.out b/test-suite/output/PrintModule.out index 1a9bc068c5..7c7600b786 100644 --- a/test-suite/output/PrintModule.out +++ b/test-suite/output/PrintModule.out @@ -7,3 +7,11 @@ Module N : S with Module T := K := M Module N : S with Module T := M Module Type Func = Funsig (T0:Test) Sig Parameter x : T0.t. End +Module +A +:= Struct + Variant I : Set := C : nat -> I. + Record R : Set := Build_R { n : nat }. + Definition n : R -> nat. + End + diff --git a/test-suite/output/PrintModule.v b/test-suite/output/PrintModule.v index 54ef305be4..b4de03b556 100644 --- a/test-suite/output/PrintModule.v +++ b/test-suite/output/PrintModule.v @@ -60,3 +60,10 @@ Print Func. End Shortest_path. End QUX. + +Module A. +Variant I := C : nat -> I. +Record R := { n : nat }. +End A. + +Print Module A. diff --git a/test-suite/output/SearchHead.v b/test-suite/output/SearchHead.v deleted file mode 100644 index 2ee8a0d184..0000000000 --- a/test-suite/output/SearchHead.v +++ /dev/null @@ -1,19 +0,0 @@ -(* Some tests of the Search command *) - -SearchHead le. (* app nodes *) -SearchHead bool. (* no apps *) -SearchHead (@eq nat). (* complex pattern *) - -Definition newdef := fun x:nat => x = x. - -Goal forall n:nat, newdef n -> False. - intros n h. - SearchHead newdef. (* search hypothesis *) -Abort. - - -Goal forall n (P:nat -> Prop), P n -> False. - intros n P h. - SearchHead P. (* search hypothesis also for patterns *) -Abort. - diff --git a/test-suite/output/SearchHead.out b/test-suite/output/Search_headconcl.out index 2f0d854ac6..24e2ee76af 100644 --- a/test-suite/output/SearchHead.out +++ b/test-suite/output/Search_headconcl.out @@ -1,17 +1,9 @@ -File "stdin", line 3, characters 0-14: -Warning: -SearchHead is deprecated. Use the headconcl: clause of Search instead. -[deprecated-searchhead,deprecated] 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_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 -File "stdin", line 4, characters 0-16: -Warning: -SearchHead is deprecated. Use the headconcl: clause of Search instead. -[deprecated-searchhead,deprecated] false: bool true: bool negb: bool -> bool @@ -35,10 +27,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 -File "stdin", line 5, characters 0-21: -Warning: -SearchHead is deprecated. Use the headconcl: clause of Search instead. -[deprecated-searchhead,deprecated] 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 @@ -57,13 +45,5 @@ 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 -File "stdin", line 11, characters 2-20: -Warning: -SearchHead is deprecated. Use the headconcl: clause of Search instead. -[deprecated-searchhead,deprecated] h: newdef n -File "stdin", line 17, characters 2-15: -Warning: -SearchHead is deprecated. Use the headconcl: clause of Search instead. -[deprecated-searchhead,deprecated] h: P n diff --git a/test-suite/output/Search_headconcl.v b/test-suite/output/Search_headconcl.v new file mode 100644 index 0000000000..8b168dcd25 --- /dev/null +++ b/test-suite/output/Search_headconcl.v @@ -0,0 +1,18 @@ +(* Some tests of the Search command *) + +Search headconcl: le. (* app nodes *) +Search headconcl: bool. (* no apps *) +Search headconcl: (@eq nat). (* complex pattern *) + +Definition newdef := fun x:nat => x = x. + +Goal forall n:nat, newdef n -> False. + intros n h. + Search headconcl: newdef. (* search hypothesis *) +Abort. + + +Goal forall n (P:nat -> Prop), P n -> False. + intros n P h. + Search headconcl: P. (* search hypothesis also for patterns *) +Abort. diff --git a/test-suite/output/Show.out b/test-suite/output/Show.out index f02e442be5..3db00be048 100644 --- a/test-suite/output/Show.out +++ b/test-suite/output/Show.out @@ -1,10 +1,10 @@ -3 subgoals (ID 29) +3 goals (ID 29) H : 0 = 0 ============================ 1 = 1 -subgoal 2 (ID 33) is: +goal 2 (ID 33) is: 1 = S (S m') -subgoal 3 (ID 20) is: +goal 3 (ID 20) is: S (S n') = S m diff --git a/test-suite/output/Sint63Syntax.out b/test-suite/output/Sint63Syntax.out new file mode 100644 index 0000000000..db14658307 --- /dev/null +++ b/test-suite/output/Sint63Syntax.out @@ -0,0 +1,66 @@ +2%sint63 + : int +2 + : int +-3 + : int +4611686018427387903 + : int +-4611686018427387904 + : int +427 + : int +427 + : int +427 + : int +427 + : int +427 + : int +The command has indeed failed with message: +Cannot interpret this number as a value of type int +The command has indeed failed with message: +Cannot interpret this number as a value of type int +0 + : int +0 + : int +The command has indeed failed with message: +The reference xg was not found in the current environment. +The command has indeed failed with message: +The reference xG was not found in the current environment. +The command has indeed failed with message: +The reference x1 was not found in the current environment. +The command has indeed failed with message: +The reference x was not found in the current environment. +2 + 2 + : int +The command has indeed failed with message: +Cannot interpret this number as a value of type int +The command has indeed failed with message: +Cannot interpret this number as a value of type int +0x1%int63 + : int +0x7fffffffffffffff%int63 + : int +2 + : nat +2%sint63 + : int +t = 2%si63 + : int +t = 2%si63 + : int +2 + : nat +2 + : int +(2 + 2)%sint63 + : int +2 + 2 + : int + = 4 + : int + = 37151199385380486 + : int diff --git a/test-suite/output/Sint63Syntax.v b/test-suite/output/Sint63Syntax.v new file mode 100644 index 0000000000..b9ed596537 --- /dev/null +++ b/test-suite/output/Sint63Syntax.v @@ -0,0 +1,49 @@ +Require Import Sint63. + +Check 2%sint63. +Open Scope sint63_scope. +Check 2. +Check -3. +Check 4611686018427387903. +Check -4611686018427387904. +Check 0x1ab. +Check 0X1ab. +Check 0x1Ab. +Check 0x1aB. +Check 0x1AB. +Fail Check 0x1ap5. (* exponents not implemented (yet?) *) +Fail Check 0x1aP5. +Check 0x0. +Check 0x000. +Fail Check 0xg. +Fail Check 0xG. +Fail Check 00x1. +Fail Check 0x. +Check (PrimInt63.add 2 2). +Fail Check 4611686018427387904. +Fail Check -4611686018427387905. + +Set Printing All. +Check 1%sint63. +Check (-1)%sint63. +Unset Printing All. + +Open Scope nat_scope. +Check 2. (* : nat *) +Check 2%sint63. +Delimit Scope sint63_scope with si63. +Definition t := 2%sint63. +Print t. +Delimit Scope nat_scope with sint63. +Print t. +Check 2. +Close Scope nat_scope. +Check 2. +Close Scope sint63_scope. +Delimit Scope sint63_scope with sint63. + +Check (2 + 2)%sint63. +Open Scope sint63_scope. +Check (2+2). +Eval vm_compute in 2+2. +Eval vm_compute in 65675757 * 565675998. diff --git a/test-suite/output/Unicode.out b/test-suite/output/Unicode.out index a57b3bbad5..abe6c39e8f 100644 --- a/test-suite/output/Unicode.out +++ b/test-suite/output/Unicode.out @@ -1,4 +1,4 @@ -1 subgoal +1 goal very_very_long_type_name1 : Type very_very_long_type_name2 : Type @@ -8,7 +8,7 @@ → True → ∀ (x : very_very_long_type_name1) (y : very_very_long_type_name2), f x y ∧ f x y ∧ f x y ∧ f x y ∧ f x y ∧ f x y -1 subgoal +1 goal very_very_long_type_name1 : Type very_very_long_type_name2 : Type @@ -18,7 +18,7 @@ → True → ∀ (x : very_very_long_type_name2) (y : very_very_long_type_name1) (z : very_very_long_type_name2), f y x ∧ f y z -1 subgoal +1 goal very_very_long_type_name1 : Type very_very_long_type_name2 : Type @@ -29,7 +29,7 @@ → ∀ (x : very_very_long_type_name2) (y : very_very_long_type_name1) (z : very_very_long_type_name2), f y x ∧ f y z ∧ f y x ∧ f y z ∧ f y x ∧ f y z -1 subgoal +1 goal very_very_long_type_name1 : Type very_very_long_type_name2 : Type diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out index 95b6c6ee95..4993b747fa 100644 --- a/test-suite/output/UnivBinders.out +++ b/test-suite/output/UnivBinders.out @@ -1,6 +1,7 @@ -Inductive Empty@{uu} : Type@{uu} := +Inductive Empty@{uu} : Type@{uu} := . (* uu |= *) -Record PWrap (A : Type@{uu}) : Type@{uu} := pwrap { punwrap : A } +Record PWrap (A : Type@{uu}) : Type@{uu} := pwrap + { punwrap : A }. (* uu |= *) PWrap has primitive projections with eta conversion. @@ -12,7 +13,8 @@ fun (A : Type@{uu}) (p : PWrap@{uu} A) => punwrap _ p (* uu |= *) Arguments punwrap _%type_scope _ -Record RWrap (A : Type@{uu}) : Type@{uu} := rwrap { runwrap : A } +Record RWrap (A : Type@{uu}) : Type@{uu} := rwrap + { runwrap : A }. (* uu |= *) Arguments RWrap _%type_scope @@ -80,9 +82,9 @@ foo@{uu u v} = Type@{u} -> Type@{v} -> Type@{uu} : Type@{max(uu+1,u+1,v+1)} (* uu u v |= *) -Inductive Empty@{E} : Type@{E} := +Inductive Empty@{E} : Type@{E} := . (* E |= *) -Record PWrap (A : Type@{E}) : Type@{E} := pwrap { punwrap : A } +Record PWrap (A : Type@{E}) : Type@{E} := pwrap { punwrap : A }. (* E |= *) PWrap has primitive projections with eta conversion. @@ -107,7 +109,7 @@ insec@{v} = Type@{uu} -> Type@{v} : Type@{max(uu+1,v+1)} (* v |= *) Inductive insecind@{k} : Type@{k+1} := - inseccstr : Type@{k} -> insecind@{k} + inseccstr : Type@{k} -> insecind@{k}. (* k |= *) Arguments inseccstr _%type_scope @@ -115,7 +117,7 @@ insec@{uu v} = Type@{uu} -> Type@{v} : Type@{max(uu+1,v+1)} (* uu v |= *) Inductive insecind@{uu k} : Type@{k+1} := - inseccstr : Type@{k} -> insecind@{uu k} + inseccstr : Type@{k} -> insecind@{uu k}. (* uu k |= *) Arguments inseccstr _%type_scope diff --git a/test-suite/output/bug_13821_native_command_line_warn.out b/test-suite/output/bug_13821_native_command_line_warn.out new file mode 100644 index 0000000000..e69de29bb2 --- /dev/null +++ b/test-suite/output/bug_13821_native_command_line_warn.out diff --git a/test-suite/output/bug_13821_native_command_line_warn.v b/test-suite/output/bug_13821_native_command_line_warn.v new file mode 100644 index 0000000000..a28210b6c2 --- /dev/null +++ b/test-suite/output/bug_13821_native_command_line_warn.v @@ -0,0 +1 @@ +(* -*- coq-prog-args: ("-w" "-native-compiler-disabled" "-native-compiler" "ondemand"); -*- *) diff --git a/test-suite/output/bug_9370.out b/test-suite/output/bug_9370.out index 0ff151c8b4..8d34b7143a 100644 --- a/test-suite/output/bug_9370.out +++ b/test-suite/output/bug_9370.out @@ -1,12 +1,12 @@ -1 subgoal +1 goal ============================ 1 = 1 -1 subgoal +1 goal ============================ 1 = 1 -1 subgoal +1 goal ============================ 1 = 1 diff --git a/test-suite/output/bug_9403.out b/test-suite/output/bug_9403.out index 850760d5ed..cd1030bd2e 100644 --- a/test-suite/output/bug_9403.out +++ b/test-suite/output/bug_9403.out @@ -1,4 +1,4 @@ -1 subgoal +1 goal X : tele α, β, γ1, γ2 : X → Prop diff --git a/test-suite/output/bug_9569.out b/test-suite/output/bug_9569.out index 2d474e4933..e49449679f 100644 --- a/test-suite/output/bug_9569.out +++ b/test-suite/output/bug_9569.out @@ -1,16 +1,16 @@ -1 subgoal +1 goal ============================ exists I : True, I = Logic.I -1 subgoal +1 goal ============================ f True False True False (Logic.True /\ Logic.False) -1 subgoal +1 goal ============================ [I | I = Logic.I; I = Logic.I] = [I | I = Logic.I; I = Logic.I] -1 subgoal +1 goal ============================ [I & I = Logic.I | I = Logic.I; Logic.I = I] diff --git a/test-suite/output/clear.out b/test-suite/output/clear.out index 42e3abf26f..ea01ac50d7 100644 --- a/test-suite/output/clear.out +++ b/test-suite/output/clear.out @@ -1,4 +1,4 @@ -1 subgoal +1 goal z := 0 : nat ============================ diff --git a/test-suite/output/goal_output.out b/test-suite/output/goal_output.out index 17c1aaa55b..453f6ee615 100644 --- a/test-suite/output/goal_output.out +++ b/test-suite/output/goal_output.out @@ -2,79 +2,79 @@ Nat.t = nat : Set Nat.t = nat : Set -2 subgoals +2 goals ============================ True -subgoal 2 is: +goal 2 is: True -2 subgoals, subgoal 1 (?Goal) +2 goals, goal 1 (?Goal) ============================ True -subgoal 2 (?Goal0) is: +goal 2 (?Goal0) is: True -1 subgoal +1 goal ============================ True -1 subgoal (?Goal0) +1 goal (?Goal0) ============================ True -1 subgoal (?Goal0) +1 goal (?Goal0) ============================ True *** Unfocused goals: -subgoal 2 (?Goal1) is: +goal 2 (?Goal1) is: True -subgoal 3 (?Goal) is: +goal 3 (?Goal) is: True -1 subgoal +1 goal ============================ True *** Unfocused goals: -subgoal 2 is: +goal 2 is: True -subgoal 3 is: +goal 3 is: True This subproof is complete, but there are some unfocused goals. Focus next goal with bullet -. -2 subgoals +2 goals -subgoal 1 is: +goal 1 is: True -subgoal 2 is: +goal 2 is: True This subproof is complete, but there are some unfocused goals. Focus next goal with bullet -. -2 subgoals +2 goals -subgoal 1 (?Goal0) is: +goal 1 (?Goal0) is: True -subgoal 2 (?Goal) is: +goal 2 (?Goal) is: True This subproof is complete, but there are some unfocused goals. Focus next goal with bullet -. -1 subgoal +1 goal -subgoal 1 is: +goal 1 is: True This subproof is complete, but there are some unfocused goals. Focus next goal with bullet -. -1 subgoal +1 goal -subgoal 1 (?Goal) is: +goal 1 (?Goal) is: True diff --git a/test-suite/output/ltac.out b/test-suite/output/ltac.out index efdc94fb1e..ed42429f85 100644 --- a/test-suite/output/ltac.out +++ b/test-suite/output/ltac.out @@ -38,7 +38,7 @@ Ltac foo := let w := () in let z := 1 in pose v -2 subgoals +2 goals n : nat ============================ @@ -47,5 +47,5 @@ Ltac foo := | S n1 => a n1 end) n = n -subgoal 2 is: +goal 2 is: forall a : nat, a = 0 diff --git a/test-suite/output/names.out b/test-suite/output/names.out index 48be63a46a..051bce7701 100644 --- a/test-suite/output/names.out +++ b/test-suite/output/names.out @@ -3,7 +3,7 @@ In environment y : nat The term "a y" has type "{y0 : nat | y = y0}" while it is expected to have type "{x : nat | x = y}". -1 focused subgoal +1 focused goal (shelved: 1) H : ?n <= 3 -> 3 <= ?n -> ?n = 3 diff --git a/test-suite/output/optimize_heap.out b/test-suite/output/optimize_heap.out index 94a0b19118..b6ee61a971 100644 --- a/test-suite/output/optimize_heap.out +++ b/test-suite/output/optimize_heap.out @@ -1,8 +1,8 @@ -1 subgoal +1 goal ============================ True -1 subgoal +1 goal ============================ True diff --git a/test-suite/output/primitive_tokens.out b/test-suite/output/primitive_tokens.out new file mode 100644 index 0000000000..afe9b25442 --- /dev/null +++ b/test-suite/output/primitive_tokens.out @@ -0,0 +1,61 @@ +"foo" + : string +1234 + : nat +Nat.add 1 2 + : nat +match "a" with +| "a" => true +| _ => false +end + : bool +match 1 with +| 1 => true +| _ => false +end + : bool +{| field := 7 |} + : test +String (Ascii.Ascii false true true false false true true false) + (String (Ascii.Ascii true true true true false true true false) + (String (Ascii.Ascii true true true true false true true false) + EmptyString)) + : string +S + (S + (S + (S + (S + (S + (S + (S + (S + (S + (S + (S + (S + (S + (S + (S + (S + (S + (S (S (S (S (S (S ...))))))))))))))))))))))) + : nat +Nat.add (S O) (S (S O)) + : nat +match + String (Ascii.Ascii true false false false false true true false) + EmptyString +with +| String (Ascii.Ascii true false false false false true true false) + EmptyString => true +| _ => false +end + : bool +match S O with +| S O => true +| _ => false +end + : bool +{| field := S (S (S (S (S (S (S O)))))) |} + : test diff --git a/test-suite/output/primitive_tokens.v b/test-suite/output/primitive_tokens.v new file mode 100644 index 0000000000..3207e5983f --- /dev/null +++ b/test-suite/output/primitive_tokens.v @@ -0,0 +1,23 @@ +Require Import String. + +Record test := { field : nat }. + +Open Scope string_scope. + +Unset Printing Notations. + +Check "foo". +Check 1234. +Check 1 + 2. +Check match "a" with "a" => true | _ => false end. +Check match 1 with 1 => true | _ => false end. +Check {| field := 7 |}. + +Set Printing Raw Literals. + +Check "foo". +Check 1234. +Check 1 + 2. +Check match "a" with "a" => true | _ => false end. +Check match 1 with 1 => true | _ => false end. +Check {| field := 7 |}. diff --git a/test-suite/output/relaxed_ambiguous_paths.out b/test-suite/output/relaxed_ambiguous_paths.out index ac5a09bad7..48368c7ede 100644 --- a/test-suite/output/relaxed_ambiguous_paths.out +++ b/test-suite/output/relaxed_ambiguous_paths.out @@ -3,32 +3,32 @@ Warning: New coercion path [ac; cd] : A >-> D is ambiguous with existing [ab; bd] : A >-> D. [ambiguous-paths,typechecker] [ab] : A >-> B -[ab; bd] : A >-> D [ac] : A >-> C +[ab; bd] : A >-> D [bd] : B >-> D [cd] : C >-> D File "stdin", line 26, characters 0-28: Warning: New coercion path [ab; bc] : A >-> C is ambiguous with existing [ac] : A >-> C. [ambiguous-paths,typechecker] +[ab] : A >-> B [ac] : A >-> C [ac; cd] : A >-> D -[ab] : A >-> B -[cd] : C >-> D [bc] : B >-> C [bc; cd] : B >-> D +[cd] : C >-> D [B_A] : B >-> A [C_A] : C >-> A -[D_B] : D >-> B [D_A] : D >-> A +[D_B] : D >-> B [D_C] : D >-> C [A'_A] : A' >-> A -[B_A'] : B >-> A' [B_A'; A'_A] : B >-> A -[C_A'] : C >-> A' +[B_A'] : B >-> A' [C_A'; A'_A] : C >-> A -[D_B; B_A'] : D >-> A' +[C_A'] : C >-> A' [D_A] : D >-> A +[D_B; B_A'] : D >-> A' [D_B] : D >-> B [D_C] : D >-> C File "stdin", line 121, characters 0-86: @@ -36,12 +36,12 @@ Warning: New coercion path [D_C; C_A'] : D >-> A' is ambiguous with existing [D_B; B_A'] : D >-> A'. [ambiguous-paths,typechecker] [A'_A] : A' >-> A -[B_A'] : B >-> A' [B_A'; A'_A] : B >-> A -[C_A'] : C >-> A' +[B_A'] : B >-> A' [C_A'; A'_A] : C >-> A -[D_B; B_A'] : D >-> A' +[C_A'] : C >-> A' [D_A] : D >-> A +[D_B; B_A'] : D >-> A' [D_B] : D >-> B [D_C] : D >-> C File "stdin", line 130, characters 0-47: diff --git a/test-suite/output/set.out b/test-suite/output/set.out index 4b72d73eb3..61f3c52656 100644 --- a/test-suite/output/set.out +++ b/test-suite/output/set.out @@ -1,16 +1,16 @@ -1 subgoal +1 goal y1 := 0 : nat x := 0 + 0 : nat ============================ x = x -1 subgoal +1 goal y1, y2 := 0 : nat x := y2 + 0 : nat ============================ x = x -1 subgoal +1 goal y1, y2, y3 := 0 : nat x := y2 + y3 : nat diff --git a/test-suite/output/simpl.out b/test-suite/output/simpl.out index 526e468f5b..fd35c5e339 100644 --- a/test-suite/output/simpl.out +++ b/test-suite/output/simpl.out @@ -1,14 +1,14 @@ -1 subgoal +1 goal x : nat ============================ x = S x -1 subgoal +1 goal x : nat ============================ 0 + x = S x -1 subgoal +1 goal x : nat ============================ diff --git a/test-suite/output/subst.out b/test-suite/output/subst.out index 209b2bc26f..9cc515b7ba 100644 --- a/test-suite/output/subst.out +++ b/test-suite/output/subst.out @@ -1,4 +1,4 @@ -1 subgoal +1 goal y, z : nat Hy : y = 0 @@ -11,7 +11,7 @@ H4 : z = 4 ============================ True -1 subgoal +1 goal x, z : nat Hx : x = 0 @@ -24,7 +24,7 @@ H4 : z = 4 ============================ True -1 subgoal +1 goal x, y : nat Hx : x = 0 @@ -37,7 +37,7 @@ H4 : 0 = 4 ============================ True -1 subgoal +1 goal H1 : 0 = 1 HA : True @@ -47,7 +47,7 @@ H4 : 0 = 4 ============================ True -1 subgoal +1 goal y, z : nat Hy : y = 0 @@ -60,7 +60,7 @@ H2 : 0 = 2 ============================ True -1 subgoal +1 goal x, z : nat Hx : x = 0 @@ -73,7 +73,7 @@ H3 : 0 = 3 ============================ True -1 subgoal +1 goal x, y : nat Hx : x = 0 @@ -86,7 +86,7 @@ H4 : 0 = 4 ============================ True -1 subgoal +1 goal HA, HB : True H4 : 0 = 4 diff --git a/test-suite/output/unifconstraints.out b/test-suite/output/unifconstraints.out index 2fadd747b7..abcb8d7e0c 100644 --- a/test-suite/output/unifconstraints.out +++ b/test-suite/output/unifconstraints.out @@ -1,44 +1,44 @@ -3 focused subgoals +3 focused goals (shelved: 1) ============================ ?Goal 0 -subgoal 2 is: +goal 2 is: forall n : nat, ?Goal n -> ?Goal (S n) -subgoal 3 is: +goal 3 is: nat unification constraint: ?Goal ?Goal2 <= True /\ True /\ True \/ veeryyyyyyyyyyyyloooooooooooooonggidentifier = veeryyyyyyyyyyyyloooooooooooooonggidentifier -3 focused subgoals +3 focused goals (shelved: 1) n, m : nat ============================ ?Goal@{n:=n; m:=m} 0 -subgoal 2 is: +goal 2 is: forall n0 : nat, ?Goal@{n:=n; m:=m} n0 -> ?Goal@{n:=n; m:=m} (S n0) -subgoal 3 is: +goal 3 is: nat unification constraint: ?Goal@{n:=n; m:=m} ?Goal2@{n:=n; m:=m} <= True /\ True /\ True \/ veeryyyyyyyyyyyyloooooooooooooonggidentifier = veeryyyyyyyyyyyyloooooooooooooonggidentifier -3 focused subgoals +3 focused goals (shelved: 1) m : nat ============================ ?Goal1@{m:=m} 0 -subgoal 2 is: +goal 2 is: forall n0 : nat, ?Goal1@{m:=m} n0 -> ?Goal1@{m:=m} (S n0) -subgoal 3 is: +goal 3 is: nat unification constraint: @@ -46,16 +46,16 @@ unification constraint: True /\ True /\ True \/ veeryyyyyyyyyyyyloooooooooooooonggidentifier = veeryyyyyyyyyyyyloooooooooooooonggidentifier -3 focused subgoals +3 focused goals (shelved: 1) m : nat ============================ ?Goal0@{m:=m} 0 -subgoal 2 is: +goal 2 is: forall n0 : nat, ?Goal0@{m:=m} n0 -> ?Goal0@{m:=m} (S n0) -subgoal 3 is: +goal 3 is: nat unification constraint: diff --git a/test-suite/output/unification.out b/test-suite/output/unification.out index cf31871e5a..4db5c2d161 100644 --- a/test-suite/output/unification.out +++ b/test-suite/output/unification.out @@ -9,25 +9,25 @@ Unable to unify "T" with "?X@{x0:=x; x:=C a}" (cannot instantiate The command has indeed failed with message: The term "id" has type "ID" while it is expected to have type "Type -> ?T" (cannot instantiate "?T" because "A" is not in its scope). -1 focused subgoal +1 focused goal (shelved: 1) H : forall x : nat, S (S (S x)) = x ============================ ?x = 0 -1 focused subgoal +1 focused goal (shelved: 1) H : forall x : nat, S (S (S x)) = x ============================ ?x = 0 -1 focused subgoal +1 focused goal (shelved: 1) H : forall x : nat, S (S (S x)) = x ============================ ?x = 0 -1 focused subgoal +1 focused goal (shelved: 1) H : forall x : nat, S x = x |