From cc47337b01227c35dc42ae4b87b0cba20fde9ed5 Mon Sep 17 00:00:00 2001
From: barras
Date: Tue, 13 Jul 2004 14:27:32 +0000
Subject: bug #794: conv made in wrong env

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5897 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/evarutil.ml | 1 -
 1 file changed, 1 deletion(-)

diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 9b29f47a65..bcf212f192 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -478,7 +478,6 @@ let get_changed_pb isevars lev =
 let solve_refl conv_algo env isevars ev argsv1 argsv2 =
   if argsv1 = argsv2 then [] else
   let evd = Evd.map isevars.evars ev in
-  let env = evar_env evd in
   let hyps = evd.evar_hyps in
   let (_,rsign) = 
     array_fold_left2
-- 
cgit v1.2.3