diff options
| author | Gaëtan Gilbert | 2021-03-22 12:42:02 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2021-03-22 13:04:20 +0100 |
| commit | cbe88ec043df8dff118e437f00c0299a464c8e8a (patch) | |
| tree | 704217f492b2a9f55d2149235f268e4d9c1cbdce /proofs/proof.ml | |
| parent | b3347fd5c3164dbe649bd819cdc0ef34b021b47a (diff) | |
Factorize goal selector handling
As a bonus ltac2 can produce bullet suggestions.
Diffstat (limited to 'proofs/proof.ml')
| -rw-r--r-- | proofs/proof.ml | 20 |
1 files changed, 1 insertions, 19 deletions
diff --git a/proofs/proof.ml b/proofs/proof.ml index 50a0e63700..e535536472 100644 --- a/proofs/proof.ml +++ b/proofs/proof.ml @@ -538,25 +538,7 @@ let solve ?with_end_tac gi info_lvl tac pr = let info = Exninfo.reify () in Proofview.tclZERO ~info (SuggestNoSuchGoals (1,pr)) in - let tac = let open Goal_select in match gi with - | SelectAlreadyFocused -> - let open Proofview.Notations in - Proofview.numgoals >>= fun n -> - if n == 1 then tac - else - let e = CErrors.UserError - (None, - Pp.(str "Expected a single focused goal but " ++ - int n ++ str " goals are focused.")) - in - let info = Exninfo.reify () in - Proofview.tclZERO ~info e - - | SelectNth i -> Proofview.tclFOCUS ~nosuchgoal i i tac - | SelectList l -> Proofview.tclFOCUSLIST ~nosuchgoal l tac - | SelectId id -> Proofview.tclFOCUSID ~nosuchgoal id tac - | SelectAll -> tac - in + let tac = Goal_select.tclSELECT ~nosuchgoal gi tac in let tac = if use_unification_heuristics () then Proofview.tclTHEN tac Refine.solve_constraints |