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

(limited to 'contrib/xml')

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