3 files changed, 16 insertions, 11 deletions
diff --git a/tactics/eqdecide.ml4 b/tactics/eqdecide.ml4
index df85e564eb..6500b0e53a 100644
--- a/tactics/eqdecide.ml4
+++ b/tactics/eqdecide.ml4
@@ -70,7 +70,7 @@ let mkBranches c1 c2 =
 let solveNoteqBranch side =
   tclTHEN (choose_noteq side)
     (tclTHEN introf
-      (onLastHypId (fun id -> Extratactics.h_discrHyp id)))
+      (onLastHypId (fun id -> Extratactics.discrHyp id)))
 
 (* Constructs the type {c1=c2}+{~c1=c2} *)
 
@@ -106,7 +106,7 @@ let diseqCase eqonleft =
   (tclTHEN  red_in_concl
   (tclTHEN  (intro_using absurd)
   (tclTHEN  (h_simplest_apply (mkVar diseq))
-  (tclTHEN  (Extratactics.h_injHyp absurd)
+  (tclTHEN  (Extratactics.injHyp absurd)
             (full_trivial [])))))))
 
 let solveArg eqonleft op a1 a2 tac g =
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index a3fa9956e7..c2d5de2653 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -93,9 +93,11 @@ TACTIC EXTEND esimplify_eq
     [ dEq true (Some (induction_arg_of_quantified_hyp h)) ]
 END
 
+let discr_main c = elimOnConstrWithHoles discr_tac false c
+
 TACTIC EXTEND discriminate_main
 | [ "discriminate" constr_with_bindings(c) ] ->
-    [ elimOnConstrWithHoles discr_tac false c ]
+    [ discr_main c ]
 END
 TACTIC EXTEND discriminate
 | [ "discriminate" ] -> [ discr_tac false None ]
@@ -112,12 +114,15 @@ TACTIC EXTEND ediscriminate
     [ discr_tac true (Some (induction_arg_of_quantified_hyp h)) ]
 END
 
-let h_discrHyp id gl =
-  h_discriminate_main {it = Term.mkVar id,NoBindings; sigma = Refiner.project gl} gl
+let discrHyp id gl =
+  discr_main {it = Term.mkVar id,NoBindings; sigma = Refiner.project gl} gl
+
+let injection_main c =
+ elimOnConstrWithHoles (injClause []) false c
 
 TACTIC EXTEND injection_main
 | [ "injection" constr_with_bindings(c) ] ->
-    [ elimOnConstrWithHoles (injClause []) false c ]
+    [ injection_main c ]
 END
 TACTIC EXTEND injection
 | [ "injection" ] -> [ injClause [] false None ]
@@ -153,8 +158,8 @@ TACTIC EXTEND einjection_as
     [ injClause ipat true (Some (induction_arg_of_quantified_hyp h)) ]
 END
 
-let h_injHyp id gl =
-  h_injection_main { it = Term.mkVar id,NoBindings; sigma = Refiner.project gl } gl
+let injHyp id gl =
+  injection_main { it = Term.mkVar id,NoBindings; sigma = Refiner.project gl } gl
 
 TACTIC EXTEND dependent_rewrite
 | [ "dependent" "rewrite" orient(b) constr(c) ] -> [ rewriteInConcl b c ]
@@ -313,7 +318,7 @@ TACTIC EXTEND refine
   [ "refine" casted_open_constr(c) ] -> [ refine c ]
 END
 
-let refine_tac = h_refine
+let refine_tac = refine
 
 (**********************************************************************)
 (* Inversion lemmas (Leminv)                                          *)
diff --git a/tactics/extratactics.mli b/tactics/extratactics.mli
index 3f30ddb425..ad72a4aac0 100644
--- a/tactics/extratactics.mli
+++ b/tactics/extratactics.mli
@@ -8,8 +8,8 @@
 
 open Proof_type
 
-val h_discrHyp : Names.identifier -> tactic
-val h_injHyp : Names.identifier -> tactic
+val discrHyp : Names.identifier -> tactic
+val injHyp : Names.identifier -> tactic
 
 val refine_tac : Evd.open_constr -> tactic