From 9d63bf75ffc312b367301dd66d2d6c3896fd71cf Mon Sep 17 00:00:00 2001
From: msozeau
Date: Mon, 23 Jan 2012 20:51:46 +0000
Subject: Fix bug #2483: anomaly raised due to wrong handling of the evars
 state.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14942 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/rewrite.ml4 | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4
index d297969d1f..1cc1b27fe0 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -257,7 +257,7 @@ let decompose_applied_relation env sigma flags orig (c,l) left2right =
   let ctype = Typing.type_of env sigma c' in
   let find_rel ty =
     let eqclause = Clenv.make_clenv_binding_env_apply env sigma None (c',ty) l in
-    let (equiv, args) = decompose_app_rel env sigma (Clenv.clenv_type eqclause) in
+    let (equiv, args) = decompose_app_rel env eqclause.evd (Clenv.clenv_type eqclause) in
     let c1 = args.(0) and c2 = args.(1) in 
     let ty1, ty2 =
       Typing.type_of env eqclause.evd c1, Typing.type_of env eqclause.evd c2
-- 
cgit v1.2.3