From 97f2cb04e369e07dc87dc15d4871b736776614bd Mon Sep 17 00:00:00 2001
From: msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Fri, 23 May 2008 11:47:43 +0000
Subject: - Fix bug #1858, Hint Unfold calling the wrong locate function. - Fix
 typeclass interface: instance_constructor now takes the instance   constrs as
 argument to build and return the corresponding term and   type. - Better
 typeclass error reporting when defining fixpoints.

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

(limited to 'tactics')

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 949db0e0f..e9424ed0c 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -432,7 +432,7 @@ let add_hints local dbnames0 h =
       add_trivials env sigma (List.map f lhints) local dbnames
   | HintsUnfold lhints ->
       let f r =
-	let r = Syntax_def.locate_global_with_alias (qualid_of_reference r) in
+	let r = Syntax_def.global_with_alias r in
         let r' = match r with
          | ConstRef c -> EvalConstRef c
          | VarRef c -> EvalVarRef c
-- 
cgit v1.2.3