diff options
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/proofview.ml | 7 | ||||
| -rw-r--r-- | engine/proofview.mli | 10 |
2 files changed, 17 insertions, 0 deletions
diff --git a/engine/proofview.ml b/engine/proofview.ml index b8f49a9c84..d876860652 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -618,6 +618,13 @@ let shelve = InfoL.leaf (Info.Tactic (fun () -> Pp.str"shelve")) >> Shelf.modify (fun gls -> gls @ initial) +let shelve_goals l = + let open Proof in + Comb.get >>= fun initial -> + let comb = CList.filter (fun g -> not (CList.mem g l)) initial in + Comb.set comb >> + InfoL.leaf (Info.Tactic (fun () -> Pp.str"shelve_goals")) >> + Shelf.modify (fun gls -> gls @ l) (** [contained_in_info e evi] checks whether the evar [e] appears in the hypotheses, the conclusion or the body of the evar_info diff --git a/engine/proofview.mli b/engine/proofview.mli index 0b63164b09..901cf26e0e 100644 --- a/engine/proofview.mli +++ b/engine/proofview.mli @@ -300,6 +300,16 @@ val tclINDEPENDENT : unit tactic -> unit tactic shelf for later use (or being solved by side-effects). *) val shelve : unit tactic +(** Shelves the given list of goals, which might include some that are + under focus and some that aren't. All the goals are placed on the + shelf for later use (or being solved by side-effects). *) +val shelve_goals : Goal.goal list -> unit tactic + +(** [unifiable sigma g l] checks whether [g] appears in another + subgoal of [l]. The list [l] may contain [g], but it does not + affect the result. Used by [shelve_unifiable]. *) +val unifiable : Evd.evar_map -> Goal.goal -> Goal.goal list -> bool + (** Shelves the unifiable goals under focus, i.e. the goals which appear in other goals under focus (the unfocused goals are not considered). *) |