From 5eb688918550156767c085e1a2e5e4108b586d8a Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 13 Oct 2000 16:15:09 +0000
Subject: Code redondant

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@708 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 proofs/refiner.ml | 13 -------------
 1 file changed, 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
 
-- 
cgit v1.2.3