Resolve abbreviation aliases in Ltac2

Useful for rewriter in mit-plv/rewriter#159
proux01 · Sep 21, 2024 · fd29066 · fd29066
1 parent 741eefd
commit fd29066
Showing 1 changed file with 1 addition and 1 deletion.
diff --git 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