fixed kernel bug (de Bruijn) + test-suite

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

1 files changed, 11 insertions, 0 deletions

diff --git a/test-suite/success/guard.v b/test-suite/success/guard.v
new file mode 100644
index 000000000..b9181d430
--- /dev/null
+++ b/test-suite/success/guard.v
@@ -0,0 +1,11 @@
+(* Specific tests about guard condition *)
+
+(* f must unfold to x, not F (de Bruijn mix-up!) *)
+Check let x (f:nat->nat) k := f k in
+      fun (y z:nat->nat) =>
+      let f:=x in (* f := Rel 3 *)
+      fix F (n:nat) : nat :=
+        match n with
+        | 0 => 0
+        | S k => f F k (* here Rel 3 = F ! *)
+        end.