Imported Upstream version 8.2~rc2+dfsgupstream/8.2.rc2+dfsg

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 00000000..b9181d43
--- /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.