Code redondant

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@708 85f007b7-540e-0410-9357-904b9bb8a0f7

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