From 7ff77d369d3fafa3ddd385f2aba37187a99544a1 Mon Sep 17 00:00:00 2001
From: Pierre Roux <pierre.roux@onera.fr>
Date: Wed, 18 Sep 2024 12:48:23 +0200
Subject: [PATCH] Resolve abbreviation aliases in Ltac2

Useful for rewriter in https://github.com/mit-plv/rewriter/pull/159
---
 plugins/ltac2/tac2core.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/plugins/ltac2/tac2core.ml b/plugins/ltac2/tac2core.ml
index 2dcb9b56d4cd7..ffea42db329e4 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