From fed48031aad31420f5ffae4b26b0324390191504 Mon Sep 17 00:00:00 2001
From: puech
Date: Fri, 29 Jul 2011 14:29:46 +0000
Subject: Tactics: replace generic = on constr by destructors

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

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 1c1843a124..71ac43c74c 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1395,7 +1395,8 @@ let ipat_of_name = function
 
 let allow_replace c gl = function (* A rather arbitrary condition... *)
   | Some (_, IntroIdentifier id) ->
-      fst (decompose_app ((strip_lam_assum c))) = mkVar id
+      let c = fst (decompose_app ((strip_lam_assum c))) in
+      isVar c && destVar c = id
   | _ ->
       false
 
-- 
cgit v1.2.3