From 13b78f7cad3cf38ff7c3083494e680a695a54d79 Mon Sep 17 00:00:00 2001
From: puech
Date: Fri, 29 Jul 2011 14:24:52 +0000
Subject: Tactics: generic equality on named_declaration replaced by
 eq_named_declaration

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

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index ce27649d22..6b67a6d60a 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1662,7 +1662,7 @@ let letin_abstract id c (occs,check_occs) gl =
       | None -> depdecls
       | Some occ ->
           let newdecl = subst_term_occ_decl occ c d in
-          if occ = (all_occurrences,InHyp) & d = newdecl then
+          if occ = (all_occurrences,InHyp) && eq_named_declaration d newdecl then
 	    if check_occs & not (in_every_hyp occs)
 	    then raise (RefinerError (DoesNotOccurIn (c,hyp)))
 	    else depdecls
-- 
cgit v1.2.3