diff options
Diffstat (limited to 'plugins/ltac/extratactics.mlg')
| -rw-r--r-- | plugins/ltac/extratactics.mlg | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg index 5e4969567d..4a2fb425ac 100644 --- a/plugins/ltac/extratactics.mlg +++ b/plugins/ltac/extratactics.mlg @@ -934,7 +934,7 @@ END VERNAC COMMAND EXTEND GrabEvars | ![ proof ] [ "Grab" "Existential" "Variables" ] => { classify_as_proofstep } - -> { fun ~pstate -> Option.map (Proof_global.simple_with_current_proof (fun _ p -> Proof.V82.grab_evars p)) pstate } + -> { fun ~pstate -> Proof_global.modify_proof (fun p -> Proof.V82.grab_evars p) pstate } END (* Shelves all the goals under focus. *) @@ -966,7 +966,7 @@ END VERNAC COMMAND EXTEND Unshelve | ![ proof ] [ "Unshelve" ] => { classify_as_proofstep } - -> { fun ~pstate -> Option.map (Proof_global.simple_with_current_proof (fun _ p -> Proof.unshelve p)) pstate } + -> { fun ~pstate -> Proof_global.modify_proof (fun p -> Proof.unshelve p) pstate } END (* Gives up on the goals under focus: the goals are considered solved, @@ -1118,7 +1118,7 @@ END VERNAC COMMAND EXTEND OptimizeProof | ![ proof ] [ "Optimize" "Proof" ] => { classify_as_proofstep } -> - { fun ~pstate -> Option.map Proof_global.(modify_current_pstate compact_the_proof) pstate } + { fun ~pstate -> Proof_global.compact_the_proof pstate } | [ "Optimize" "Heap" ] => { classify_as_proofstep } -> { Gc.compact () } END |