diff options
| author | Pierre-Marie Pédrot | 2019-02-04 12:18:34 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-02-04 12:18:34 +0100 |
| commit | 6adc5763894fe6da025fd46f5b879af4cc7e99ec (patch) | |
| tree | 6c832ace84b7f0f19170cd2eaedb3617c16bef48 /test-suite | |
| parent | 019123cf911949480d300beba30b63db19c46b7b (diff) | |
| parent | 50bf6109ad0625c81c9776f9ab823a501c574d5b (diff) | |
Merge PR #9452: [proof] optimize proof always works on incomplete proofs
Ack-by: SkySkimmer
Ack-by: ejgallego
Ack-by: gares
Reviewed-by: ppedrot
Diffstat (limited to 'test-suite')
| -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. |