diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/evar_refiner.ml | 2 | ||||
| -rw-r--r-- | proofs/refiner.ml | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml index 0f3fa75843..d5ea25bd30 100644 --- a/proofs/evar_refiner.ml +++ b/proofs/evar_refiner.ml @@ -25,7 +25,7 @@ open Refiner let w_refine env ev rawc evd = if Evd.is_defined (evars_of evd) ev then error "Instantiate called on already-defined evar"; - let e_info = Evd.map (evars_of evd) ev in + let e_info = Evd.find (evars_of evd) ev in let env = Evd.evar_env e_info in let sigma,typed_c = Pretyping.Default.understand_tcc (evars_of evd) env diff --git a/proofs/refiner.ml b/proofs/refiner.ml index 0bb4a9735f..ee4b672a18 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -263,7 +263,7 @@ let extract_open_proof sigma pf = let meta_cnt = ref 0 in let rec f () = incr meta_cnt; - if in_dom sigma (existential_of_int !meta_cnt) then f () + if Evd.mem sigma (existential_of_int !meta_cnt) then f () else !meta_cnt in f in |