aboutsummaryrefslogtreecommitdiff
path: root/test-suite/output
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/output')
-rw-r--r--test-suite/output/Notations3.out17
-rw-r--r--test-suite/output/Record.out40
-rw-r--r--test-suite/output/Record.v31
-rw-r--r--test-suite/output/bug_12908.out5
-rw-r--r--test-suite/output/bug_12908.v7
-rw-r--r--test-suite/output/bug_13112.out4
-rw-r--r--test-suite/output/bug_13112.v5
-rw-r--r--test-suite/output/bug_9180.out3
-rw-r--r--test-suite/output/bug_9682.out9
-rw-r--r--test-suite/output/bug_9682.v28
-rw-r--r--test-suite/output/locate.out5
11 files changed, 139 insertions, 15 deletions
diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out
index abada44da7..bd22d45059 100644
--- a/test-suite/output/Notations3.out
+++ b/test-suite/output/Notations3.out
@@ -231,16 +231,13 @@ fun l : list nat => match l with
: list nat -> list nat
Arguments foo _%list_scope
-Notation
-"'exists' x .. y , p" := ex (fun x => .. (ex (fun y => p)) ..) : type_scope
-(default interpretation)
-"'exists' ! x .. y , p" := ex
- (unique
- (fun x => .. (ex (unique (fun y => p))) ..))
-: type_scope (default interpretation)
-Notation
-"( x , y , .. , z )" := pair .. (pair x y) .. z : core_scope
-(default interpretation)
+Notation "'exists' x .. y , p" := (ex (fun x => .. (ex (fun y => p)) ..))
+ : type_scope (default interpretation)
+Notation "'exists' ! x .. y , p" :=
+ (ex (unique (fun x => .. (ex (unique (fun y => p))) ..))) : type_scope
+ (default interpretation)
+Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z) : core_scope
+ (default interpretation)
1 subgoal
============================
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_12908.out b/test-suite/output/bug_12908.out
index fca6dde704..54c4f98422 100644
--- a/test-suite/output/bug_12908.out
+++ b/test-suite/output/bug_12908.out
@@ -1,2 +1,7 @@
forall m n : nat, m * n = (2 * m * n)%nat
: Prop
+File "stdin", line 11, characters 0-31:
+Warning: Notation "_ * _" was already used in scope nat_scope.
+[notation-overridden,parsing]
+forall m n : nat, m * n = Nat.mul (Nat.mul 2 m) n
+ : Prop
diff --git a/test-suite/output/bug_12908.v b/test-suite/output/bug_12908.v
index 558c9f9f6a..6f7be22fa0 100644
--- a/test-suite/output/bug_12908.v
+++ b/test-suite/output/bug_12908.v
@@ -1,6 +1,13 @@
Definition mult' m n := 2 * m * n.
+
Module A.
(* Test hiding of a scoped notation by a lonely notation *)
Infix "*" := mult'.
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 *)
+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_13112.out b/test-suite/output/bug_13112.out
new file mode 100644
index 0000000000..a8a98d6b68
--- /dev/null
+++ b/test-suite/output/bug_13112.out
@@ -0,0 +1,4 @@
+0 + 0
+ : nat
+HI
+ : nat
diff --git a/test-suite/output/bug_13112.v b/test-suite/output/bug_13112.v
new file mode 100644
index 0000000000..9fee5e09d8
--- /dev/null
+++ b/test-suite/output/bug_13112.v
@@ -0,0 +1,5 @@
+Reserved Notation "'HI'".
+Notation "'HI'" := (O + O) (only parsing).
+Check HI. (* 0 + 0 : nat *)
+Notation "'HI'" := (O + O) (only printing).
+Check HI. (* 0 + 0 : nat *)
diff --git a/test-suite/output/bug_9180.out b/test-suite/output/bug_9180.out
index ed4892b389..f035d0252a 100644
--- a/test-suite/output/bug_9180.out
+++ b/test-suite/output/bug_9180.out
@@ -1,4 +1,3 @@
-Notation
-"n .+1" := S n : nat_scope (default interpretation)
+Notation "n .+1" := (S n) : nat_scope (default interpretation)
forall x : nat, x.+1 = x.+1
: Prop
diff --git a/test-suite/output/bug_9682.out b/test-suite/output/bug_9682.out
new file mode 100644
index 0000000000..45d9e4cad1
--- /dev/null
+++ b/test-suite/output/bug_9682.out
@@ -0,0 +1,9 @@
+mmatch 1 + 2 + 3 + 4 + 5 + 6 in nat as x
+return M (x = x) with
+| 1
+end
+ : unit
+#
+ : True
+##
+ : True
diff --git a/test-suite/output/bug_9682.v b/test-suite/output/bug_9682.v
new file mode 100644
index 0000000000..fa30d323ef
--- /dev/null
+++ b/test-suite/output/bug_9682.v
@@ -0,0 +1,28 @@
+Declare Scope blafu.
+Delimit Scope blafu with B.
+Axiom DoesNotMatch : Type.
+Axiom consumer : forall {A} (B : A -> Type) (E:Type) (x : A) (ls : list nat), unit.
+
+Notation "| p1 | .. | pn" := (@cons _ p1 .. (@cons _ pn nil) ..) (at level 91) : blafu.
+Notation "'mmatch_do_not_write' x 'in' T 'as' y 'return' 'M' p 'with_do_not_write' ls" :=
+ (@consumer _ (fun y : T => p%type) DoesNotMatch x ls%B)
+ (at level 200, ls at level 91, only parsing).
+Notation "'mmatch' x 'in' T 'as' y 'return' 'M' p 'with' ls 'end'" :=
+ (mmatch_do_not_write x in T as y return M p with_do_not_write ls)
+ (at level 200, ls at level 91, p at level 10, only parsing).
+(* This should not gives a warning *)
+Notation "'mmatch' x 'in' T 'as' y 'return' 'M' p 'with' ls 'end'" :=
+ (@consumer _ (fun y : T => p%type) DoesNotMatch x ls%B)
+ (at level 200, ls at level 91, p at level 10, only printing,
+ format "'[ ' mmatch '/' x ']' '/' '[ ' in '/' T ']' '/' '[ ' as '/' y ']' '/' '[ ' return M p ']' with '//' '[' ls ']' '//' end"
+ ).
+(* Check use of "mmatch" *)
+Check (mmatch 1 + 2 + 3 + 4 + 5 + 6 in nat as x return M (x = x) with | 1 end).
+
+(* 2nd example *)
+Notation "#" := I (at level 0, only parsing).
+Notation "#" := I (at level 0, only printing).
+Check #.
+Notation "##" := I (at level 0, only printing).
+Notation "##" := I (at level 0, only parsing).
+Check ##.
diff --git a/test-suite/output/locate.out b/test-suite/output/locate.out
index 473db2d312..93d9d6cf7b 100644
--- a/test-suite/output/locate.out
+++ b/test-suite/output/locate.out
@@ -1,3 +1,2 @@
-Notation
-"b1 && b2" := if b1 then b2 else false (default interpretation)
-"x && y" := andb x y : bool_scope
+Notation "b1 && b2" := (if b1 then b2 else false) (default interpretation)
+Notation "x && y" := (andb x y) : bool_scope
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 11:28:35 +0000