- 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

1 files changed, 1 insertions, 1 deletions

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