aboutsummaryrefslogtreecommitdiff
path: root/test-suite/output
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/output')
-rw-r--r--test-suite/output/Cases.out3
-rw-r--r--test-suite/output/Cases.v12
-rw-r--r--test-suite/output/DependentInductionErrors.out4
-rw-r--r--test-suite/output/DependentInductionErrors.v17
-rw-r--r--test-suite/output/ErrorLocation_13241_1.out3
-rw-r--r--test-suite/output/ErrorLocation_13241_1.v5
-rw-r--r--test-suite/output/ErrorLocation_13241_2.out3
-rw-r--r--test-suite/output/ErrorLocation_13241_2.v5
-rw-r--r--test-suite/output/Notations4.out4
-rw-r--r--test-suite/output/Record.out40
-rw-r--r--test-suite/output/Record.v31
-rw-r--r--test-suite/output/bug_13004.out4
-rw-r--r--test-suite/output/bug_13238.out4
-rw-r--r--test-suite/output/bug_13238.v13
-rw-r--r--test-suite/output/goal_output.out74
-rw-r--r--test-suite/output/goal_output.v28
-rw-r--r--test-suite/output/prim_array.out9
-rw-r--r--test-suite/output/prim_array.v10
18 files changed, 262 insertions, 7 deletions
diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out
index da2fc90fc3..01564e7f25 100644
--- a/test-suite/output/Cases.out
+++ b/test-suite/output/Cases.out
@@ -178,3 +178,6 @@ match N with
| _ => Node
end
: Tree -> Tree
+File "stdin", line 253, characters 4-5:
+Warning: Unused variable B catches more than one case.
+[unused-pattern-matching-variable,pattern-matching]
diff --git a/test-suite/output/Cases.v b/test-suite/output/Cases.v
index 262ec2b677..2d8a8b359c 100644
--- a/test-suite/output/Cases.v
+++ b/test-suite/output/Cases.v
@@ -242,3 +242,15 @@ end.
Print stray.
End Bug11231.
+
+Module Wish12762.
+
+Inductive foo := a | b | c.
+
+Definition bar (f : foo) :=
+ match f with
+ | a => 0
+ | B => 1
+ end.
+
+End Wish12762.
diff --git a/test-suite/output/DependentInductionErrors.out b/test-suite/output/DependentInductionErrors.out
new file mode 100644
index 0000000000..4a83375f6f
--- /dev/null
+++ b/test-suite/output/DependentInductionErrors.out
@@ -0,0 +1,4 @@
+The command has indeed failed with message:
+Tactic failure: To use dependent destruction, first [Require Import Coq.Program.Equality.].
+The command has indeed failed with message:
+Tactic failure: To use dependent induction, first [Require Import Coq.Program.Equality.].
diff --git a/test-suite/output/DependentInductionErrors.v b/test-suite/output/DependentInductionErrors.v
new file mode 100644
index 0000000000..2fce00f9fd
--- /dev/null
+++ b/test-suite/output/DependentInductionErrors.v
@@ -0,0 +1,17 @@
+Theorem foo (b:bool) : b = true \/ b = false.
+Proof.
+ Fail dependent destruction b.
+ Fail dependent induction b.
+Abort.
+
+From Coq Require Import Program.Equality.
+
+Theorem foo_with_destruction (b:bool) : b = true \/ b = false.
+Proof.
+ dependent destruction b; auto.
+Qed.
+
+Theorem foo_with_induction (b:bool) : b = true \/ b = false.
+Proof.
+ dependent induction b; auto.
+Qed.
diff --git a/test-suite/output/ErrorLocation_13241_1.out b/test-suite/output/ErrorLocation_13241_1.out
new file mode 100644
index 0000000000..d899dd5d46
--- /dev/null
+++ b/test-suite/output/ErrorLocation_13241_1.out
@@ -0,0 +1,3 @@
+File "stdin", line 4, characters 0-1:
+Error: No product even after head-reduction.
+
diff --git a/test-suite/output/ErrorLocation_13241_1.v b/test-suite/output/ErrorLocation_13241_1.v
new file mode 100644
index 0000000000..3102b13fb8
--- /dev/null
+++ b/test-suite/output/ErrorLocation_13241_1.v
@@ -0,0 +1,5 @@
+Ltac a := intro.
+Ltac b := a.
+Goal True.
+b.
+Abort.
diff --git a/test-suite/output/ErrorLocation_13241_2.out b/test-suite/output/ErrorLocation_13241_2.out
new file mode 100644
index 0000000000..d899dd5d46
--- /dev/null
+++ b/test-suite/output/ErrorLocation_13241_2.out
@@ -0,0 +1,3 @@
+File "stdin", line 4, characters 0-1:
+Error: No product even after head-reduction.
+
diff --git a/test-suite/output/ErrorLocation_13241_2.v b/test-suite/output/ErrorLocation_13241_2.v
new file mode 100644
index 0000000000..b82f36ed6f
--- /dev/null
+++ b/test-suite/output/ErrorLocation_13241_2.v
@@ -0,0 +1,5 @@
+Ltac a _ := intro.
+Ltac b := a ().
+Goal True.
+b.
+Abort.
diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out
index a42518822f..fa0c20bf73 100644
--- a/test-suite/output/Notations4.out
+++ b/test-suite/output/Notations4.out
@@ -8,7 +8,7 @@ Entry custom:myconstr is
| "4" RIGHTA
[ SELF; "*"; NEXT ]
| "3" RIGHTA
- [ "<"; operconstr LEVEL "10"; ">" ] ]
+ [ "<"; term LEVEL "10"; ">" ] ]
[< b > + < b > * < 2 >]
: nat
@@ -77,7 +77,7 @@ The command has indeed failed with message:
The format is not the same on the right- and left-hand sides of the special token "..".
Entry custom:expr is
[ "201" RIGHTA
- [ "{"; operconstr LEVEL "200"; "}" ] ]
+ [ "{"; term LEVEL "200"; "}" ] ]
fun x : nat => [ x ]
: nat -> nat
diff --git a/test-suite/output/Record.out b/test-suite/output/Record.out
index d45343fe60..7de1e7d559 100644
--- a/test-suite/output/Record.out
+++ b/test-suite/output/Record.out
@@ -30,3 +30,43 @@ fun '{| U := T; a := a; q := p |} => (T, p, a)
: M -> Type * True * nat
fun '{| U := T; a := a; q := p |} => (T, p, a)
: M -> Type * True * nat
+{| a := 0; b := 0 |}
+ : T
+fun '{| |} => 0
+ : LongModuleName.test -> nat
+ = {|
+ a :=
+ {|
+ LongModuleName.long_field_name0 := 0;
+ LongModuleName.long_field_name1 := 1;
+ LongModuleName.long_field_name2 := 2;
+ LongModuleName.long_field_name3 := 3
+ |};
+ b :=
+ fun
+ '{|
+ LongModuleName.long_field_name0 := a;
+ LongModuleName.long_field_name1 := b;
+ LongModuleName.long_field_name2 := c;
+ LongModuleName.long_field_name3 := d
+ |} => (a, b, c, d)
+ |}
+ : T
+ = {|
+ a :=
+ {|
+ long_field_name0 := 0;
+ long_field_name1 := 1;
+ long_field_name2 := 2;
+ long_field_name3 := 3
+ |};
+ b :=
+ fun
+ '{|
+ long_field_name0 := a;
+ long_field_name1 := b;
+ long_field_name2 := c;
+ long_field_name3 := d
+ |} => (a, b, c, d)
+ |}
+ : T
diff --git a/test-suite/output/Record.v b/test-suite/output/Record.v
index 71a8afa131..13ea37b11e 100644
--- a/test-suite/output/Record.v
+++ b/test-suite/output/Record.v
@@ -33,3 +33,34 @@ Check fun x:M => let 'D T _ p := x in T.
Check fun x:M => let 'D T p := x in (T,p).
Check fun x:M => let 'D T a p := x in (T,p,a).
Check fun x:M => let '{|U:=T;a:=a;q:=p|} := x in (T,p,a).
+
+Module FormattingIssue13142.
+
+Record T {A B} := {a:A;b:B}.
+
+Module LongModuleName.
+ Record test := { long_field_name0 : nat;
+ long_field_name1 : nat;
+ long_field_name2 : nat;
+ long_field_name3 : nat }.
+End LongModuleName.
+
+Definition c :=
+ {| LongModuleName.long_field_name0 := 0;
+ LongModuleName.long_field_name1 := 1;
+ LongModuleName.long_field_name2 := 2;
+ LongModuleName.long_field_name3 := 3 |}.
+
+Definition d :=
+ fun '{| LongModuleName.long_field_name0 := a;
+ LongModuleName.long_field_name1 := b;
+ LongModuleName.long_field_name2 := c;
+ LongModuleName.long_field_name3 := d |} => (a,b,c,d).
+
+Check {|a:=0;b:=0|}.
+Check fun '{| LongModuleName.long_field_name0:=_ |} => 0.
+Eval compute in {|a:=c;b:=d|}.
+Import LongModuleName.
+Eval compute in {|a:=c;b:=d|}.
+
+End FormattingIssue13142.
diff --git a/test-suite/output/bug_13004.out b/test-suite/output/bug_13004.out
index 2bd7d67535..28bc580202 100644
--- a/test-suite/output/bug_13004.out
+++ b/test-suite/output/bug_13004.out
@@ -1,2 +1,2 @@
-Ltac bug_13004.t := ltac2:(print (of_string "hi"))
-Ltac bug_13004.u := ident:(H)
+Ltac t := ltac2:(print (of_string "hi"))
+Ltac u := ident:(H)
diff --git a/test-suite/output/bug_13238.out b/test-suite/output/bug_13238.out
new file mode 100644
index 0000000000..a17d05200d
--- /dev/null
+++ b/test-suite/output/bug_13238.out
@@ -0,0 +1,4 @@
+Ltac t1 x := replace (x x) with (x x)
+Ltac t2 x := case : x
+Ltac t3 := by move ->
+Ltac t4 := congr True
diff --git a/test-suite/output/bug_13238.v b/test-suite/output/bug_13238.v
new file mode 100644
index 0000000000..9b8063bf13
--- /dev/null
+++ b/test-suite/output/bug_13238.v
@@ -0,0 +1,13 @@
+Require Import ssreflect.
+
+Ltac t1 x := replace (x x) with (x x).
+Print t1.
+
+Ltac t2 x := case: x.
+Print t2.
+
+Ltac t3 := by move->.
+Print t3.
+
+Ltac t4 := congr True.
+Print t4.
diff --git a/test-suite/output/goal_output.out b/test-suite/output/goal_output.out
index 773533a8d3..17c1aaa55b 100644
--- a/test-suite/output/goal_output.out
+++ b/test-suite/output/goal_output.out
@@ -2,7 +2,79 @@ Nat.t = nat
: Set
Nat.t = nat
: Set
+2 subgoals
+
+ ============================
+ True
+
+subgoal 2 is:
+ True
+2 subgoals, subgoal 1 (?Goal)
+
+ ============================
+ True
+
+subgoal 2 (?Goal0) is:
+ True
1 subgoal
============================
- False
+ True
+1 subgoal (?Goal0)
+
+ ============================
+ True
+1 subgoal (?Goal0)
+
+ ============================
+ True
+
+*** Unfocused goals:
+
+subgoal 2 (?Goal1) is:
+ True
+subgoal 3 (?Goal) is:
+ True
+1 subgoal
+
+ ============================
+ True
+
+*** Unfocused goals:
+
+subgoal 2 is:
+ True
+subgoal 3 is:
+ True
+This subproof is complete, but there are some unfocused goals.
+Focus next goal with bullet -.
+
+2 subgoals
+
+subgoal 1 is:
+ True
+subgoal 2 is:
+ True
+This subproof is complete, but there are some unfocused goals.
+Focus next goal with bullet -.
+
+2 subgoals
+
+subgoal 1 (?Goal0) is:
+ True
+subgoal 2 (?Goal) is:
+ True
+This subproof is complete, but there are some unfocused goals.
+Focus next goal with bullet -.
+
+1 subgoal
+
+subgoal 1 is:
+ True
+This subproof is complete, but there are some unfocused goals.
+Focus next goal with bullet -.
+
+1 subgoal
+
+subgoal 1 (?Goal) is:
+ True
diff --git a/test-suite/output/goal_output.v b/test-suite/output/goal_output.v
index 327b80b0aa..b1ced94054 100644
--- a/test-suite/output/goal_output.v
+++ b/test-suite/output/goal_output.v
@@ -6,8 +6,32 @@
Print Nat.t.
Timeout 1 Print Nat.t.
-Lemma toto: False.
Set Printing All.
+Lemma toto: True/\True.
+Proof.
+split.
Show.
+Set Printing Goal Names.
+Show.
+Unset Printing Goal Names.
+assert True.
+- idtac.
+Show.
+Set Printing Goal Names.
+Show.
+Set Printing Unfocused.
+Show.
+Unset Printing Goal Names.
+Show.
+Unset Printing Unfocused.
+ auto.
+Show.
+Set Printing Goal Names.
+Show.
+Unset Printing Goal Names.
+- auto.
+Show.
+Set Printing Goal Names.
+Show.
+Unset Printing Goal Names.
Abort.
-
diff --git a/test-suite/output/prim_array.out b/test-suite/output/prim_array.out
new file mode 100644
index 0000000000..6c12153ab9
--- /dev/null
+++ b/test-suite/output/prim_array.out
@@ -0,0 +1,9 @@
+[| | 0 : nat |]
+ : array nat
+[| 1; 2; 3 | 0 : nat |]
+ : array nat
+[| | 0 : nat |]@{Set}
+ : array@{Set} nat
+[| bool; list nat | nat : Set |]@{prim_array.4}
+ : array@{prim_array.4} Set
+(* {prim_array.4} |= Set < prim_array.4 *)
diff --git a/test-suite/output/prim_array.v b/test-suite/output/prim_array.v
new file mode 100644
index 0000000000..a82f6a16f1
--- /dev/null
+++ b/test-suite/output/prim_array.v
@@ -0,0 +1,10 @@
+Primitive array := #array_type.
+
+Check [| | 0 |].
+
+Check [| 1; 2; 3 | 0 |].
+
+Set Printing Universes.
+Check [| | 0 |].
+
+Check [| bool; list nat | nat |].
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 21:56:07 +0000