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
---
 pretyping/reductionops.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'pretyping/reductionops.ml')

diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 20b48a01ae..9a01250250 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -428,13 +428,13 @@ let whd_betadeltaiota_nolet env sigma x =
 let rec whd_evar sigma c =
   match kind_of_term c with
     | Evar (ev,args)
-        when Evd.in_dom sigma ev & Evd.is_defined sigma ev ->
+        when Evd.mem sigma ev & Evd.is_defined sigma ev ->
 	whd_evar sigma (Evd.existential_value sigma (ev,args))
     | Sort s when is_sort_variable sigma s -> whd_sort_variable sigma c
     | _ -> collapse_appl c
 
-let nf_evar evd =
-  local_strong (whd_evar evd)
+let nf_evar sigma =
+  local_strong (whd_evar sigma)
 
 (* lazy reduction functions. The infos must be created for each term *)
 let clos_norm_flags flgs env sigma t =
-- 
cgit v1.2.3