From 15682aeca70802dba6f7e13b66521d4ab9e13af9 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 21 Jun 2008 15:19:01 +0000
Subject: Correction petit bug sur révision 11159 (res_pf fait un effet de bord
 sur le sigma, utilisation de refine à la place).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11162 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/equality.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/tactics/equality.ml b/tactics/equality.ml
index 3bfc719e2c..8428560665 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -571,8 +571,9 @@ let discr_positions env sigma (lbeq,(t,t1,t2)) eq_clause cpath dirn sort =
   let (pf, absurd_term) = discrimination_pf e (t,t1,t2) discriminator lbeq in
   let pf_ty = mkArrow eqn absurd_term in
   let absurd_clause = apply_on_clause (pf,pf_ty) eq_clause in
+  let pf = clenv_value_cast_meta absurd_clause in
   tclTHENS (cut_intro absurd_term)
-    [onLastHyp gen_absurdity; res_pf absurd_clause]
+    [onLastHyp gen_absurdity; refine pf]
 
 let discrEq (lbeq,(t,t1,t2) as u) eq_clause gls =
   let sigma = Evd.evars_of eq_clause.evd in
-- 
cgit v1.2.3