diff options
| -rw-r--r-- | proofs/refiner.ml | 13 |
1 files changed, 0 insertions, 13 deletions
diff --git a/proofs/refiner.ml b/proofs/refiner.ml index af3f15ef48..048ce3721f 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -212,19 +212,6 @@ let refiner = function let context ctxt = refiner (Context ctxt) let vernac_tactic texp = refiner (Tactic texp) -(* hide_tactic s tac pr registers a tactic s under the name s *) - -let hide_tactic s tac = - add_tactic s tac; - (fun args -> vernac_tactic(s,args)) - -(* overwriting_register_tactic s tac pr registers a tactic s under the - name s even if a tactic of the same name is already registered *) - -let overwrite_hidden_tactic s tac = - overwriting_add_tactic s tac; - (fun args -> vernac_tactic(s,args)) - (* rc_of_pfsigma : proof sigma -> readable_constraints *) let rc_of_pfsigma sigma = rc_of_gc sigma.sigma sigma.it.goal |