Fixing amazing loop when using eta-expansion in pattern-matching for

printing notations. Since notation printing is not typed, printing "F G"
using a notation for "f (fun x => g)" recursively eta-expands G, then
x, then a new x and so on forever.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14796 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 10 insertions, 0 deletions

diff --git a/test-suite/complexity/Notations.v b/test-suite/complexity/Notations.v
new file mode 100644
index 000000000..d36d77d57
--- /dev/null
+++ b/test-suite/complexity/Notations.v
@@ -0,0 +1,10 @@
+(* Last line should not loop, even in the presence of eta-expansion in the *)
+(* printing mechanism *)
+(* Expected time < 1.00s *)
+
+Notation "'bind' x <- y ; z" :=(y (fun x => z)) (at level 99, x at
+  level 0, y at level 0,format "'[hv' 'bind'  x  <-  y ;  '/' z ']'").
+
+Definition f (g : (nat -> nat) -> nat) := g (fun x => 0).
+
+Check (fun g => f g).