diff --git a/plugins/ltac2/tac2core.ml b/plugins/ltac2/tac2core.ml index 2dcb9b56d4cd..ffea42db329e 100644 --- a/plugins/ltac2/tac2core.ml +++ b/plugins/ltac2/tac2core.ml @@ -1751,7 +1751,7 @@ let () = GlbVal (GlobRef.VarRef id), gtypref t_reference | Tac2qexpr.QReference qid -> let gr = - try Nametab.locate qid + try Smartlocate.locate_global_with_alias qid with Not_found as exn -> let _, info = Exninfo.capture exn in Nametab.error_global_not_found ~info qid