diff options
| -rw-r--r-- | engine/proofview.ml | 2 | ||||
| -rw-r--r-- | test-suite/bugs/closed/bug_9451.v | 8 |
2 files changed, 9 insertions, 1 deletions
diff --git a/engine/proofview.ml b/engine/proofview.ml index cf4224bbdb..d4ad53ff5f 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -39,7 +39,7 @@ let proofview p = let compact el ({ solution } as pv) = let nf c = Evarutil.nf_evar solution c in - let nf0 c = EConstr.(to_constr solution (of_constr c)) in + let nf0 c = EConstr.(to_constr ~abort_on_undefined_evars:false solution (of_constr c)) in let size = Evd.fold (fun _ _ i -> i+1) solution 0 in let new_el = List.map (fun (t,ty) -> nf t, nf ty) el in let pruned_solution = Evd.drop_all_defined solution in 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. |