From a184d54b95c40bc2890fc91f236bbdf983ebc83d Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 28 Apr 2006 12:24:14 +0000
Subject: Standardisation du nom des méthodes de Evd

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8759 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 proofs/evar_refiner.ml | 2 +-
 proofs/refiner.ml      | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'proofs')

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
-- 
cgit v1.2.3