From 7e52f7728dcfcede7e40455385f3eef05a499c0d Mon Sep 17 00:00:00 2001
From: letouzey
Date: Tue, 17 May 2011 20:13:21 +0000
Subject: Class_tactics: Pervasives.(=) don't work for named_context_val (fix
 ATBR)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14135 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 16e38598b5..870e05e4b7 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -259,7 +259,7 @@ let make_autogoal_hints =
     fun only_classes ?(st=full_transparent_state) g ->
     let sign = pf_filtered_hyps g in
       match !res with
-      | Some (sign', hints) when sign = sign' -> hints
+      | Some (sign', hints) when Environ.eq_named_context_val sign sign' -> hints
       | _ -> let hints = make_hints g st only_classes (Environ.named_context_of_val sign) in
 	  res := Some (sign, hints); hints
 	  
-- 
cgit v1.2.3