From f610068823b33bdc0af752a646df05b98489d7ce Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 11 Jun 2017 06:08:02 +0200 Subject: [proof] Deprecate redundant wrappers. As we would like to reduce the role of proof_global in future versions, we start to deprecate old compatibility aliases in `Pfedit` in favor of the real functions underlying the 8.5 proof engine. We also deprecate a couple of alias types and explicitly mark the few remaining uses of `Pfedit`. --- vernac/obligations.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'vernac/obligations.ml') 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 -- cgit v1.2.3