summaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed/3993.v
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/bugs/closed/3993.v')
-rw-r--r--test-suite/bugs/closed/3993.v3
1 files changed, 3 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/3993.v b/test-suite/bugs/closed/3993.v
new file mode 100644
index 00000000..086d8dd0
--- /dev/null
+++ b/test-suite/bugs/closed/3993.v
@@ -0,0 +1,3 @@
+(* Test smooth failure on not fully applied term to destruct with eqn: given *)
+Goal True.
+Fail induction S eqn:H.