diff options
Diffstat (limited to 'engine/proofview.ml')
| -rw-r--r-- | engine/proofview.ml | 13 |
1 files changed, 7 insertions, 6 deletions
diff --git a/engine/proofview.ml b/engine/proofview.ml index fd8512d73e..0ed945f5d4 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -230,8 +230,7 @@ let apply ~name ~poly env t sp = match ans with | Nil (e, info) -> Exninfo.iraise (TacticFailure e, info) | Cons ((r, (state, _), status, info), _) -> - let (status, gaveup) = status in - let status = (status, state.shelf, gaveup) in + let status = (status, state.shelf) in let state = { state with shelf = [] } in r, state, status, Trace.to_tree info @@ -833,14 +832,18 @@ let mark_as_unsafe = Status.put false (** Gives up on the goal under focus. Reports an unsafe status. Proofs with given up goals cannot be closed. *) + +let give_up evs pv = + let solution = List.fold_left (fun sigma ev -> Evd.give_up (drop_state ev) sigma) pv.solution evs in + { pv with solution } + let give_up = let open Proof in Comb.get >>= fun initial -> Comb.set [] >> mark_as_unsafe >> InfoL.leaf (Info.Tactic (fun _ _ -> Pp.str"give_up")) >> - Giveup.put (CList.map drop_state initial) - + Pv.modify (give_up initial) (** {7 Control primitives} *) @@ -1008,8 +1011,6 @@ module Unsafe = struct let tclPUTSHELF to_shelve = tclBIND tclGETSHELF (fun shelf -> tclSETSHELF (to_shelve@shelf)) - let tclPUTGIVENUP = Giveup.put - let tclEVARSADVANCE evd = Pv.modify (fun ps -> { ps with solution = evd; comb = undefined evd ps.comb }) |