From cb38fe75f0f846a701b1a3fba8bf5fe1093ce79f Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Sat, 21 Jun 2014 14:00:51 +0200
Subject: Reindex section variables for typeclass resolution if their type
 changed. Fixes bug #3331.

---
 tactics/class_tactics.ml | 18 ++++++++++++------
 1 file changed, 12 insertions(+), 6 deletions(-)

diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 37064b0a7c..31fbc0661d 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -272,12 +272,18 @@ let make_hints g st only_classes sign =
   let paths, hintlist =
     List.fold_left
     (fun (paths, hints) hyp ->
-     if is_section_variable (pi1 hyp) then (paths, hints)
-     else
-       let path, hint =
-	 PathEmpty, pf_apply make_resolve_hyp g st (true,false,false) only_classes None hyp
-       in
-	 (PathOr (paths, path), hint @ hints))
+      let consider =
+	try let (_, b, t) = Global.lookup_named (pi1 hyp) in
+	      (* Section variable, reindex only if the type changed *)
+	      not (eq_constr t (pi3 hyp))
+	with Not_found -> true
+     in
+      if consider then 
+	let path, hint =
+	  PathEmpty, pf_apply make_resolve_hyp g st (true,false,false) only_classes None hyp
+	in
+	  (PathOr (paths, path), hint @ hints)
+      else (paths, hints))
     (PathEmpty, []) sign
   in Hint_db.add_list hintlist (Hint_db.empty st true)
 
-- 
cgit v1.2.3