Fixing #4932 (anomaly when using binders as terms in recursive notations).

This application was actually not anticipated. It is nice and was not
too difficult to support.

Design for pattern binders maybe to clarify. When seing pat(x1,..,xn)
as a term, I just reused pat(x1,..,xn), but maybe it is worth using
the variable aliasing the pattern, for more a concise notation. But at
the same time, this means exposing the internal name of the alias
which is not so elegant.

1 files changed, 40 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/4932.v b/test-suite/bugs/closed/4932.v
new file mode 100644
index 0000000000..df200cdce0
--- /dev/null
+++ b/test-suite/bugs/closed/4932.v
@@ -0,0 +1,40 @@
+(* Testing recursive notations with binders seen as terms *)
+
+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 fun '((y,z):nat*nat) => pack (fr (fun '((y,z):nat*nat) => fb tt))
+                                   (existT _ (y,z) tt).
+
+Example test := tele (t : Type) := tt.
+Check test nat.
+
+Example test2 := tele (t : Type) (x:t) := tt.
+Check test2 nat 0.
+
+Check tele (t : Type) (y:=0) (x:t) := tt.
+Check (tele (t : Type) (y:=0) (x:t) := tt) nat 0.
+
+Check tele (t : Type) '((y,z):nat*nat) (x:t) := tt.
+Check (tele (t : Type) '((y,z):nat*nat) (x:t) := tt) nat (1,2) 3.