From d0ed43b5cc0c31b5f0532753587f641716246bb7 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 14 Nov 2020 21:29:52 +0100
Subject: Fixes #11816: using {wf ...} in a local fixpoint is an error, not an
 anomaly.

---
 test-suite/bugs/closed/bug_11816.v | 2 ++
 1 file changed, 2 insertions(+)
 create mode 100644 test-suite/bugs/closed/bug_11816.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/bug_11816.v b/test-suite/bugs/closed/bug_11816.v
new file mode 100644
index 0000000000..82a317b250
--- /dev/null
+++ b/test-suite/bugs/closed/bug_11816.v
@@ -0,0 +1,2 @@
+(* This should be an error, not an anomaly *)
+Fail Definition foo := fix foo (n : nat) { wf n n } := 0.
-- 
cgit v1.2.3