diff options
| author | Enrico Tassi | 2019-01-31 18:13:49 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2019-01-31 18:13:49 +0100 |
| commit | 50bf6109ad0625c81c9776f9ab823a501c574d5b (patch) | |
| tree | 19945c81feded1af5979b3cfb787674c7a84d140 | |
| parent | 54f0149481afaeacf7c41dc131aab16dbe29379b (diff) | |
add test
| -rw-r--r-- | test-suite/bugs/closed/bug_9451.v | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/bug_9451.v b/test-suite/bugs/closed/bug_9451.v new file mode 100644 index 0000000000..03bb0433f1 --- /dev/null +++ b/test-suite/bugs/closed/bug_9451.v @@ -0,0 +1,8 @@ +Goal False. +cut True. +assert False. +evar (x : True). +let v := open_constr:(_) in idtac. all: exfalso; clear. +Optimize Proof. +(* Error: Anomaly "grounding a non evar-free term" *) +Abort All. |