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 | |
| parent | b3347fd5c3164dbe649bd819cdc0ef34b021b47a (diff) | |
Factorize goal selector handling
As a bonus ltac2 can produce bullet suggestions.
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/goal_select.ml | 19 | ||||
| -rw-r--r-- | proofs/goal_select.mli | 2 | ||||
| -rw-r--r-- | proofs/proof.ml | 20 | ||||
| -rw-r--r-- | proofs/proofs.mllib | 2 |
4 files changed, 23 insertions, 20 deletions
diff --git a/proofs/goal_select.ml b/proofs/goal_select.ml index e847535aaf..68646c93c9 100644 --- a/proofs/goal_select.ml +++ b/proofs/goal_select.ml @@ -57,3 +57,22 @@ let get_default_goal_selector = ~value:(SelectNth 1) parse_goal_selector (fun v -> Pp.string_of_ppcmds @@ pr_goal_selector v) + +(* Select a subset of the goals *) +let tclSELECT ?nosuchgoal g tac = match g with + | SelectNth i -> Proofview.tclFOCUS ?nosuchgoal i i tac + | SelectList l -> Proofview.tclFOCUSLIST ?nosuchgoal l tac + | SelectId id -> Proofview.tclFOCUSID ?nosuchgoal id tac + | SelectAll -> tac + | 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 diff --git a/proofs/goal_select.mli b/proofs/goal_select.mli index 977392baa6..c6726300f0 100644 --- a/proofs/goal_select.mli +++ b/proofs/goal_select.mli @@ -24,3 +24,5 @@ type t = val pr_goal_selector : t -> Pp.t val get_default_goal_selector : unit -> t + +val tclSELECT : ?nosuchgoal:'a Proofview.tactic -> t -> 'a Proofview.tactic -> 'a Proofview.tactic 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 diff --git a/proofs/proofs.mllib b/proofs/proofs.mllib index 5f19c1bb09..43cde83e58 100644 --- a/proofs/proofs.mllib +++ b/proofs/proofs.mllib @@ -2,9 +2,9 @@ Miscprint Goal Evar_refiner Refine +Goal_select Proof Logic -Goal_select Proof_bullet Tacmach Clenv |