diff options
Diffstat (limited to 'vernac/obligations.ml')
| -rw-r--r-- | vernac/obligations.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/obligations.ml b/vernac/obligations.ml index 6dee95bc5..e03e9b803 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -947,7 +947,7 @@ let rec solve_obligation prg num tac = let hook ctx = Lemmas.mk_hook (obligation_hook prg obl num auto ctx) in let () = Lemmas.start_proof_univs ~sign:prg.prg_sign obl.obl_name kind evd (EConstr.of_constr obl.obl_type) ~terminator hook in let _ = Pfedit.by !default_tactic in - Option.iter (fun tac -> Pfedit.set_end_tac tac) tac + Option.iter (fun tac -> Proof_global.set_endline_tactic tac) tac and obligation (user_num, name, typ) tac = let num = pred user_num in |