aboutsummaryrefslogtreecommitdiff
path: root/test-suite/output
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/output')
-rw-r--r--test-suite/output/Notations3.out10
-rw-r--r--test-suite/output/RecordProjParameter.out33
-rw-r--r--test-suite/output/RecordProjParameter.v21
-rw-r--r--test-suite/output/bug_13240.out3
-rw-r--r--test-suite/output/bug_13240.v10
-rw-r--r--test-suite/output/ltac2_deprecated.out12
-rw-r--r--test-suite/output/ltac2_deprecated.v15
-rw-r--r--test-suite/output/primitive_tokens.out61
-rw-r--r--test-suite/output/primitive_tokens.v23
-rw-r--r--test-suite/output/relaxed_ambiguous_paths.out66
-rw-r--r--test-suite/output/relaxed_ambiguous_paths.v72
11 files changed, 276 insertions, 50 deletions
diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out
index 60213cab0c..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)
diff --git a/test-suite/output/RecordProjParameter.out b/test-suite/output/RecordProjParameter.out
new file mode 100644
index 0000000000..91ae4b6511
--- /dev/null
+++ b/test-suite/output/RecordProjParameter.out
@@ -0,0 +1,33 @@
+t1 : Atype -> forall a : Type, a
+
+t1 is not universe polymorphic
+Arguments t1 _ _%type_scope
+t1 is transparent
+Expands to: Constant RecordProjParameter.t1
+t3 : forall a0 : Atype, t2 a0
+
+t3 is not universe polymorphic
+t3 is transparent
+Expands to: Constant RecordProjParameter.t3
+u1 : Btype -> forall b b0 : Type, b * b0
+
+u1 is not universe polymorphic
+Arguments u1 _ (_ _)%type_scope
+u1 is transparent
+Expands to: Constant RecordProjParameter.u1
+u3 : forall b1 : Btype, u2 b1
+
+u3 is not universe polymorphic
+u3 is transparent
+Expands to: Constant RecordProjParameter.u3
+v1 : Ctype -> forall c0 : Type, c0
+
+v1 is not universe polymorphic
+Arguments v1 _ _%type_scope
+v1 is transparent
+Expands to: Constant RecordProjParameter.v1
+v3 : forall c : Ctype, v2 c
+
+v3 is not universe polymorphic
+v3 is transparent
+Expands to: Constant RecordProjParameter.v3
diff --git a/test-suite/output/RecordProjParameter.v b/test-suite/output/RecordProjParameter.v
new file mode 100644
index 0000000000..8b892c694c
--- /dev/null
+++ b/test-suite/output/RecordProjParameter.v
@@ -0,0 +1,21 @@
+Record Atype : Type :=
+ { t1 : forall (a : Type), a
+ ; t2 : Type
+ ; t3 : t2 }.
+About t1.
+About t3.
+
+Record Btype : Type :=
+ { u1 : forall (b : Type) (b0 : Type), b * b0
+ ; u2 : Type
+ ; u3 : u2 }.
+About u1.
+About u3.
+
+Record Ctype : Type :=
+ { v1 : forall (c0 : Type), c0
+ ; v2 : Type
+ ; v3 : v2
+ }.
+About v1.
+About v3.
diff --git a/test-suite/output/bug_13240.out b/test-suite/output/bug_13240.out
new file mode 100644
index 0000000000..5fccef5cfe
--- /dev/null
+++ b/test-suite/output/bug_13240.out
@@ -0,0 +1,3 @@
+Ltac t1 a b := a ; last b
+Ltac t2 := do !idtac
+Ltac t3 := idtac => True
diff --git a/test-suite/output/bug_13240.v b/test-suite/output/bug_13240.v
new file mode 100644
index 0000000000..a999450cd2
--- /dev/null
+++ b/test-suite/output/bug_13240.v
@@ -0,0 +1,10 @@
+Require Import ssreflect.
+
+Ltac t1 a b := a; last b.
+Print t1.
+
+Ltac t2 := do !idtac.
+Print t2.
+
+Ltac t3 := idtac => True.
+Print t3.
diff --git a/test-suite/output/ltac2_deprecated.out b/test-suite/output/ltac2_deprecated.out
new file mode 100644
index 0000000000..d17b719bcd
--- /dev/null
+++ b/test-suite/output/ltac2_deprecated.out
@@ -0,0 +1,12 @@
+File "stdin", line 13, characters 11-14:
+Warning: Ltac2 definition foo is deprecated. test_definition
+[deprecated-ltac2-definition,deprecated]
+- : unit = ()
+File "stdin", line 14, characters 11-14:
+Warning: Ltac2 alias bar is deprecated. test_notation
+[deprecated-ltac2-alias,deprecated]
+- : unit = ()
+File "stdin", line 15, characters 11-14:
+Warning: Ltac2 definition qux is deprecated. test_external
+[deprecated-ltac2-definition,deprecated]
+- : 'a array -> int = <fun>
diff --git a/test-suite/output/ltac2_deprecated.v b/test-suite/output/ltac2_deprecated.v
new file mode 100644
index 0000000000..9598a5979c
--- /dev/null
+++ b/test-suite/output/ltac2_deprecated.v
@@ -0,0 +1,15 @@
+Require Import Ltac2.Ltac2.
+
+#[deprecated(note="test_definition")]
+Ltac2 foo := ().
+
+#[deprecated(note="test_notation")]
+Ltac2 Notation bar := ().
+
+#[deprecated(note="test_external")]
+Ltac2 @ external qux : 'a array -> int := "ltac2" "array_length".
+(* Randomly picked external function *)
+
+Ltac2 Eval foo.
+Ltac2 Eval bar.
+Ltac2 Eval qux.
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..6bf03d30d3 100644
--- a/test-suite/output/relaxed_ambiguous_paths.out
+++ b/test-suite/output/relaxed_ambiguous_paths.out
@@ -1,58 +1,82 @@
-File "stdin", line 10, characters 0-28:
+File "stdin", line 13, characters 0-29:
Warning:
-New coercion path [ac; cd] : A >-> D is ambiguous with existing
-[ab; bd] : A >-> D. [ambiguous-paths,typechecker]
+New coercion path [g1; f2] : A >-> B' is ambiguous with existing
+[f1; g2] : A >-> B'. [ambiguous-paths,typechecker]
+File "stdin", line 14, characters 0-29:
+Warning:
+New coercion path [h1; f3] : B >-> C' is ambiguous with existing
+[f2; h2] : B >-> C'. [ambiguous-paths,typechecker]
+[f1] : A >-> A'
+[g1] : A >-> B
+[f1; g2] : A >-> B'
+[g1; h1] : A >-> C
+[f1; g2; h2] : A >-> C'
+[g2] : A' >-> B'
+[g2; h2] : A' >-> C'
+[f2] : B >-> B'
+[h1] : B >-> C
+[f2; h2] : B >-> C'
+[h2] : B' >-> C'
+[f3] : C >-> C'
+File "stdin", line 33, characters 0-28:
+Warning:
+New coercion path [ab; bc] : A >-> C is ambiguous with existing
+[ac] : A >-> C. [ambiguous-paths,typechecker]
[ab] : A >-> B
-[ab; bd] : A >-> D
[ac] : A >-> C
-[bd] : B >-> D
+[ac; cd] : A >-> D
+[bc] : B >-> C
+[bc; cd] : B >-> D
[cd] : C >-> D
-File "stdin", line 26, characters 0-28:
+File "stdin", line 50, characters 0-28:
Warning:
New coercion path [ab; bc] : A >-> C is ambiguous with existing
[ac] : A >-> C. [ambiguous-paths,typechecker]
-[ac] : A >-> C
-[ac; cd] : A >-> D
+File "stdin", line 51, characters 0-28:
+Warning:
+New coercion path [ba; ab] : B >-> B is not definitionally an identity function.
+New coercion path [ab; ba] : A >-> A is not definitionally an identity function.
+[ambiguous-paths,typechecker]
[ab] : A >-> B
-[cd] : C >-> D
+[ac] : A >-> C
+[ba] : B >-> A
[bc] : B >-> C
-[bc; cd] : B >-> 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:
+File "stdin", line 147, characters 0-86:
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:
+File "stdin", line 156, characters 0-47:
Warning:
New coercion path [unwrap_nat; wrap_nat] : NAT >-> NAT is not definitionally an identity function.
[ambiguous-paths,typechecker]
-File "stdin", line 131, characters 0-64:
+File "stdin", line 157, characters 0-64:
Warning:
New coercion path [unwrap_list; wrap_list] : LIST >-> LIST is not definitionally an identity function.
[ambiguous-paths,typechecker]
-File "stdin", line 132, characters 0-51:
+File "stdin", line 158, characters 0-51:
Warning:
New coercion path [unwrap_Type; wrap_Type] : TYPE >-> TYPE is not definitionally an identity function.
[ambiguous-paths,typechecker]
diff --git a/test-suite/output/relaxed_ambiguous_paths.v b/test-suite/output/relaxed_ambiguous_paths.v
index 41322045f2..182e155273 100644
--- a/test-suite/output/relaxed_ambiguous_paths.v
+++ b/test-suite/output/relaxed_ambiguous_paths.v
@@ -1,13 +1,20 @@
Module test1.
Section test1.
-Variable (A B C D : Type).
-Variable (ab : A -> B) (bd : B -> D) (ac : A -> C) (cd : C -> D).
-
-Local Coercion ab : A >-> B.
-Local Coercion bd : B >-> D.
-Local Coercion ac : A >-> C.
-Local Coercion cd : C >-> D.
+Variable (A B C A' B' C' : Type).
+Variable (f1 : A -> A') (f2 : B -> B') (f3 : C -> C').
+Variable (g1 : A -> B) (g2 : A' -> B') (h1 : B -> C) (h2 : B' -> C').
+
+Local Coercion g1 : A >-> B.
+Local Coercion g2 : A' >-> B'.
+Local Coercion h1 : B >-> C.
+Local Coercion h2 : B' >-> C'.
+Local Coercion f1 : A >-> A'.
+Local Coercion f2 : B >-> B'.
+Local Coercion f3 : C >-> C'.
+(* [g1; h1; f3], [f1; g2; h2] : A >-> C' should not be reported as ambiguous *)
+(* paths because they are redundant with `[g1; f2], [f1; g2] : A >-> B'` and *)
+(* `[h1; f3], [f2; h2] : B >-> C'`. *)
Print Graph.
@@ -24,8 +31,8 @@ Local Coercion ac : A >-> C.
Local Coercion cd : C >-> D.
Local Coercion ab : A >-> B.
Local Coercion bc : B >-> C.
-(* `[ab; bc; cd], [ac; cd] : A >-> D` should not be shown as ambiguous paths *)
-(* here because they are redundant with `[ab; bc], [ac] : A >-> C`. *)
+(* `[ab; bc; cd], [ac; cd] : A >-> D` should not be reported as ambiguous *)
+(* paths because they are redundant with `[ab; bc], [ac] : A >-> C`. *)
Print Graph.
@@ -34,6 +41,25 @@ End test2.
Module test3.
Section test3.
+
+Variable (A B C : Type).
+Variable (ab : A -> B) (ba : B -> A) (ac : A -> C) (bc : B -> C).
+
+Local Coercion ac : A >-> C.
+Local Coercion bc : B >-> C.
+Local Coercion ab : A >-> B.
+Local Coercion ba : B >-> A.
+(* `[ba; ac], [bc] : B >-> C` should not be reported as ambiguous paths *)
+(* because they are redundant with `[ab; bc], [ac] : A >-> C` and *)
+(* `[ba; ab] : B >-> B`. *)
+
+Print Graph.
+
+End test3.
+End test3.
+
+Module test4.
+Section test4.
Variable (A : Type) (P Q : A -> Prop).
Record B := {
@@ -57,11 +83,11 @@ Local Coercion D_C (d : D) : C := Build_C (D_A d) (D_Q d).
Print Graph.
-End test3.
-End test3.
+End test4.
+End test4.
-Module test4.
-Section test4.
+Module test5.
+Section test5.
Variable (A : Type) (P Q : A -> Prop).
@@ -89,11 +115,11 @@ Local Coercion D_C (d : D) : C true := Build_C true (D_A d) (D_Q d).
Print Graph.
-End test4.
-End test4.
+End test5.
+End test5.
-Module test5.
-Section test5.
+Module test6.
+Section test6.
Variable (A : Type) (P Q : A -> Prop).
@@ -123,18 +149,18 @@ Local Coercion D_C (d : D) : C true :=
Print Graph.
-End test5.
-End test5.
+End test6.
+End test6.
-Module test6.
+Module test7.
Record > NAT := wrap_nat { unwrap_nat :> nat }.
Record > LIST (T : Type) := wrap_list { unwrap_list :> list T }.
Record > TYPE := wrap_Type { unwrap_Type :> Type }.
-End test6.
+End test7.
-Module test7.
+Module test8.
Set Primitive Projections.
Record > NAT_prim := wrap_nat { unwrap_nat :> nat }.
Record > LIST_prim (T : Type) := wrap_list { unwrap_list :> list T }.
Record > TYPE_prim := wrap_Type { unwrap_Type :> Type }.
-End test7.
+End test8.
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 23:03:54 +0000