diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/auto.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml index 949db0e0f3..e9424ed0c4 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 |