diff options
| author | Maxime Dénès | 2017-11-08 13:00:14 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2017-11-08 13:00:14 +0100 |
| commit | d9f79d97dbc503e149cba2df1b228a94d7ac970b (patch) | |
| tree | d34f23cbf0a05f9351bff43276e1a9914fdc8a1f /proofs/pfedit.ml | |
| parent | e38df89db1b7cd9d201569a39a6a935299317f3e (diff) | |
| parent | 9402b6efad32757f44d72d83f6aabdca8829e3ed (diff) | |
Merge PR #6100: [api] Remove 8.7 ML-deprecated functions.
Diffstat (limited to 'proofs/pfedit.ml')
| -rw-r--r-- | proofs/pfedit.ml | 28 |
1 files changed, 0 insertions, 28 deletions
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 469e1a011e..2d4aba17cb 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -230,31 +230,3 @@ let apply_implicit_tactic tac = (); fun env sigma evk -> let solve_by_implicit_tactic () = match !implicit_tactic with | None -> None | Some tac -> Some (apply_implicit_tactic tac) - -(** Deprecated functions *) -let refining = Proof_global.there_are_pending_proofs -let check_no_pending_proofs = Proof_global.check_no_pending_proof - -let get_current_proof_name = Proof_global.get_current_proof_name -let get_all_proof_names = Proof_global.get_all_proof_names - -type lemma_possible_guards = Proof_global.lemma_possible_guards - -let delete_proof = Proof_global.discard -let delete_current_proof = Proof_global.discard_current -let delete_all_proofs = Proof_global.discard_all - -let get_pftreestate () = - Proof_global.give_me_the_proof () - -let set_end_tac tac = - Proof_global.set_endline_tactic tac - -let set_used_variables l = - Proof_global.set_used_variables l - -let get_used_variables () = - Proof_global.get_used_variables () - -let get_universe_decl () = - Proof_global.get_universe_decl () |