From dda7c7bb0b6ea0c2106459d8ae208eff0dfd6738 Mon Sep 17 00:00:00 2001
From: filliatr
Date: Wed, 1 Dec 1999 08:03:06 +0000
Subject:  - Typing -> Safe_typing  - proofs/Typing_ev -> pretyping/Typing  -
 env -> sign  - fonctions var_context

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@167 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/reduction.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'kernel/reduction.ml')

diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 4bc551c6aa..2ce121ed12 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -1296,17 +1296,17 @@ let nf_ise1 sigma = strong (fun _ -> whd_ise1) empty_env sigma
 (* Same as whd_ise1, but replaces the remaining ISEVAR by Metavariables
  * Similarly we have is_fmachine1_metas and is_resolve1_metas *)
 
-let rec whd_ise1_metas env sigma = function
+let rec whd_ise1_metas sigma = function
   | (DOPN(Evar n,_) as k) ->
       if Evd.in_dom sigma n then
 	if Evd.is_defined sigma n then
-      	  whd_ise1_metas env sigma (existential_value sigma k)
+      	  whd_ise1_metas sigma (existential_value sigma k)
 	else 
       	  let m = DOP0(Meta (new_meta())) in
 	  DOP2(Cast,m,existential_type sigma k)
       else
 	k
-  | DOP2(Cast,c,_) -> whd_ise1_metas env sigma c
+  | DOP2(Cast,c,_) -> whd_ise1_metas sigma c
   | c -> c
 
 
-- 
cgit v1.2.3