diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/clenv.ml | 2 | ||||
| -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 |
5 files changed, 24 insertions, 21 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 44d3b44077..b529bba3f5 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -298,7 +298,7 @@ let meta_reducible_instance env evd b = if not is_coerce then irec g else u with Not_found -> u) | Proj (p,c) when isMeta evd c || isCast evd c && isMeta evd (pi1 (destCast evd c)) (* What if two nested casts? *) -> - let m = try destMeta evd c with _ -> destMeta evd (pi1 (destCast evd c)) (* idem *) in + let m = try destMeta evd c with DestKO -> destMeta evd (pi1 (destCast evd c)) (* idem *) in (match try let g, s = Metamap.find m metas in 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 |