aboutsummaryrefslogtreecommitdiff
path: root/plugins/ltac/g_ltac.mlg
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ltac/g_ltac.mlg')
-rw-r--r--plugins/ltac/g_ltac.mlg2
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg
index 996f6b3eb3..114acaa412 100644
--- a/plugins/ltac/g_ltac.mlg
+++ b/plugins/ltac/g_ltac.mlg
@@ -363,7 +363,7 @@ let print_info_trace =
let vernac_solve ~pstate n info tcom b =
let open Goal_select in
- let pstate, status = Declare.Proof.map_fold_proof_endline (fun etac p ->
+ let pstate, status = Declare.Proof.map_fold_endline ~f:(fun etac p ->
let with_end_tac = if b then Some etac else None in
let global = match n with SelectAll | SelectList _ -> true | _ -> false in
let info = Option.append info (print_info_trace ()) in