diff options
Diffstat (limited to 'plugins/ltac/extratactics.mlg')
| -rw-r--r-- | plugins/ltac/extratactics.mlg | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg index ffb597d4cb..40c64a1c26 100644 --- a/plugins/ltac/extratactics.mlg +++ b/plugins/ltac/extratactics.mlg @@ -918,7 +918,7 @@ END VERNAC COMMAND EXTEND GrabEvars STATE proof | [ "Grab" "Existential" "Variables" ] => { classify_as_proofstep } - -> { fun ~pstate -> Declare.Proof.map_proof (fun p -> Proof.V82.grab_evars p) pstate } + -> { fun ~pstate -> Declare.Proof.map ~f:(fun p -> Proof.V82.grab_evars p) pstate } END (* Shelves all the goals under focus. *) @@ -950,7 +950,7 @@ END VERNAC COMMAND EXTEND Unshelve STATE proof | [ "Unshelve" ] => { classify_as_proofstep } - -> { fun ~pstate -> Declare.Proof.map_proof (fun p -> Proof.unshelve p) pstate } + -> { fun ~pstate -> Declare.Proof.map ~f:(fun p -> Proof.unshelve p) pstate } END (* Gives up on the goals under focus: the goals are considered solved, |