Merge branch 'v8.6'

5 files changed, 281 insertions, 22 deletions

diff --git a/test-suite/output/Notations2.out b/test-suite/output/Notations2.out
index d9ce42c60..20101f48e 100644
--- a/test-suite/output/Notations2.out
+++ b/test-suite/output/Notations2.out
@@ -12,7 +12,7 @@ let '(a, _, _) := (2, 3, 4) in a
      : nat
 exists myx y : bool, myx = y
      : Prop
-fun (P : nat -> nat -> Prop) (x : nat) => exists x0, P x x0
+fun (P : nat -> nat -> Prop) (x : nat) => exists y, P x y
      : (nat -> nat -> Prop) -> nat -> Prop
 ∃ n p : nat, n + p = 0
      : Prop
diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out
new file mode 100644
index 000000000..360f37967
--- /dev/null
+++ b/test-suite/output/Notations3.out
@@ -0,0 +1,100 @@
+[<0, 2 >]
+     : nat * nat * (nat * nat)
+[<0, 2 >]
+     : nat * nat * (nat * nat)
+(0, 2, (2, 2))
+     : nat * nat * (nat * nat)
+pair (pair O (S (S O))) (pair (S (S O)) O)
+     : prod (prod nat nat) (prod nat nat)
+<< 0, 2, 4 >>
+     : nat * nat * nat * (nat * (nat * nat))
+<< 0, 2, 4 >>
+     : nat * nat * nat * (nat * (nat * nat))
+(0, 2, 4, (2, (2, 0)))
+     : 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))
+     : prod (prod (prod nat nat) nat) (prod nat (prod nat nat))
+ETA x y : nat, Nat.add
+     : nat -> nat -> nat
+ETA x y : nat, Nat.add
+     : nat -> nat -> nat
+ETA x y : nat, Nat.add
+     : nat -> nat -> nat
+fun x y : nat => Nat.add x y
+     : forall (_ : nat) (_ : nat), nat
+ETA x y : nat, le_S
+     : forall x y : nat, x <= y -> x <= S y
+fun f : forall x : nat * (bool * unit), ?T => CURRY (x : nat) (y : bool), f
+     : (forall x : nat * (bool * unit), ?T) ->
+       forall (x : nat) (y : bool), ?T@{x:=(x, (y, tt))}
+where
+?T : [x : nat * (bool * unit) |- Type] 
+fun f : forall x : bool * (nat * unit), ?T =>
+CURRYINV (x : nat) (y : bool), f
+     : (forall x : bool * (nat * unit), ?T) ->
+       forall (x : nat) (y : bool), ?T@{x:=(y, (x, tt))}
+where
+?T : [x : bool * (nat * unit) |- Type] 
+fun f : forall x : unit * nat * bool, ?T => CURRYLEFT (x : nat) (y : bool), f
+     : (forall x : unit * nat * bool, ?T) ->
+       forall (x : nat) (y : bool), ?T@{x:=(tt, x, y)}
+where
+?T : [x : unit * nat * bool |- Type] 
+fun f : forall x : unit * bool * nat, ?T =>
+CURRYINVLEFT (x : nat) (y : bool), f
+     : (forall x : unit * bool * nat, ?T) ->
+       forall (x : nat) (y : bool), ?T@{x:=(tt, y, x)}
+where
+?T : [x : unit * bool * nat |- Type] 
+forall n : nat, {#n | 1 > n}
+     : Prop
+forall x : nat, {|x | x > 0|}
+     : Prop
+exists2 x : nat, x = 1 & x = 2
+     : Prop
+fun n : nat =>
+foo2 n (fun x y z : nat => (fun _ _ _ : nat => x + y + z = 0) z y x)
+     : nat -> Prop
+fun n : nat =>
+foo2 n (fun a b c : nat => (fun _ _ _ : nat => a + b + c = 0) c b a)
+     : nat -> Prop
+fun n : nat =>
+foo2 n (fun n0 y z : nat => (fun _ _ _ : nat => n0 + y + z = 0) z y n0)
+     : nat -> Prop
+fun n : nat =>
+foo2 n (fun x n0 z : nat => (fun _ _ _ : nat => x + n0 + z = 0) z n0 x)
+     : nat -> Prop
+fun n : nat =>
+foo2 n (fun x y n0 : nat => (fun _ _ _ : nat => x + y + n0 = 0) n0 y x)
+     : nat -> Prop
+fun n : nat => {|n, y | fun _ _ _ : nat => n + y = 0 |}_2
+     : nat -> Prop
+fun n : nat => {|n, y | fun _ _ _ : nat => n + y = 0 |}_2
+     : nat -> Prop
+fun n : nat => {|n, n0 | fun _ _ _ : nat => n + n0 = 0 |}_2
+     : nat -> Prop
+fun n : nat =>
+foo2 n (fun x y z : nat => (fun _ _ _ : nat => x + y + n = 0) z y x)
+     : nat -> Prop
+fun n : nat =>
+foo2 n (fun x y z : nat => (fun _ _ _ : nat => x + y + n = 0) z y x)
+     : nat -> Prop
+fun n : nat => {|n, fun _ : nat => 0 = 0 |}_3
+     : nat -> Prop
+fun n : nat => {|n, fun _ : nat => n = 0 |}_3
+     : nat -> Prop
+fun n : nat => foo3 n (fun x _ : nat => ETA z : nat, (fun _ : nat => x = 0))
+     : nat -> Prop
+fun n : nat => {|n, fun _ : nat => 0 = 0 |}_4
+     : nat -> Prop
+fun n : nat => {|n, fun _ : nat => n = 0 |}_4
+     : nat -> Prop
+fun n : nat => foo4 n (fun _ _ : nat => ETA z : nat, (fun _ : nat => z = 0))
+     : nat -> Prop
+fun n : nat => foo4 n (fun _ y : nat => ETA z : nat, (fun _ : nat => y = 0))
+     : nat -> Prop
+tele (t : Type) '(y, z) (x : t0) := tt
+     : forall t : Type, nat * nat -> t -> fpack
diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v
new file mode 100644
index 000000000..4b8bfe312
--- /dev/null
+++ b/test-suite/output/Notations3.v
@@ -0,0 +1,141 @@
+(**********************************************************************)
+(* Check printing of notations with several instances of a recursive pattern *)
+(* Was wrong but I could not trigger a problem due to the collision between *)
+(* different instances of ".." *)
+
+Notation "[< x , y , .. , z >]" := (pair (.. (pair x y) ..) z,pair y ( .. (pair z x) ..)).
+Check [<0,2>].
+Check ((0,2),(2,0)).
+Check ((0,2),(2,2)).
+Unset Printing Notations.
+Check [<0,2>].
+Set Printing Notations.
+
+Notation "<< x , y , .. , z >>" := ((.. (x,y) .., z),(z, .. (y,x) ..)).
+Check <<0,2,4>>.
+Check (((0,2),4),(4,(2,0))).
+Check (((0,2),4),(2,(2,0))).
+Check (((0,2),4),(0,(2,4))).
+Unset Printing Notations.
+Check <<0,2,4>>.
+Set Printing Notations.
+
+(**********************************************************************)
+(* Check notations with recursive notations both in binders and terms *)
+
+Notation "'ETA' x .. y , f" :=
+  (fun x => .. (fun y => (.. (f x) ..) y ) ..)
+  (at level 200, x binder, y binder).
+Check ETA (x:nat) (y:nat), Nat.add.
+Check ETA (x y:nat), Nat.add.
+Check ETA x y, Nat.add.
+Unset Printing Notations.
+Check ETA (x:nat) (y:nat), Nat.add.
+Set Printing Notations.
+Check ETA x y, le_S.
+
+Notation "'CURRY' x .. y , f" := (fun x => .. (fun y => f (x, .. (y,tt) ..)) ..)
+  (at level 200, x binder, y binder).
+Check fun f => CURRY (x:nat) (y:bool), f.
+
+Notation "'CURRYINV' x .. y , f" := (fun x => .. (fun y => f (y, .. (x,tt) ..)) ..)
+  (at level 200, x binder, y binder).
+Check fun f => CURRYINV (x:nat) (y:bool), f.
+
+Notation "'CURRYLEFT' x .. y , f" := (fun x => .. (fun y => f (.. (tt,x) .., y)) ..)
+  (at level 200, x binder, y binder).
+Check fun f => CURRYLEFT (x:nat) (y:bool), f.
+
+Notation "'CURRYINVLEFT' x .. y , f" := (fun x => .. (fun y => f (.. (tt,y) .., x)) ..)
+  (at level 200, x binder, y binder).
+Check fun f => CURRYINVLEFT (x:nat) (y:bool), f.
+
+(**********************************************************************)
+(* Notations with variables bound both as a term and as a binder      *)
+(* This is #4592 *)
+
+Notation "{# x | P }" := (ex2 (fun y => x = y) (fun x => P)).
+Check forall n:nat, {# n | 1 > n}.
+
+Parameter foo : forall {T}(x : T)(P : T -> Prop), Prop.
+Notation "{| x | P |}" := (foo x (fun x => P)).
+Check forall x:nat, {| x | x > 0 |}.
+
+Check ex2 (fun x => x=1) (fun x0 => x0=2).
+
+(* Other tests about alpha-conversions: the following notation
+   contains all three kinds of bindings:
+
+   - x is bound in the lhs as a term and a binder: its name is forced
+     by its position as a term; it can bind variables in P
+   - y is bound in the lhs as a binder only: its name is given by its
+     name as a binder in the term to display; it can bind variables in P
+   - z is a binder local to the rhs; it cannot bind a variable in P
+*)
+
+Parameter foo2 : forall {T}(x : T)(P : T -> T -> T -> Prop), Prop.
+Notation "{| x , y | P |}_2" := (foo2 x (fun x y z => P z y x)).
+
+(* Not printable: z (resp c, n) occurs in P *)
+Check fun n => foo2 n (fun x y z => (fun _ _ _ => x+y+z=0) z y x).
+Check fun n => foo2 n (fun a b c => (fun _ _ _ => a+b+c=0) c b a).
+Check fun n => foo2 n (fun n y z => (fun _ _ _ => n+y+z=0) z y n).
+Check fun n => foo2 n (fun x n z => (fun _ _ _ => x+n+z=0) z n x).
+Check fun n => foo2 n (fun x y n => (fun _ _ _ => x+y+n=0) n y x).
+
+(* Printable *)
+Check fun n => foo2 n (fun x y z => (fun _ _ _ => x+y=0) z y x).
+Check fun n => foo2 n (fun n y z => (fun _ _ _ => n+y=0) z y n).
+Check fun n => foo2 n (fun x n z => (fun _ _ _ => x+n=0) z n x).
+
+(* Not printable: renaming x into n would bind the 2nd occurrence of n *)
+Check fun n => foo2 n (fun x y z => (fun _ _ _ => x+y+n=0) z y x).
+Check fun n => foo2 n (fun x y z => (fun _ _ _ => x+y+n=0) z y x).
+
+(* Other tests *)
+Parameter foo3 : forall {T}(x : T)(P : T -> T -> T -> Prop), Prop.
+Notation "{| x , P |}_3" := (foo3 x (fun x x x => P x)).
+
+(* Printable *)
+Check fun n : nat => foo3 n (fun x y z => (fun _ => 0=0) z).
+Check fun n => foo3 n (fun x y z => (fun _ => z=0) z).
+
+(* Not printable: renaming z in n would hide the renaming of x into n *)
+Check fun n => foo3 n (fun x y z => (fun _ => x=0) z).
+
+(* Other tests *)
+Parameter foo4 : forall {T}(x : T)(P : T -> T -> T -> Prop), Prop.
+Notation "{| x , P |}_4" := (foo4 x (fun x _ z => P z)).
+
+(* Printable *)
+Check fun n : nat => foo4 n (fun x y z => (fun _ => 0=0) z).
+Check fun n => foo4 n (fun x y z => (fun _ => x=0) z).
+
+(* Not printable: y, z not allowed to occur in P *)
+Check fun n => foo4 n (fun x y z => (fun _ => z=0) z).
+Check fun n => foo4 n (fun x y z => (fun _ => y=0) z).
+
+(**********************************************************************)
+(* Test printing of #4932                                             *)
+
+Inductive ftele : Type :=
+| fb {T:Type} : T -> ftele
+| fr {T} : (T -> ftele) -> ftele.
+
+Fixpoint args ftele : Type :=
+  match ftele with
+    | fb _ => unit
+    | fr f => sigT (fun t => args (f t))
+  end.
+
+Definition fpack := sigT args.
+Definition pack fp fa : fpack := existT _ fp fa.
+
+Notation "'tele' x .. z := b" :=
+  (fun x => .. (fun z =>
+     pack (fr (fun x => .. ( fr (fun z => fb b) ) .. ) )
+          (existT _ x .. (existT _ z tt) .. )
+                ) ..)
+  (at level 85, x binder, z binder).
+
+Check tele (t:Type) '((y,z):nat*nat) (x:t) := tt.
diff --git a/test-suite/output/PatternsInBinders.out b/test-suite/output/PatternsInBinders.out
index 6a28475d7..c012a86b0 100644
--- a/test-suite/output/PatternsInBinders.out
+++ b/test-suite/output/PatternsInBinders.out
@@ -4,28 +4,36 @@ fun '(x, y) => (y, x)
      : A * B -> B * A
 forall '(x, y), swap (x, y) = (y, x)
      : Prop
-proj_informative = fun 'exist _ x _ => x : A
+proj_informative = fun '(exist _ x _) => x : A
      : {x : A | P x} -> A
-foo = fun 'Bar n b tt p => if b then n + p else n - p
+foo = fun '(Bar n b tt p) => if b then n + p else n - p
      : Foo -> nat
 baz = 
-fun 'Bar n1 _ tt p1 => fun 'Bar _ _ tt _ => n1 + p1
+fun '(Bar n1 _ tt p1) '(Bar _ _ tt _) => n1 + p1
      : Foo -> Foo -> nat
-λ '(x, y), (y, x)
-     : A * B → B * A
-∀ '(x, y), swap (x, y) = (y, x)
-     : Prop
 swap = 
-fun (A B : Type) (pat : A * B) => let '(x, y) := pat in (y, x)
+fun (A B : Type) '(x, y) => (y, x)
      : forall A B : Type, A * B -> B * A
 
 Arguments A, B are implicit and maximally inserted
 Argument scopes are [type_scope type_scope _]
-forall (A B : Type) (pat : A * B), let '(x, y) := pat in swap (x, y) = (y, x)
+fun (A B : Type) '(x, y) => swap (x, y) = (y, x)
+     : forall A B : Type, A * B -> Prop
+forall (A B : Type) '(x, y), swap (x, y) = (y, x)
+     : Prop
+exists '(x, y), swap (x, y) = (y, x)
      : Prop
-exists pat : A * A, let '(x, y) := pat in swap (x, y) = (y, x)
+exists '(x, y) '(z, w), swap (x, y) = (z, w)
+     : Prop
+λ '(x, y), (y, x)
+     : A * B → B * A
+∀ '(x, y), swap (x, y) = (y, x)
      : Prop
 both_z = 
 fun pat : nat * nat =>
 let '(n, p) as pat0 := pat return (F pat0) in (Z n, Z p) : F (n, p)
      : forall pat : nat * nat, F pat
+fun '(x, y) '(z, t) => swap (x, y) = (z, t)
+     : A * B -> B * A -> Prop
+forall '(x, y) '(z, t), swap (x, y) = (z, t)
+     : Prop
diff --git a/test-suite/output/PatternsInBinders.v b/test-suite/output/PatternsInBinders.v
index 8911909ab..b5c91e347 100644
--- a/test-suite/output/PatternsInBinders.v
+++ b/test-suite/output/PatternsInBinders.v
@@ -21,7 +21,20 @@ Print foo.
 Definition baz '(Bar n1 b1 tt p1) '(Bar n2 b2 tt p2) := n1+p1.
 Print baz.
 
-(** Some test involving unicode noations. *)
+Module WithParameters.
+
+Definition swap {A B} '((x,y) : A*B) := (y,x).
+Print swap.
+
+Check fun (A B:Type) '((x,y) : A*B) => swap (x,y) = (y,x).
+Check forall (A B:Type) '((x,y) : A*B), swap (x,y) = (y,x).
+
+Check exists '((x,y):A*A), swap (x,y) = (y,x).
+Check exists '((x,y):A*A) '(z,w), swap (x,y) = (z,w).
+
+End WithParameters.
+
+(** Some test involving unicode notations. *)
 Module WithUnicode.
 
   Require Import Coq.Unicode.Utf8.
@@ -31,24 +44,21 @@ Module WithUnicode.
 
 End WithUnicode.
 
-
 (** * Suboptimal printing *)
 
-(** These tests show examples which expose the [let] introduced by
-    the pattern notation in binders. *)
-
 Module Suboptimal.
 
-Definition swap {A B} '((x,y) : A*B) := (y,x).
-Print swap.
-
-Check forall (A B:Type) '((x,y) : A*B), swap (x,y) = (y,x).
-
-Check exists '((x,y):A*A), swap (x,y) = (y,x).
+(** This test shows an example which exposes the [let] introduced by
+    the pattern notation in binders. *)
 
 Inductive Fin (n:nat) := Z : Fin n.
 Definition F '(n,p) : Type := (Fin n * Fin p)%type.
 Definition both_z '(n,p) : F (n,p) := (Z _,Z _).
 Print both_z.
 
+(** These tests show examples which do not factorize binders *)
+
+Check fun '((x,y) : A*B) '(z,t) => swap (x,y) = (z,t).
+Check forall '(x,y) '((z,t) : B*A), swap (x,y) = (z,t).
+
 End Suboptimal.