diff options
| author | Pierre-Marie Pédrot | 2021-03-24 11:19:13 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2021-03-24 11:19:13 +0100 |
| commit | e80d2ddc7db13c861c865ed5acf7708f99f125ec (patch) | |
| tree | aaf168349be1f96c05ccd9b89bfb16c1159c8b6f /plugins/ltac | |
| parent | 47c20236f578dca9381822a62b5a406d6b42676d (diff) | |
| parent | cbe88ec043df8dff118e437f00c0299a464c8e8a (diff) | |
Merge PR #13973: Factorize goal selector handling
Reviewed-by: ppedrot
Diffstat (limited to 'plugins/ltac')
| -rw-r--r-- | plugins/ltac/tacinterp.ml | 2 |
1 files changed, 1 insertions, 1 deletions
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 |