aboutsummaryrefslogtreecommitdiff
path: root/test-suite/output
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/output')
-rw-r--r--test-suite/output/Implicit.out7
-rw-r--r--test-suite/output/Implicit.v10
-rw-r--r--test-suite/output/ImplicitTypes.out26
-rw-r--r--test-suite/output/ImplicitTypes.v37
-rw-r--r--test-suite/output/Notations.out13
-rw-r--r--test-suite/output/Notations4.out36
-rw-r--r--test-suite/output/Notations4.v89
-rw-r--r--test-suite/output/Notations5.out136
-rw-r--r--test-suite/output/Notations5.v126
-rw-r--r--test-suite/output/NumeralNotations.out2
-rw-r--r--test-suite/output/NumeralNotations.v1
-rw-r--r--test-suite/output/Record.v2
-rw-r--r--test-suite/output/UnivBinders.out18
13 files changed, 416 insertions, 87 deletions
diff --git a/test-suite/output/Implicit.out b/test-suite/output/Implicit.out
index 5f22eb5d7c..ef7667936c 100644
--- a/test-suite/output/Implicit.out
+++ b/test-suite/output/Implicit.out
@@ -1,4 +1,4 @@
-compose (C:=nat) S
+compose S
: (nat -> nat) -> nat -> nat
ex_intro (P:=fun _ : nat => True) (x:=0) I
: ex (fun _ : nat => True)
@@ -12,3 +12,8 @@ map id' (1 :: nil)
: list nat
map (id'' (A:=nat)) (1 :: nil)
: list nat
+fix f (x : nat) : option nat := match x with
+ | 0 => None
+ | S _ => x
+ end
+ : nat -> option nat
diff --git a/test-suite/output/Implicit.v b/test-suite/output/Implicit.v
index 306532c0df..a7c4399e38 100644
--- a/test-suite/output/Implicit.v
+++ b/test-suite/output/Implicit.v
@@ -51,3 +51,13 @@ Definition id'' (A:Type) (x:A) := x.
Check map (@id'' nat) (1::nil).
+Module MatchBranchesInContext.
+
+Set Implicit Arguments.
+Set Contextual Implicit.
+
+Inductive option A := None | Some (a:A).
+Coercion some_nat := @Some nat.
+Check fix f x := match x with 0 => None | n => some_nat n end.
+
+End MatchBranchesInContext.
diff --git a/test-suite/output/ImplicitTypes.out b/test-suite/output/ImplicitTypes.out
new file mode 100644
index 0000000000..824c260e92
--- /dev/null
+++ b/test-suite/output/ImplicitTypes.out
@@ -0,0 +1,26 @@
+forall b, b = b
+ : Prop
+forall b : nat, b = b
+ : Prop
+forall b : bool, @eq bool b b
+ : Prop
+forall b : bool, b = b
+ : Prop
+forall b c : bool, b = c
+ : Prop
+forall c b : bool, b = c
+ : Prop
+forall b1 b2, b1 = b2
+ : Prop
+fun b => b = b
+ : bool -> Prop
+fix f b (n : nat) {struct n} : bool :=
+ match n with
+ | 0 => b
+ | S p => f b p
+ end
+ : bool -> nat -> bool
+∀ b c : bool, b = c
+ : Prop
+∀ b1 b2, b1 = b2
+ : Prop
diff --git a/test-suite/output/ImplicitTypes.v b/test-suite/output/ImplicitTypes.v
new file mode 100644
index 0000000000..dbc83f9229
--- /dev/null
+++ b/test-suite/output/ImplicitTypes.v
@@ -0,0 +1,37 @@
+Implicit Types b : bool.
+Check forall b, b = b.
+
+(* Check the type is not used if not the reserved one *)
+Check forall b:nat, b = b.
+
+(* Check full printing *)
+Set Printing All.
+Check forall b, b = b.
+Unset Printing All.
+
+(* Check printing of type *)
+Unset Printing Use Implicit Types.
+Check forall b, b = b.
+Set Printing Use Implicit Types.
+
+(* Check factorization: we give priority on factorization over implicit type *)
+Check forall b c, b = c.
+Check forall c b, b = c.
+
+(* Check factorization of implicit types *)
+Check forall b1 b2, b1 = b2.
+
+(* Check in "fun" *)
+Check fun b => b = b.
+
+(* Check in binders *)
+Check fix f b n := match n with 0 => b | S p => f b p end.
+
+(* Check in notations *)
+Module Notation.
+ Notation "∀ x .. y , P" := (forall x, .. (forall y, P) ..)
+ (at level 200, x binder, y binder, right associativity,
+ format "'[ ' '[ ' ∀ x .. y ']' , '/' P ']'") : type_scope.
+ Check forall b c, b = c.
+ Check forall b1 b2, b1 = b2.
+End Notation.
diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out
index b870fa6f6f..53ad8a9612 100644
--- a/test-suite/output/Notations.out
+++ b/test-suite/output/Notations.out
@@ -107,14 +107,15 @@ fun x : option Z => match x with
end
: option Z -> Z
fun x : option Z => match x with
- | SOME2 x0 => x0
- | NONE2 => 0
+ | SOME3 _ x0 => x0
+ | NONE3 _ => 0
end
: option Z -> Z
-fun x : list ?T => match x with
- | NIL => NONE2
- | (_ :') t => SOME2 t
- end
+fun x : list ?T =>
+match x with
+| NIL => NONE3 (list ?T)
+| (_ :') t => SOME3 (list ?T) t
+end
: list ?T -> option (list ?T)
where
?T : [x : list ?T x1 : list ?T x0 := x1 : list ?T |- Type] (x, x1,
diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out
index f65696e464..e121b5e86c 100644
--- a/test-suite/output/Notations4.out
+++ b/test-suite/output/Notations4.out
@@ -71,3 +71,39 @@ The command has indeed failed with message:
The format is not the same on the right- and left-hand sides of the special token "..".
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 constr:expr is
+[ "201" RIGHTA
+ [ "{"; constr:operconstr LEVEL "200"; "}" ] ]
+
+fun x : nat => [ x ]
+ : nat -> nat
+fun x : nat => [x]
+ : nat -> nat
+∀ x : nat, x = x
+ : Prop
+File "stdin", line 219, 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 232, characters 0-60:
+Warning: Notation "_ %%% _" was already defined with a different format.
+[notation-incompatible-format,parsing]
+File "stdin", line 236, characters 0-64:
+Warning: Notation "_ %%% _" was already defined with a different format.
+[notation-incompatible-format,parsing]
+File "stdin", line 241, characters 0-62:
+Warning: Lonely notation "_ %%%% _" was already defined with a different
+format. [notation-incompatible-format,parsing]
+3 %% 4
+ : nat
+3 %% 4
+ : nat
+3 %% 4
+ : nat
+File "stdin", line 269, characters 0-61:
+Warning: The format modifier is irrelevant for only parsing rules.
+[irrelevant-format-only-parsing,parsing]
+File "stdin", line 273, characters 0-63:
+Warning: The only parsing modifier has no effect in Reserved Notation.
+[irrelevant-reserved-notation-only-parsing,parsing]
diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v
index 4de6ce19b4..1cf0d919b1 100644
--- a/test-suite/output/Notations4.v
+++ b/test-suite/output/Notations4.v
@@ -184,3 +184,92 @@ Fail Notation " {@ T1 ; T2 ; .. ; Tn } " :=
(format "'[v' {@ '[' T1 ']' ; '//' '[' T2 ']' ; '//' .. ; '//' '[' Tn ']' } ']'").
End M.
+
+Module Bug11331.
+
+Declare Custom Entry expr.
+Notation "{ p }" := (p) (in custom expr at level 201, p constr).
+Print Custom Grammar expr.
+
+End Bug11331.
+
+Module Bug_6082.
+
+Declare Scope foo.
+Notation "[ x ]" := (S x) (format "[ x ]") : foo.
+Open Scope foo.
+Check fun x => S x.
+
+Declare Scope bar.
+Notation "[ x ]" := (S x) (format "[ x ]") : bar.
+Open Scope bar.
+
+Check fun x => S x.
+
+End Bug_6082.
+
+Module Bug_7766.
+
+Notation "∀ x .. y , P" := (forall x, .. (forall y, P) ..)
+ (at level 200, x binder, y binder, right associativity,
+ format "'[ ' ∀ x .. y ']' , P") : type_scope.
+
+Check forall (x : nat), x = x.
+
+Notation "∀ x .. y , P" := (forall x, .. (forall y, P) ..)
+ (at level 200, x binder, y binder, right associativity,
+ format "∀ x .. y , P") : type_scope.
+
+Check forall (x : nat), x = x.
+
+End Bug_7766.
+
+Module N.
+
+(* Other tests about generic and specific formats *)
+
+Reserved Notation "x %%% y" (format "x %%% y", at level 35).
+Reserved Notation "x %%% y" (format "x %%% y", at level 35).
+
+(* Not using the reserved format, we warn *)
+
+Notation "x %%% y" := (x+y) (format "x %%% y", at level 35).
+
+(* Same scope (here lonely): we warn *)
+
+Notation "x %%%% y" := (x+y) (format "x %%%% y", at level 35).
+Notation "x %%%% y" := (x+y) (format "x %%%% y", at level 35).
+
+(* Test if the format for a specific notation becomes the default
+ generic format or if the generic format, in the absence of a
+ Reserved Notation, is the one canonically obtained from the
+ notation *)
+
+Declare Scope foo_scope.
+Declare Scope bar_scope.
+Declare Scope bar'_scope.
+Notation "x %% y" := (x+y) (at level 47, format "x %% y") : foo_scope.
+Open Scope foo_scope.
+Check 3 %% 4.
+
+(* No scope, we inherit the initial format *)
+
+Notation "x %% y" := (x*y) : bar_scope. (* Inherit the format *)
+Open Scope bar_scope.
+Check 3 %% 4.
+
+(* Different scope and no reserved notation, we don't warn *)
+
+Notation "x %% y" := (x*y) (at level 47, format "x %% y") : bar'_scope.
+Open Scope bar'_scope.
+Check 3 %% 4.
+
+(* Warn for combination of "only parsing" and "format" *)
+
+Notation "###" := 0 (at level 0, only parsing, format "###").
+
+(* In reserved notation, warn only for the "only parsing" *)
+
+Reserved Notation "##" (at level 0, only parsing, format "##").
+
+End N.
diff --git a/test-suite/output/Notations5.out b/test-suite/output/Notations5.out
index 83dd2f40fb..f59306c454 100644
--- a/test-suite/output/Notations5.out
+++ b/test-suite/output/Notations5.out
@@ -6,13 +6,13 @@ where
?B : [ |- Type]
p 0
: forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b
-p 0 0 (B:=bool)
+p 0 0
: forall b : bool, 0 = 0 /\ b = b
-p 0 0 (B:=bool)
+p 0 0
: forall b : bool, 0 = 0 /\ b = b
-p (A:=nat)
+p
: forall (a1 a2 : nat) (B : Type) (b : B), a1 = a2 /\ b = b
-p (A:=nat)
+p
: forall (a1 a2 : nat) (B : Type) (b : B), a1 = a2 /\ b = b
@p nat 0 0
: forall (B : Type) (b : B), 0 = 0 /\ b = b
@@ -44,16 +44,16 @@ p
: forall (A : Type) (a1 a2 : A) (B : Type) (b : B), a1 = a2 /\ b = b
f x true
: 0 = 0 /\ true = true
-f x (B:=bool)
+f x
: forall b : bool, 0 = 0 /\ b = b
-f x (B:=bool)
+f x
: forall b : bool, 0 = 0 /\ b = b
@f nat
: forall a1 a2 : nat,
T a1 a2 -> forall (B : Type) (b : B), a1 = a2 /\ b = b
-f (a1:=0) (a2:=0)
+f
: T 0 0 -> forall (B : Type) (b : B), 0 = 0 /\ b = b
-f (a1:=0) (a2:=0)
+f
: T 0 0 -> forall (B : Type) (b : B), 0 = 0 /\ b = b
@f
: forall (A : Type) (a1 a2 : A),
@@ -62,27 +62,27 @@ f
: T 0 0 -> forall (B : Type) (b : B), 0 = 0 /\ b = b
x.(f) true
: 0 = 0 /\ true = true
-x.(f) (B:=bool)
+x.(f)
: forall b : bool, 0 = 0 /\ b = b
-x.(f) (B:=bool)
+x.(f)
: forall b : bool, 0 = 0 /\ b = b
@f nat
: forall a1 a2 : nat,
T a1 a2 -> forall (B : Type) (b : B), a1 = a2 /\ b = b
-f (a1:=0) (a2:=0)
+f
: T 0 0 -> forall (B : Type) (b : B), 0 = 0 /\ b = b
-f (a1:=0) (a2:=0)
+f
: T 0 0 -> forall (B : Type) (b : B), 0 = 0 /\ b = b
@f
: forall (A : Type) (a1 a2 : A),
T a1 a2 -> forall (B : Type) (b : B), a1 = a2 /\ b = b
f
: T 0 0 -> forall (B : Type) (b : B), 0 = 0 /\ b = b
-p
+u ?A
: forall (a1 a2 : ?A) (B : Type) (b : B), a1 = a2 /\ b = b
where
?A : [ |- Type]
-p
+u ?A
: forall (a1 a2 : ?A) (B : Type) (b : B), a1 = a2 /\ b = b
where
?A : [ |- Type]
@@ -90,23 +90,23 @@ u
: forall (A : Type) (a1 a2 : A) (B : Type) (b : B), a1 = a2 /\ b = b
u
: forall (A : Type) (a1 a2 : A) (B : Type) (b : B), a1 = a2 /\ b = b
-p 0 0
+u nat 0 0 ?B
: forall b : ?B, 0 = 0 /\ b = b
where
?B : [ |- Type]
-p 0 0
+u nat 0 0 bool
: forall b : bool, 0 = 0 /\ b = b
-@p nat 0 0
+u nat 0 0
: forall (B : Type) (b : B), 0 = 0 /\ b = b
-@p nat 0 0
+u nat 0 0
: forall (B : Type) (b : B), 0 = 0 /\ b = b
u
: forall (a1 a2 : ?A) (B : Type) (b : B), a1 = a2 /\ b = b
where
?A : [ |- Type]
-u
+@u
: forall (A : Type) (a1 a2 : A) (B : Type) (b : B), a1 = a2 /\ b = b
-u
+@u
: forall (A : Type) (a1 a2 : A) (B : Type) (b : B), a1 = a2 /\ b = b
u
: forall (a1 a2 : ?A) (B : Type) (b : B), a1 = a2 /\ b = b
@@ -138,7 +138,7 @@ v 0
: forall b : ?B, 0 = 0 /\ b = b
where
?B : [ |- Type]
-v 0 (B:=bool) true
+v 0 true
: 0 = 0 /\ true = true
v
: forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b
@@ -158,7 +158,7 @@ v 0
: forall b : ?B, 0 = 0 /\ b = b
where
?B : [ |- Type]
-v 0 (B:=bool) true
+v 0 true
: 0 = 0 /\ true = true
v
: forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b
@@ -188,15 +188,15 @@ where
: forall b : ?B, 0 = 0 /\ b = b
where
?B : [ |- Type]
-## 0 0 (B:=bool) true
+## 0 0 true
: 0 = 0 /\ true = true
-## 0 0 (B:=bool) true
+## 0 0 true
: 0 = 0 /\ true = true
## 0 0 (B:=bool)
: forall b : bool, 0 = 0 /\ b = b
## 0 0 (B:=bool)
: forall b : bool, 0 = 0 /\ b = b
-p
+## ?A
: forall (a1 a2 : ?A) (B : Type) (b : B), a1 = a2 /\ b = b
where
?A : [ |- Type]
@@ -204,45 +204,109 @@ where
: forall (A : Type) (a1 a2 : A) (B : Type) (b : B), a1 = a2 /\ b = b
##
: forall (A : Type) (a1 a2 : A) (B : Type) (b : B), a1 = a2 /\ b = b
-p 0
+## nat 0
: forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b
-p 0
+## nat 0
: forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b
-@p nat 0 0
+## nat 0 0
: forall (B : Type) (b : B), 0 = 0 /\ b = b
-p 0 0
+## nat 0 0 ?B
: forall b : ?B, 0 = 0 /\ b = b
where
?B : [ |- Type]
-p 0 0
+## nat 0 0 ?B
: forall b : ?B, 0 = 0 /\ b = b
where
?B : [ |- Type]
-p 0 0 (B:=bool)
+## nat 0 0 bool
: forall b : bool, 0 = 0 /\ b = b
-p 0 0 true
+## nat 0 0 bool true
: 0 = 0 /\ true = true
## 0
: forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b
## 0
: forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b
+## 0 0
+ : forall b : ?B, 0 = 0 /\ b = b
+where
+?B : [ |- Type]
## 0 0 (B:=bool)
: forall b : bool, 0 = 0 /\ b = b
## 0 0 (B:=bool)
: forall b : bool, 0 = 0 /\ b = b
-## 0 0 (B:=bool) true
+## 0 0 true
: 0 = 0 /\ true = true
-## 0 0 (B:=bool) true
+## 0 0 true
: 0 = 0 /\ true = true
## 0
: forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b
## 0
: forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b
+## 0 0
+ : forall b : ?B, 0 = 0 /\ b = b
+where
+?B : [ |- Type]
## 0 0 (B:=bool)
: forall b : bool, 0 = 0 /\ b = b
## 0 0 (B:=bool)
: forall b : bool, 0 = 0 /\ b = b
-## 0 0 (B:=bool) true
+## 0 0 true
: 0 = 0 /\ true = true
-## 0 0 (B:=bool) true
+## 0 0 true
: 0 = 0 /\ true = true
+# 0 0 bool 0%bool
+ : T
+fun a : T => match a with
+ | # 0 0 _ _ => 1
+ | _ => 2
+ end
+ : T -> nat
+#' 0 0 0%bool
+ : T
+fun a : T => match a with
+ | #' 0 0 _ => 1
+ | _ => 2
+ end
+ : T -> nat
+## 0 0 0%bool
+ : T
+fun a : T => match a with
+ | ## 0 0 _ => 1
+ | _ => 2
+ end
+ : T -> nat
+##' 0 0 0%bool
+ : T
+fun a : T => match a with
+ | ##' 0 0 _ => 1
+ | _ => 2
+ end
+ : T -> nat
+P 0 0 bool 0%bool
+ : T
+fun a : T => match a with
+ | P 0 0 _ _ => 1
+ | _ => 2
+ end
+ : T -> nat
+P' 0 0 0%bool
+ : T
+fun a : T => match a with
+ | P' 0 0 _ => 1
+ | _ => 2
+ end
+ : T -> nat
+Q 0 0 0%bool
+ : T
+fun a : T => match a with
+ | Q 0 0 _ => 1
+ | _ => 2
+ end
+ : T -> nat
+Q' 0 0 0%bool
+ : T
+fun a : T => match a with
+ | Q' 0 0 _ => 1
+ | _ => 2
+ end
+ : T -> nat
diff --git a/test-suite/output/Notations5.v b/test-suite/output/Notations5.v
index b3bea929ba..09d5e31c48 100644
--- a/test-suite/output/Notations5.v
+++ b/test-suite/output/Notations5.v
@@ -115,21 +115,21 @@ Module AppliedTermsPrinting.
Notation u := @p.
Check u _.
- (* p *)
+ (* u ?A *)
Check p.
- (* p *)
+ (* u ?A *)
Check @p.
(* u *)
Check u.
(* u *)
Check p 0 0.
- (* p 0 0 *)
+ (* u nat 0 0 ?B *)
Check u nat 0 0 bool.
- (* p 0 0 -- WEAKNESS should ideally be (B:=bool) *)
+ (* u nat 0 0 bool *)
Check u nat 0 0.
- (* @p nat 0 0 *)
+ (* u nat 0 0 *)
Check @p nat 0 0.
- (* @p nat 0 0 *)
+ (* u nat 0 0 *)
End AtAbbreviationForApplicationHead.
@@ -145,9 +145,9 @@ Module AppliedTermsPrinting.
Check p.
(* u *)
Check @p.
- (* u -- BUG *)
+ (* @u *)
Check @u.
- (* u -- BUG *)
+ (* @u *)
Check u.
(* u *)
Check p 0 0.
@@ -181,7 +181,7 @@ Module AppliedTermsPrinting.
Check v 0.
(* v 0 *)
Check v 0 true.
- (* v 0 (B:=bool) true -- BUG *)
+ (* v 0 true *)
Check @p nat 0.
(* v *)
Check @p nat 0 0.
@@ -209,7 +209,7 @@ Module AppliedTermsPrinting.
Check v 0.
(* v 0 *)
Check v 0 true.
- (* v 0 (B:=bool) true -- BUG *)
+ (* v 0 true *)
Check @p nat 0.
(* v *)
Check @p nat 0 0.
@@ -243,9 +243,9 @@ Module AppliedTermsPrinting.
Check ## 0 0.
(* ## 0 0 *)
Check p 0 0 true.
- (* ## 0 0 (B:=bool) true -- BUG B should not be displayed *)
+ (* ## 0 0 true *)
Check ## 0 0 true.
- (* ## 0 0 (B:=bool) true -- BUG B should not be displayed *)
+ (* ## 0 0 true *)
Check p 0 0 (B:=bool).
(* ## 0 0 (B:=bool) *)
Check ## 0 0 (B:=bool).
@@ -263,25 +263,25 @@ Module AppliedTermsPrinting.
Notation "##" := @p (at level 0).
Check p.
- (* p *)
+ (* ## ?A *)
Check @p.
(* ## *)
Check ##.
(* ## *)
Check p 0.
- (* p 0 -- why not "## nat 0" *)
+ (* ## nat 0 *)
Check ## nat 0.
- (* p 0 *)
+ (* ## nat 0 *)
Check ## nat 0 0.
- (* @p nat 0 0 *)
+ (* ## nat 0 0 *)
Check p 0 0.
- (* p 0 0 *)
+ (* ## nat 0 0 ?B *)
Check ## nat 0 0 _.
- (* p 0 0 *)
+ (* ## nat 0 0 ?B *)
Check ## nat 0 0 bool.
- (* p 0 0 (B:=bool) *)
+ (* ## nat 0 0 bool *)
Check ## nat 0 0 bool true.
- (* p 0 0 true *)
+ (* ## nat 0 0 bool true *)
End AtNotationForHeadApplication.
@@ -298,16 +298,16 @@ Module AppliedTermsPrinting.
(* ## 0 *)
Check ## 0.
(* ## 0 *)
- (* Check ## 0 0. *)
- (* Anomaly *)
+ Check ## 0 0.
+ (* ## 0 0 *)
Check p 0 0 (B:=bool).
(* ## 0 0 (B:=bool) *)
- Check ## 0 0 bool.
- (* ## 0 0 (B:=bool) -- INCONSISTENT parsing/printing *)
+ Check ## 0 0 (B:=bool).
+ (* ## 0 0 (B:=bool) *)
Check p 0 0 true.
- (* ## 0 0 (B:=bool) true -- BUG B should not be displayed *)
- Check ## 0 0 bool true.
- (* ## 0 0 (B:=bool) true -- INCONSISTENT parsing/printing + BUG B should not be displayed *)
+ (* ## 0 0 true *)
+ Check ## 0 0 true.
+ (* ## 0 0 true *)
End NotationForPartialApplication.
@@ -324,17 +324,75 @@ Module AppliedTermsPrinting.
(* ## 0 *)
Check ## 0.
(* ## 0 *)
- (* Check ## 0 0. *)
- (* Anomaly *)
+ Check ## 0 0.
+ (* ## 0 0 *)
Check p 0 0 (B:=bool).
(* ## 0 0 (B:=bool) *)
- Check ## 0 0 bool.
- (* ## 0 0 (B:=bool) -- INCONSISTENT parsing/printing *)
+ Check ## 0 0 (B:=bool).
+ (* ## 0 0 (B:=bool) *)
Check p 0 0 true.
- (* ## 0 0 (B:=bool) true -- BUG B should not be displayed *)
- Check ## 0 0 bool true.
- (* ## 0 0 (B:=bool) true -- INCONSISTENCY parsing/printing + BUG B should not be displayed *)
+ (* ## 0 0 true *)
+ Check ## 0 0 true.
+ (* ## 0 0 true *)
End AtNotationForPartialApplication.
End AppliedTermsPrinting.
+
+Module AppliedPatternsPrinting.
+
+ (* Other tests testing inheritance of scope and implicit in
+ term and pattern for parsing and printing *)
+
+ Inductive T := p (a:nat) (b:bool) {B} (b:B) : T.
+ Notation "0" := true : bool_scope.
+
+ Module A.
+ Notation "#" := @p (at level 0).
+ Check # 0 0 _ true.
+ Check fun a => match a with # 0 0 _ _ => 1 | _ => 2 end. (* !! *)
+ End A.
+
+ Module B.
+ Notation "#'" := p (at level 0).
+ Check #' 0 0 true.
+ Check fun a => match a with #' 0 0 _ => 1 | _ => 2 end.
+ End B.
+
+ Module C.
+ Notation "## q" := (@p q) (at level 0, q at level 0).
+ Check ## 0 0 true.
+ Check fun a => match a with ## 0 0 _ => 1 | _ => 2 end.
+ End C.
+
+ Module D.
+ Notation "##' q" := (p q) (at level 0, q at level 0).
+ Check ##' 0 0 true.
+ Check fun a => match a with ##' 0 0 _ => 1 | _ => 2 end.
+ End D.
+
+ Module E.
+ Notation P := @ p.
+ Check P 0 0 _ true.
+ Check fun a => match a with P 0 0 _ _ => 1 | _ => 2 end.
+ End E.
+
+ Module F.
+ Notation P' := p.
+ Check P' 0 0 true.
+ Check fun a => match a with P' 0 0 _ => 1 | _ => 2 end.
+ End F.
+
+ Module G.
+ Notation Q q := (@p q).
+ Check Q 0 0 true.
+ Check fun a => match a with Q 0 0 _ => 1 | _ => 2 end.
+ End G.
+
+ Module H.
+ Notation Q' q := (p q).
+ Check Q' 0 0 true.
+ Check fun a => match a with Q' 0 0 _ => 1 | _ => 2 end.
+ End H.
+
+End AppliedPatternsPrinting.
diff --git a/test-suite/output/NumeralNotations.out b/test-suite/output/NumeralNotations.out
index 505dc52ebe..113384e9cf 100644
--- a/test-suite/output/NumeralNotations.out
+++ b/test-suite/output/NumeralNotations.out
@@ -75,7 +75,7 @@ The command has indeed failed with message:
In environment
v := 0 : nat
The term "v" has type "nat" while it is expected to have type "wuint".
-File "stdin", line 202, characters 2-72:
+File "stdin", line 203, characters 2-72:
Warning: The 'abstract after' directive has no effect when the parsing
function (of_uint) targets an option type.
[abstract-large-number-no-op,numbers]
diff --git a/test-suite/output/NumeralNotations.v b/test-suite/output/NumeralNotations.v
index c306b15ef3..22aff36d67 100644
--- a/test-suite/output/NumeralNotations.v
+++ b/test-suite/output/NumeralNotations.v
@@ -123,6 +123,7 @@ Module Test6.
Export Scopes.
Numeral Notation wnat of_uint to_uint : wnat_scope (abstract after 5000).
End Notations.
+ Set Printing Coercions.
Check let v := 0%wnat in v : wnat.
Check wrap O.
Timeout 1 Check wrap (ack 4 4). (* should be instantaneous *)
diff --git a/test-suite/output/Record.v b/test-suite/output/Record.v
index d9a649fadc..71a8afa131 100644
--- a/test-suite/output/Record.v
+++ b/test-suite/output/Record.v
@@ -20,6 +20,8 @@ Check {| field := 5 |}.
Check build_r 5.
Check build_c 5.
+Set Printing Records.
+
Record N := C { T : Type; _ : True }.
Check fun x:N => let 'C _ p := x in p.
Check fun x:N => let 'C T _ := x in T.
diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out
index 525ca48bee..04514c15cb 100644
--- a/test-suite/output/UnivBinders.out
+++ b/test-suite/output/UnivBinders.out
@@ -67,9 +67,9 @@ mono
The command has indeed failed with message:
Universe u already exists.
bobmorane =
-let tt := Type@{UnivBinders.34} in
-let ff := Type@{UnivBinders.36} in tt -> ff
- : Type@{max(UnivBinders.33,UnivBinders.35)}
+let tt := Type@{UnivBinders.33} in
+let ff := Type@{UnivBinders.35} in tt -> ff
+ : Type@{max(UnivBinders.32,UnivBinders.34)}
The command has indeed failed with message:
Universe u already bound.
foo@{E M N} =
@@ -142,16 +142,16 @@ Applied.infunct@{u v} =
inmod@{u} -> Type@{v}
: Type@{max(u+1,v+1)}
(* u v |= *)
-axfoo@{i UnivBinders.59 UnivBinders.60} :
-Type@{UnivBinders.59} -> Type@{i}
-(* i UnivBinders.59 UnivBinders.60 |= *)
+axfoo@{i UnivBinders.58 UnivBinders.59} :
+Type@{UnivBinders.58} -> Type@{i}
+(* i UnivBinders.58 UnivBinders.59 |= *)
axfoo is universe polymorphic
Arguments axfoo _%type_scope
Expands to: Constant UnivBinders.axfoo
-axbar@{i UnivBinders.59 UnivBinders.60} :
-Type@{UnivBinders.60} -> Type@{i}
-(* i UnivBinders.59 UnivBinders.60 |= *)
+axbar@{i UnivBinders.58 UnivBinders.59} :
+Type@{UnivBinders.59} -> Type@{i}
+(* i UnivBinders.58 UnivBinders.59 |= *)
axbar is universe polymorphic
Arguments axbar _%type_scope
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 00:18:59 +0000