diff options
Diffstat (limited to 'engine/proofview.ml')
| -rw-r--r-- | engine/proofview.ml | 7 |
1 files changed, 7 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 |