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 /engine | |
| 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 'engine')
| -rw-r--r-- | engine/proofview.ml | 2 |
1 files changed, 1 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 |