diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-06-11 06:08:02 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-06-11 15:54:48 +0200 |
| commit | f610068823b33bdc0af752a646df05b98489d7ce (patch) | |
| tree | 5d664bd1b3efb43536250b30b0dffa724e28dba4 /vernac/obligations.ml | |
| parent | 79c42e22dd5106dcb85229ceec75331029ab5486 (diff) | |
[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`.
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 |