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
---
 contrib/correctness/ptactic.ml     | 4 ++--
 contrib/xml/doubleTypeInference.ml | 2 +-
 contrib/xml/proof2aproof.ml        | 2 +-
 3 files changed, 4 insertions(+), 4 deletions(-)

(limited to 'contrib')

diff --git a/contrib/correctness/ptactic.ml b/contrib/correctness/ptactic.ml
index 5994fb38d4..e7610923cd 100644
--- a/contrib/correctness/ptactic.ml
+++ b/contrib/correctness/ptactic.ml
@@ -208,8 +208,8 @@ let reduce_open_constr (em0,c) =
       | Cast (c',t) -> 
 	  (match kind_of_term c' with
 	     | Evar (ev,_) ->
-                 if not (Evd.in_dom em ev) then
-                   Evd.add em ev (Evd.map em0 ev)
+                 if not (Evd.mem em ev) then
+                   Evd.add em ev (Evd.find em0 ev)
                  else
                    em
 	     | _ -> fold_constr collect em c)
diff --git a/contrib/xml/doubleTypeInference.ml b/contrib/xml/doubleTypeInference.ml
index 518f6c115f..a3336817e0 100644
--- a/contrib/xml/doubleTypeInference.ml
+++ b/contrib/xml/doubleTypeInference.ml
@@ -93,7 +93,7 @@ let double_type_of env sigma cstr expectedty subterms_to_types =
         let jty = execute env sigma ty None in
         let jty = assumption_of_judgment env sigma jty in
         let evar_context = 
-	  E.named_context_of_val (Evd.map sigma n).Evd.evar_hyps in
+	  E.named_context_of_val (Evd.find sigma n).Evd.evar_hyps in
          let rec iter actual_args evar_context =
           match actual_args,evar_context with
              [],[] -> ()
diff --git a/contrib/xml/proof2aproof.ml b/contrib/xml/proof2aproof.ml
index dff546c948..678b650cc8 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)
-- 
cgit v1.2.3