diff options
Diffstat (limited to 'contrib/xml/proof2aproof.ml')
| -rw-r--r-- | contrib/xml/proof2aproof.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/xml/proof2aproof.ml b/contrib/xml/proof2aproof.ml index dff546c9..678b650c 100644 --- a/contrib/xml/proof2aproof.ml +++ b/contrib/xml/proof2aproof.ml @@ -47,7 +47,7 @@ let nf_evar sigma ~preserve = | _ -> T.mkApp (c', l') ) | _ -> T.mkApp (c', l')) - | T.Evar (e,l) when Evd.in_dom sigma e & Evd.is_defined sigma e -> + | T.Evar (e,l) when Evd.mem sigma e & Evd.is_defined sigma e -> aux (Evd.existential_value sigma (e,l)) | T.Evar (e,l) -> T.mkEvar (e, Array.map aux l) | T.Case (ci,p,c,bl) -> T.mkCase (ci, aux p, aux c, Array.map aux bl) |