From c4d6bd430c4ba0cbc0c9d444583c8291537ebc3e Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 11 Jan 2001 13:51:20 +0000
Subject: Bug environnement

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1242 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/coercion.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 9193425854..428af0a4a8 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -119,7 +119,7 @@ let rec inh_conv_coerce_to_fail env isevars c1 hj =
              then 
 	       let (x,v1,v2) = destLambda v' in
                let env1 = push_rel_assum (x,v1) env in
-               let h2 = inh_conv_coerce_to_fail env isevars u2
+               let h2 = inh_conv_coerce_to_fail env1 isevars u2
 			  {uj_val = v2; uj_type = t2 } in
                fst (abs_rel env !isevars x v1 h2)
              else 
@@ -131,7 +131,7 @@ let rec inh_conv_coerce_to_fail env isevars c1 hj =
 		 inh_conv_coerce_to_fail env isevars t1
 		   {uj_val = mkRel 1; 
 		    uj_type = u1 } in
-               let h2 = inh_conv_coerce_to_fail env isevars u2  
+               let h2 = inh_conv_coerce_to_fail env1 isevars u2  
 			 { uj_val = mkApp (lift 1 v, [|h1.uj_val|]);
                            uj_type = subst1 h1.uj_val t2 }
 	       in
-- 
cgit v1.2.3