Notations: fixing multiple binders used as terms in reverse order.

2 files changed, 32 insertions, 1 deletions

diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out
index c10c78652e..950382d572 100644
--- a/test-suite/output/Notations3.out
+++ b/test-suite/output/Notations3.out
@@ -32,6 +32,23 @@ fun f : forall x : nat * (bool * unit), ?T => CURRY (x : nat) (y : bool), f
        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|}
diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v
index 9577d10747..9efac6508c 100644
--- a/test-suite/output/Notations3.v
+++ b/test-suite/output/Notations3.v
@@ -34,9 +34,22 @@ 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).
+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 *)
@@ -101,3 +114,4 @@ 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).
+