From b36a4fe2708d54c5bf973763610e0553c8bb8eb3 Mon Sep 17 00:00:00 2001
From: puech
Date: Fri, 29 Jul 2011 14:26:55 +0000
Subject: Class_tactics: generic equality on named_context_val replaced by
 eq_named_context_val

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

diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index aed9f59857..be81e329d7 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -352,7 +352,7 @@ let hints_tac hints =
 			  { info with auto_depth = j :: i :: info.auto_depth; auto_last_tac = pp;
 			      is_evar = evar;
 			      hints =
-			      if b && Goal.V82.hyps s' g <> Goal.V82.hyps s' gl
+			      if b && not (Environ.eq_named_context_val (Goal.V82.hyps s' g) (Goal.V82.hyps s' gl))
 			      then make_autogoal_hints info.only_classes
 				~st:(Hint_db.transparent_state info.hints) {it = g; sigma = s'}
 			      else info.hints }
-- 
cgit v1.2.3