From cbe88ec043df8dff118e437f00c0299a464c8e8a Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Mon, 22 Mar 2021 12:42:02 +0100
Subject: Factorize goal selector handling

As a bonus ltac2 can produce bullet suggestions.
---
 plugins/ltac/tacinterp.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins')

diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 54d7c310aa..da95869abb 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -1180,7 +1180,7 @@ and eval_tactic_ist ist tac : unit Proofview.tactic = match tac with
   | TacSolve l -> Tacticals.New.tclSOLVE (List.map (interp_tactic ist) l)
   | TacComplete tac -> Tacticals.New.tclCOMPLETE (interp_tactic ist tac)
   | TacArg {CAst.loc} -> Ftactic.run (val_interp (ensure_loc loc ist) tac) (fun v -> tactic_of_value ist v)
-  | TacSelect (sel, tac) -> Tacticals.New.tclSELECT sel (interp_tactic ist tac)
+  | TacSelect (sel, tac) -> Goal_select.tclSELECT sel (interp_tactic ist tac)
   (* For extensions *)
   | TacAlias {loc; v=(s,l)} ->
       let alias = Tacenv.interp_alias s in
-- 
cgit v1.2.3