diff options
Diffstat (limited to 'test-suite/output')
31 files changed, 361 insertions, 96 deletions
diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out index 01564e7f25..ea647a990a 100644 --- a/test-suite/output/Cases.out +++ b/test-suite/output/Cases.out @@ -50,10 +50,11 @@ f = fun H : B => match H with | AC x => - let b0 := b in - (if b0 as b return (P b -> True) - then fun _ : P true => Logic.I - else fun _ : P false => Logic.I) x + (fun x0 : P b => + let b0 := b in + (if b0 as b return (P b -> True) + then fun _ : P true => Logic.I + else fun _ : P false => Logic.I) x0) x end : B -> True The command has indeed failed with message: @@ -74,7 +75,9 @@ fun '{{n, m, p}} => n + m + p fun '(D n m p q) => n + m + p + q : J -> nat The command has indeed failed with message: -The constructor D (in type J) expects 3 arguments. +Once notations are expanded, the resulting constructor D (in type J) is +expected to be applied to no arguments while it is actually applied to +1 argument. lem1 = fun dd : nat * nat => let (bb, cc) as aa return (aa = aa) := dd in eq_refl : forall k : nat * nat, k = k @@ -86,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 @@ -106,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, @@ -181,3 +184,51 @@ end File "stdin", line 253, characters 4-5: Warning: Unused variable B catches more than one case. [unused-pattern-matching-variable,pattern-matching] +The command has indeed failed with message: +Application of arguments to a recursive notation not supported in patterns. +The command has indeed failed with message: +The constructor cons (in type list) is expected to be applied to 2 arguments +while it is actually applied to 3 arguments. +The command has indeed failed with message: +The constructor cons (in type list) is expected to be applied to 2 arguments +while it is actually applied to 1 argument. +The command has indeed failed with message: +The constructor D' (in type J') is expected to be applied to 4 arguments (or +6 arguments when including variables for local definitions) while it is +actually applied to 5 arguments. +fun x : J' bool (true, true) => +match x with +| D' _ _ _ m _ e => existT (fun x0 : nat => x0 = x0) m e +end + : J' bool (true, true) -> {x0 : nat & x0 = x0} +fun x : J' bool (true, true) => +match x with +| @D' _ _ _ _ n _ p _ => n + p +end + : J' bool (true, true) -> nat +The command has indeed failed with message: +Application of arguments to a recursive notation not supported in patterns. +The command has indeed failed with message: +The constructor cons (in type list) is expected to be applied to 2 arguments +while it is actually applied to 3 arguments. +The command has indeed failed with message: +The constructor cons (in type list) is expected to be applied to 2 arguments +while it is actually applied to 1 argument. +The command has indeed failed with message: +The constructor D' (in type J') is expected to be applied to 3 arguments (or +4 arguments when including variables for local definitions) while it is +actually applied to 2 arguments. +The command has indeed failed with message: +The constructor D' (in type J') is expected to be applied to 3 arguments (or +4 arguments when including variables for local definitions) while it is +actually applied to 5 arguments. +fun x : J' bool (true, true) => +match x with +| @D' _ _ _ _ _ m _ e => existT (fun x0 : nat => x0 = x0) m e +end + : J' bool (true, true) -> {x0 : nat & x0 = x0} +fun x : J' bool (true, true) => +match x with +| @D' _ _ _ _ n _ p _ => (n, p) +end + : J' bool (true, true) -> nat * nat diff --git a/test-suite/output/Cases.v b/test-suite/output/Cases.v index 2d8a8b359c..0cb3ac3ddc 100644 --- a/test-suite/output/Cases.v +++ b/test-suite/output/Cases.v @@ -254,3 +254,33 @@ Definition bar (f : foo) := end. End Wish12762. + +Module ConstructorArgumentsNumber. + +Arguments cons {A} _ _. + +Inductive J' A {B} (C:=(A*B)%type) (c:C) := D' : forall n {m}, let p := n+m in m=m -> J' A c. + +Unset Asymmetric Patterns. + +Fail Check fun x => match x with (y,z) w => y+z+w end. +Fail Check fun x => match x with cons y z w => 0 | nil => 0 end. +Fail Check fun x => match x with cons y => 0 | nil => 0 end. + +(* Missing a let-in to be in let-in mode *) +Fail Check fun x => match x with D' _ _ n p e => 0 end. +Check fun x : J' bool (true,true) => match x with D' _ _ n e => existT (fun x => eq x x) _ e end. +Check fun x : J' bool (true,true) => match x with D' _ _ _ n p e => n+p end. + +Set Asymmetric Patterns. + +Fail Check fun x => match x with (y,z) w => y+z+w end. +Fail Check fun x => match x with cons y z w => 0 | nil => 0 end. +Fail Check fun x => match x with cons y => 0 | nil => 0 end. + +Fail Check fun x => match x with D' n _ => 0 end. +Fail Check fun x => match x with D' n m p e _ => 0 end. +Check fun x : J' bool (true,true) => match x with D' n m e => existT (fun x => eq x x) m e end. +Check fun x : J' bool (true,true) => match x with D' n m p e => (n,p) end. + +End ConstructorArgumentsNumber. 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/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..60213cab0c 100644 --- a/test-suite/output/Notations3.out +++ b/test-suite/output/Notations3.out @@ -238,7 +238,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/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/RecordFieldErrors.out b/test-suite/output/RecordFieldErrors.out index 5b67f632c9..b80345108e 100644 --- a/test-suite/output/RecordFieldErrors.out +++ b/test-suite/output/RecordFieldErrors.out @@ -11,4 +11,4 @@ This record defines several times the field foo. The command has indeed failed with message: This record defines several times the field unit. The command has indeed failed with message: -unit: Not a projection of inductive t. +unit: Not a projection. diff --git a/test-suite/output/RecordFieldErrors.v b/test-suite/output/RecordFieldErrors.v index 27aa07822b..ff817c31aa 100644 --- a/test-suite/output/RecordFieldErrors.v +++ b/test-suite/output/RecordFieldErrors.v @@ -35,4 +35,4 @@ acceptable and seems an unlikely mistake. *) Fail Check {| foo := tt; unit := tt |}. -(* unit: Not a projection of inductive t. *) +(* unit: Not a projection. *) 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/StringSyntaxPrimitive.out b/test-suite/output/StringSyntaxPrimitive.out new file mode 100644 index 0000000000..131975c760 --- /dev/null +++ b/test-suite/output/StringSyntaxPrimitive.out @@ -0,0 +1,20 @@ +"abc" + : intList +"abc" + : intList +mk_intList [97%int63; 98%int63; 99%int63] + : intList +"abc" + : intArray +"abc" + : intArray + = "abc" + : nestArray +"abc" + : nestArray +"100" + : floatList +"100" + : floatList +mk_floatList [1%float; 0%float; 0%float] + : floatList diff --git a/test-suite/output/StringSyntaxPrimitive.v b/test-suite/output/StringSyntaxPrimitive.v new file mode 100644 index 0000000000..23ef082013 --- /dev/null +++ b/test-suite/output/StringSyntaxPrimitive.v @@ -0,0 +1,139 @@ +Require Import Coq.Lists.List. +Require Import Coq.Strings.String Coq.Strings.Byte Coq.Strings.Ascii. +Require Coq.Array.PArray Coq.Floats.PrimFloat. +Require Import Coq.Numbers.BinNums Coq.Numbers.Cyclic.Int63.Int63. + +Set Printing Depth 100000. +Set Printing Width 1000. + +Close Scope char_scope. +Close Scope string_scope. + +(* Notations for primitive integers inside polymorphic datatypes *) +Module Test1. + Inductive intList := mk_intList (_ : list int). + Definition i63_from_byte (b : byte) : int := Int63.of_Z (BinInt.Z.of_N (Byte.to_N b)). + Definition i63_to_byte (i : int) : byte := + match Byte.of_N (BinInt.Z.to_N (Int63.to_Z i)) with Some x => x | None => x00%byte end. + + Definition to_byte_list '(mk_intList a) := List.map i63_to_byte a. + + Definition from_byte_list (xs : list byte) : intList:= + mk_intList (List.map i63_from_byte xs). + + Declare Scope intList_scope. + Delimit Scope intList_scope with intList. + + String Notation intList from_byte_list to_byte_list : intList_scope. + + Open Scope intList_scope. + Import List.ListNotations. + Check mk_intList [97; 98; 99]%int63%list. + Check "abc"%intList. + + Definition int' := int. + Check mk_intList (@cons int' 97 [98; 99])%int63%list. +End Test1. + +Import PArray. + +(* Notations for primitive arrays *) +Module Test2. + Inductive intArray := mk_intArray (_ : array int). + + Definition i63_from_byte (b : byte) : Int63.int := Int63.of_Z (BinInt.Z.of_N (Byte.to_N b)). + Definition i63_to_byte (i : Int63.int) : byte := + match Byte.of_N (BinInt.Z.to_N (Int63.to_Z i)) with Some x => x | None => x00%byte end. + + Definition i63_to_nat x := BinInt.Z.to_nat (Int63.to_Z x). + Local Definition nat_length {X} (x : array X) :nat := i63_to_nat (length x). + + Local Fixpoint list_length_i63 {A} (xs : list A) :int := + match xs with + | nil => 0 + | cons _ xs => 1 + list_length_i63 xs + end. + + Definition to_byte_list '(mk_intArray a) := + ((fix go (n : nat) (i : Int63.int) (acc : list byte) := + match n with + | 0 => acc + | S n => go n (i - 1) (cons (i63_to_byte a.[i]) acc) + end) (nat_length a) (length a - 1) nil)%int63. + + Definition from_byte_list (xs : list byte) := + (let arr := make (list_length_i63 xs) 0 in + mk_intArray ((fix go i xs acc := + match xs with + | nil => acc + | cons x xs => go (i + 1) xs (acc.[i <- i63_from_byte x]) + end) 0 xs arr))%int63. + + Declare Scope intArray_scope. + Delimit Scope intArray_scope with intArray. + + String Notation intArray from_byte_list to_byte_list : intArray_scope. + + Open Scope intArray_scope. + Check mk_intArray ( [| 97; 98; 99 | 0|])%int63%array. + Check "abc"%intArray. + +End Test2. + +(* Primitive arrays inside primitive arrays *) +Module Test3. + + Inductive nestArray := mk_nestArray (_ : array (array int)). + Definition to_byte_list '(mk_nestArray a) := + ((fix go (n : nat) (i : Int63.int) (acc : list byte) := + match n with + | 0 => acc + | S n => go n (i - 1) (cons (Test2.i63_to_byte a.[i].[0]) acc) + end) (Test2.nat_length a) (length a - 1) nil)%int63. + + Definition from_byte_list (xs : list byte) := + (let arr := make (Test2.list_length_i63 xs) (make 0 0) in + mk_nestArray ((fix go i xs acc := + match xs with + | nil => acc + | cons x xs => go (i + 1) xs (acc.[i <- make 1 (Test2.i63_from_byte x)]) + end) 0 xs arr))%int63. + + Declare Scope nestArray_scope. + Delimit Scope nestArray_scope with nestArray. + + String Notation nestArray from_byte_list to_byte_list : nestArray_scope. + + Open Scope nestArray_scope. + Eval cbv in mk_nestArray ( [| make 1 97; make 1 98; make 1 99 | make 0 0|])%int63%array. + Check "abc"%nestArray. +End Test3. + + + +(* Notations for primitive floats inside polymorphic datatypes *) +Module Test4. + Import PrimFloat. + Inductive floatList := mk_floatList (_ : list float). + Definition float_from_byte (b : byte) : float := + if Byte.eqb b "0"%byte then PrimFloat.zero else PrimFloat.one. + Definition float_to_byte (f : float) : byte := + if PrimFloat.is_zero f then "0" else "1". + Definition to_byte_list '(mk_floatList a) := List.map float_to_byte a. + + Definition from_byte_list (xs : list byte) : floatList:= + mk_floatList (List.map float_from_byte xs). + + Declare Scope floatList_scope. + Delimit Scope floatList_scope with floatList. + + String Notation floatList from_byte_list to_byte_list : floatList_scope. + + Open Scope floatList_scope. + Import List.ListNotations. + Check mk_floatList [97; 0; 0]%float%list. + Check "100"%floatList. + + Definition float' := float. + Check mk_floatList (@cons float' 1 [0; 0])%float%list. +End Test4. 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 0fbb4f4c11..95b6c6ee95 100644 --- a/test-suite/output/UnivBinders.out +++ b/test-suite/output/UnivBinders.out @@ -162,6 +162,9 @@ When declaring multiple axioms in one command, only the first is allowed a unive foo@{i} = Type@{M.i} -> Type@{i} : Type@{max(M.i+1,i+1)} (* i |= *) +Type@{u0} -> Type@{UnivBinders.64} + : Type@{max(u0+1,UnivBinders.64+1)} +(* {UnivBinders.64} |= *) bind_univs.mono = Type@{bind_univs.mono.u} : Type@{bind_univs.mono.u+1} diff --git a/test-suite/output/UnivBinders.v b/test-suite/output/UnivBinders.v index ed6e90b2a6..9539e34cfe 100644 --- a/test-suite/output/UnivBinders.v +++ b/test-suite/output/UnivBinders.v @@ -161,6 +161,16 @@ Module Notas. End Notas. +Module NoAutoNames. + Monomorphic Universe u0. + + (* The anonymous universe doesn't get a name (names are only + invented at the end of a definition/inductive) so no need to + qualify u0. *) + Check (Type@{u0} -> Type). + +End NoAutoNames. + (* Universe binders survive through compilation, sections and modules. *) Require TestSuite.bind_univs. Print bind_univs.mono. diff --git a/test-suite/output/bug_12908.v b/test-suite/output/bug_12908.v index 6f7be22fa0..7ab218a27a 100644 --- a/test-suite/output/bug_12908.v +++ b/test-suite/output/bug_12908.v @@ -7,7 +7,7 @@ Check forall m n, mult' m n = Nat.mul (Nat.mul 2 m) n. End A. Module B. -(* Test that an overriden scoped notation is deactivated *) +(* Test that an overridden scoped notation is deactivated *) Infix "*" := mult' : nat_scope. Check forall m n, mult' m n = Nat.mul (Nat.mul 2 m) n. End B. diff --git a/test-suite/output/bug_13595.out b/test-suite/output/bug_13595.out new file mode 100644 index 0000000000..2423b77b55 --- /dev/null +++ b/test-suite/output/bug_13595.out @@ -0,0 +1,4 @@ +The command has indeed failed with message: +Tactic failure: Goal is solvable by congruence but some arguments are missing. + Try "congruence with ((Triple a _ _)) ((Triple d c _))", + replacing metavariables by arbitrary terms. diff --git a/test-suite/output/bug_13595.v b/test-suite/output/bug_13595.v new file mode 100644 index 0000000000..27a9ebe15d --- /dev/null +++ b/test-suite/output/bug_13595.v @@ -0,0 +1,8 @@ +Inductive Cube:Set :=| Triple: nat -> nat -> nat -> Cube. + +Theorem incomplete :forall a b c d : nat,Triple a = Triple b->Triple d c = Triple d b->a = c. +Proof. + Fail congruence. + intros. + congruence with ((Triple a a a)) ((Triple d c a)). +Qed. 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/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 |