Extending support for mixing binders and terms in abbreviations.

3 files changed, 19 insertions, 1 deletions

diff --git a/test-suite/bugs/closed/bug_7903.v b/test-suite/bugs/closed/bug_7903.v
index 55c7ee99a7..18e1884ca7 100644
--- a/test-suite/bugs/closed/bug_7903.v
+++ b/test-suite/bugs/closed/bug_7903.v
@@ -1,4 +1,4 @@
 (* Slightly improving interpretation of Ltac subterms in notations *)
 
 Notation bar x f := (let z := ltac:(exact 1) in (fun x : nat => f)).
-Check bar x (x + x).
+Check fun x => bar x (x + x).
diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out
index f48eaac4c9..9cb019ca56 100644
--- a/test-suite/output/Notations4.out
+++ b/test-suite/output/Notations4.out
@@ -111,3 +111,11 @@ Warning: The format modifier is irrelevant for only parsing rules.
 File "stdin", line 280, characters 0-63:
 Warning: The only parsing modifier has no effect in Reserved Notation.
 [irrelevant-reserved-notation-only-parsing,parsing]
+fun x : nat => U (S x)
+     : nat -> nat
+V tt
+     : unit * (unit -> unit)
+fun x : nat => V x
+     : forall x : nat, nat * (?T -> ?T)
+where
+?T : [x : nat  x0 : ?T |- Type] (x0 cannot be used)
diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v
index 4d4b37a8b2..b3270d4f92 100644
--- a/test-suite/output/Notations4.v
+++ b/test-suite/output/Notations4.v
@@ -280,3 +280,13 @@ Notation "###" := 0 (at level 0, only parsing, format "###").
 Reserved Notation "##" (at level 0, only parsing, format "##").
 
 End N.
+
+Module O.
+
+Notation U t := (match t with 0 => 0 | S t => t | _ => 0 end).
+Check fun x => U (S x).
+Notation V t := (t,fun t => t).
+Check V tt.
+Check fun x : nat => V x.
+
+End O.