Continue killing hidden tactics : no more generated h_xxx

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

4 files changed, 17 insertions, 38 deletions

diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4
index e50ea27e55..09c49b3b61 100644
--- a/grammar/tacextend.ml4
+++ b/grammar/tacextend.ml4
@@ -77,24 +77,6 @@ let rec make_args = function
       <:expr< [ Genarg.in_gen $make_wit loc t$ $lid:p$ :: $make_args l$ ] >>
   | _::l -> make_args l
 
-let rec make_eval_tactic e = function
-  | [] -> e
-  | GramNonTerminal(loc,tag,_,Some p)::l when is_tactic_genarg tag ->
-      let loc = of_coqloc loc in
-      let p = Names.string_of_id p in
-      let loc = CompatLoc.merge loc (MLast.loc_of_expr e) in
-      let e = make_eval_tactic e l in
-      <:expr< let $lid:p$ = $lid:p$ in $e$ >>
-  | _::l -> make_eval_tactic e l
-
-let rec make_fun e = function
-  | [] -> e
-  | GramNonTerminal(loc,_,_,Some p)::l ->
-      let loc = of_coqloc loc in
-      let p = Names.string_of_id p in
-      <:expr< fun $lid:p$ -> $make_fun e l$ >>
-  | _::l -> make_fun e l
-
 let mlexpr_terminals_of_grammar_tactic_prod_item_expr = function
   | GramTerminal s -> <:expr< Some $mlexpr_of_string s$ >>
   | GramNonTerminal (loc,nt,_,sopt) ->
@@ -171,18 +153,10 @@ let declare_tactic loc s cl =
   let se = mlexpr_of_string s in
   let pp = make_printing_rule se cl in
   let gl = mlexpr_of_clause cl in
-  let hide_tac (p,e) =
-    (* reste a definir les fonctions cachees avec des noms frais *)
-    let stac = "h_"^s in
-    let e = make_fun (make_eval_tactic e p) p in
-    <:str_item< value $lid:stac$ = $e$ >>
-  in
-  let hidden = if List.length cl = 1 then List.map hide_tac cl else [] in
   let atomic_tactics =
     mlexpr_of_list (mlexpr_of_pair mlexpr_of_string (fun x -> x))
       (possibly_atomic loc cl) in
   declare_str_items loc
-   (hidden @
     [ <:str_item< do {
       try
         let _=Tacinterp.add_tactic $se$ $make_fun_clauses loc s cl$ in
@@ -201,7 +175,7 @@ let declare_tactic loc s cl =
 	     (Errors.print e));
       Egramml.extend_tactic_grammar $se$ $gl$;
       List.iter Pptactic.declare_extra_tactic_pprule $pp$; } >>
-    ])
+    ]
 
 open Pcaml
 open PcamlSig
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