Remove the Hiddentac module.

Since the new proof engine, Hiddentac has been essentially trivial.
Here is what happened to the functions defined there
- Aliases, or tactics that were trivial to inline were systematically inlined
- Tactics used only in tacinterp have been moved to tacinterp
- Other tactics have been moved to a new module Tactics.Simple.

17 files changed, 175 insertions, 355 deletions

diff --git a/dev/base_include b/dev/base_include
index 87c0e5b7e..94146102b 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -136,7 +136,6 @@ open Equality
 open Evar_tactics
 open Extraargs
 open Extratactics
-open Hiddentac
 open Hipattern
 open Inv
 open Leminv
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 3d74c5bc9..52ba41869 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -9,7 +9,6 @@ open Names
 open Declarations
 open Declareops
 open Pp
-open Hiddentac
 open Tacmach
 open Proof_type
 open Tacticals
@@ -120,7 +119,7 @@ type body_info = constr dynamic_info
 
 let finish_proof dynamic_infos g =
   observe_tac "finish"
-    (Proofview.V82.of_tactic h_assumption)
+    (Proofview.V82.of_tactic assumption)
     g
 
 
@@ -179,7 +178,7 @@ let change_hyp_with_using msg hyp_id t tac : tactic =
       [tclTHENLIST
       [
 	(* observe_tac "change_hyp_with_using thin" *) (thin [hyp_id]);
-	(* observe_tac "change_hyp_with_using rename " *) (h_rename [prov_id,hyp_id])
+	(* observe_tac "change_hyp_with_using rename " *) (rename_hyp [prov_id,hyp_id])
       ]] g
 
 exception TOREMOVE
@@ -370,7 +369,7 @@ let isLetIn t =
 
 
 let h_reduce_with_zeta =
-  h_reduce
+  reduce
     (Genredexpr.Cbv
        {Redops.all_flags
 	with Genredexpr.rDelta = false;
@@ -638,7 +637,7 @@ let instanciate_hyps_with_args (do_prove:Id.t list -> tactic) hyps args_id =
 	  tclTHENLIST[
 	    Proofview.V82.of_tactic (pose_proof (Name prov_hid) (mkApp(mkVar hid,args)));
 	    thin [hid];
-	    h_rename [prov_hid,hid]
+	    rename_hyp [prov_hid,hid]
 	  ] g
       )
       ( (*
@@ -700,11 +699,11 @@ let build_proof
 		  in
 		  tclTHENSEQ
 		    [
-		      h_generalize (term_eq::(List.map mkVar dyn_infos.rec_hyps));
+		      Simple.generalize (term_eq::(List.map mkVar dyn_infos.rec_hyps));
 		      thin dyn_infos.rec_hyps;
 		      pattern_option [Locus.AllOccurrencesBut [1],t] None;
 		      (fun g -> observe_tac "toto" (
-			 tclTHENSEQ [Proofview.V82.of_tactic (h_simplest_case t);
+			 tclTHENSEQ [Proofview.V82.of_tactic (Simple.case t);
 				     (fun g' ->
 					let g'_nb_prod = nb_prod (pf_concl g') in
 					let nb_instanciate_partial = g'_nb_prod - g_nb_prod in
@@ -925,7 +924,7 @@ let generalize_non_dep hyp g =
   in
 (*   observe (str "to_revert := " ++ prlist_with_sep spc Ppconstr.pr_id to_revert); *)
   tclTHEN
-    ((* observe_tac "h_generalize" *) (h_generalize  (List.map mkVar to_revert) ))
+    ((* observe_tac "h_generalize" *) (Simple.generalize  (List.map mkVar to_revert) ))
     ((* observe_tac "thin" *) (thin to_revert))
     g
 
@@ -970,7 +969,7 @@ let generate_equation_lemma fnames f fun_num nb_params nb_args rec_args_num =
 	   let rec_id = pf_nth_hyp_id g 1 in
 	   tclTHENSEQ
 	     [(* observe_tac "generalize_non_dep in generate_equation_lemma" *) (generalize_non_dep rec_id);
-	      (* observe_tac "h_case" *) (Proofview.V82.of_tactic (h_case false (mkVar rec_id,NoBindings)));
+	      (* observe_tac "h_case" *) (Proofview.V82.of_tactic (general_case_analysis false (mkVar rec_id,NoBindings)));
 	      (Proofview.V82.of_tactic intros_reflexivity)] g
 	)
       ]
@@ -1198,10 +1197,10 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams :
 	    in
 	    if List.is_empty other_fix_infos
 	    then
-	      (* observe_tac ("h_fix") *) (h_fix (Some this_fix_info.name) (this_fix_info.idx +1))
+	      (* observe_tac ("h_fix") *) (fix (Some this_fix_info.name) (this_fix_info.idx +1))
 	    else
-	      h_mutual_fix this_fix_info.name (this_fix_info.idx + 1)
-		other_fix_infos
+	      Tactics.mutual_fix this_fix_info.name (this_fix_info.idx + 1)
+		other_fix_infos 0
 	| _ -> anomaly (Pp.str "Not a valid information")
     in
     let first_tac : tactic = (* every operations until fix creations *)
@@ -1536,7 +1535,7 @@ let prove_principle_for_gen
     Nameops.out_name (fresh_id (Name (Id.of_string ("Acc_"^(Id.to_string rec_arg_id)))))
   in
   let revert l =
-    tclTHEN (h_generalize (List.map mkVar l)) (clear l)
+    tclTHEN (Tactics.Simple.generalize (List.map mkVar l)) (clear l)
   in
   let fix_id = Nameops.out_name (fresh_id (Name hrec_id)) in
   let prove_rec_arg_acc g =
@@ -1549,7 +1548,7 @@ let prove_principle_for_gen
 	       (
 		 (* observe_tac  *)
 (* 		   "apply wf_thm"  *)
-		 h_simplest_apply (mkApp(mkVar wf_thm_id,[|mkVar rec_arg_id|]))
+		 Tactics.Simple.apply (mkApp(mkVar wf_thm_id,[|mkVar rec_arg_id|]))
 	       )
 	    )
 	 )
@@ -1583,7 +1582,7 @@ let prove_principle_for_gen
       tclTHENSEQ
 	[
 	  generalize [lemma];
-	  Proofview.V82.of_tactic (h_intro hid);
+	  Proofview.V82.of_tactic (Simple.intro hid);
 	  Proofview.V82.of_tactic (Elim.h_decompose_and (mkVar hid));
 	  (fun g ->
 	     let new_hyps = pf_ids_of_hyps g in
@@ -1614,7 +1613,7 @@ let prove_principle_for_gen
 (*       observe_tac "reverting" *) (revert (List.rev (acc_rec_arg_id::args_ids)));
 (*       (fun g -> observe (Printer.pr_goal (sig_it g) ++ fnl () ++  *)
 (* 			   str "fix arg num" ++ int (List.length args_ids + 1) ); tclIDTAC g); *)
-      (* observe_tac "h_fix " *) (h_fix (Some fix_id) (List.length args_ids + 1));
+      (* observe_tac "h_fix " *) (fix (Some fix_id) (List.length args_ids + 1));
 (*       (fun g -> observe (Printer.pr_goal (sig_it g) ++ fnl() ++ pr_lconstr_env (pf_env g ) (pf_type_of g (mkVar fix_id) )); tclIDTAC g); *)
       h_intros (List.rev (acc_rec_arg_id::args_ids));
       Proofview.V82.of_tactic (Equality.rewriteLR (mkConst eq_ref));
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 4f32feb24..3dc59b7ca 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -106,7 +106,7 @@ let functional_induction with_clean c princl pat =
 	in
 	Tacticals.tclTHEN
 	  (Tacticals.tclMAP (fun id -> Tacticals.tclTRY (Proofview.V82.of_tactic (Equality.subst_gen (do_rewrite_dependent ()) [id]))) idl )
-	  (Hiddentac.h_reduce flag Locusops.allHypsAndConcl)
+	  (Tactics.reduce flag Locusops.allHypsAndConcl)
 	  g
       else Tacticals.tclIDTAC g
     in
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index e5b975e14..b7072ea3b 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -3,7 +3,6 @@ open Pp
 open Libnames
 open Globnames
 open Refiner
-open Hiddentac 
 let mk_prefix pre id = Id.of_string (pre^(Id.to_string id))
 let mk_rel_id = mk_prefix "R_"
 let mk_correct_id id = Nameops.add_suffix (mk_rel_id id) "_correct"
@@ -484,7 +483,7 @@ let jmeq_refl () =
   with e when Errors.noncritical e -> raise (ToShow e)
 
 let h_intros l =
-  tclMAP (fun x -> Proofview.V82.of_tactic (h_intro x)) l
+  tclMAP (fun x -> Proofview.V82.of_tactic (Tactics.Simple.intro x)) l
 
 let h_id = Id.of_string "h"
 let hrec_id = Id.of_string "hrec"
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 36de85595..0d32bf2bc 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -18,7 +18,6 @@ open Tacticals
 open Tactics
 open Indfun_common
 open Tacmach
-open Hiddentac
 open Misctypes
 
 (* Some pretty printing function for debugging purpose *)
@@ -399,11 +398,11 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
 	    observe_tac("h_intro_patterns ")  (let l = (List.nth intro_pats (pred i)) in 
 					       match l with 
 						 | [] -> tclIDTAC 
-						 | _ -> Proofview.V82.of_tactic (h_intro_patterns l));
+						 | _ -> Proofview.V82.of_tactic (intro_patterns l));
 	    (* unfolding of all the defined variables introduced by this branch *)
 	    (* observe_tac "unfolding" pre_tac; *)
 	    (* $zeta$ normalizing of the conclusion *)
-	    h_reduce
+	    reduce
 	      (Genredexpr.Cbv
 		 { Redops.all_flags with
 		     Genredexpr.rDelta = false ;
@@ -414,11 +413,11 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
 	    observe_tac ("toto ") tclIDTAC;
     
 	    (* introducing the the result of the graph and the equality hypothesis *)
-	    observe_tac "introducing" (tclMAP (fun x -> Proofview.V82.of_tactic (h_intro x)) [res;hres]);
+	    observe_tac "introducing" (tclMAP (fun x -> Proofview.V82.of_tactic (Simple.intro x)) [res;hres]);
 	    (* replacing [res] with its value *)
 	    observe_tac "rewriting res value" (Proofview.V82.of_tactic (Equality.rewriteLR (mkVar hres)));
 	    (* Conclusion *)
-	    observe_tac "exact" (fun g -> h_exact (app_constructor g) g)  
+	    observe_tac "exact" (fun g -> exact_check (app_constructor g) g)  
 	  ]
       )
 	g
@@ -469,8 +468,8 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
 	observe_tac "principle" (Proofview.V82.of_tactic (assert_by
 	  (Name principle_id)
 	  princ_type
-	  (Proofview.V82.tactic (h_exact f_principle))));
-	observe_tac "intro args_names" (tclMAP (fun id -> Proofview.V82.of_tactic (h_intro id)) args_names);
+	  (Proofview.V82.tactic (exact_check f_principle))));
+	observe_tac "intro args_names" (tclMAP (fun id -> Proofview.V82.of_tactic (Simple.intro id)) args_names);
 	(* observe_tac "titi" (pose_proof (Name (Id.of_string "__")) (Reductionops.nf_beta Evd.empty  ((mkApp (mkVar principle_id,Array.of_list bindings))))); *)
 	observe_tac "idtac" tclIDTAC;
 	tclTHEN_i
@@ -653,7 +652,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
 	    (* replacing [res] with its value *)
 	    observe_tac "rewriting res value" (Equality.rewriteLR (mkVar hres));
 	    (* Conclusion *)
-	    observe_tac "exact" (h_exact app_constructor)
+	    observe_tac "exact" (exact_check app_constructor)
 	  ]
       )
 	g
@@ -692,7 +691,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
 	observe_tac "principle" (assert_by
 	  (Name principle_id)
 	  princ_type
-	  (h_exact f_principle));
+	  (exact_check f_principle));
 	tclTHEN_i
 	  (observe_tac "functional_induction" (
 	     fun g ->
@@ -715,7 +714,7 @@ let generalize_dependent_of x hyp g =
   tclMAP
     (function
        | (id,None,t) when not (Id.equal id hyp) &&
-	   (Termops.occur_var (pf_env g) x t) -> tclTHEN (h_generalize [mkVar id]) (thin [id])
+	   (Termops.occur_var (pf_env g) x t) -> tclTHEN (Tactics.Simple.generalize [mkVar id]) (thin [id])
        | _ -> tclIDTAC
     )
     (pf_hyps g)
@@ -741,7 +740,7 @@ and intros_with_rewrite_aux : tactic =
  		      if Reductionops.is_conv (pf_env g) (project g) args.(1) args.(2)
 		      then
 			let id = pf_get_new_id (Id.of_string "y") g  in
-			tclTHENSEQ [ Proofview.V82.of_tactic (h_intro id); thin [id]; intros_with_rewrite ] g
+			tclTHENSEQ [ Proofview.V82.of_tactic (Simple.intro id); thin [id]; intros_with_rewrite ] g
 		      else if isVar args.(1) && (Environ.evaluable_named (destVar args.(1)) (pf_env g)) 
 		      then tclTHENSEQ[
 			unfold_in_concl [(Locus.AllOccurrences, Names.EvalVarRef (destVar args.(1)))];
@@ -759,7 +758,7 @@ and intros_with_rewrite_aux : tactic =
 		      else if isVar args.(1)
 		      then
 			let id = pf_get_new_id (Id.of_string "y") g  in
-			tclTHENSEQ [ Proofview.V82.of_tactic (h_intro id);
+			tclTHENSEQ [ Proofview.V82.of_tactic (Simple.intro id);
 				     generalize_dependent_of (destVar args.(1)) id;
 				     tclTRY (Proofview.V82.of_tactic (Equality.rewriteLR (mkVar id)));
 				     intros_with_rewrite
@@ -768,7 +767,7 @@ and intros_with_rewrite_aux : tactic =
 		      else if isVar args.(2) 
 		      then 
 			let id = pf_get_new_id (Id.of_string "y") g  in
-			tclTHENSEQ [ Proofview.V82.of_tactic (h_intro id);
+			tclTHENSEQ [ Proofview.V82.of_tactic (Simple.intro id);
 				     generalize_dependent_of (destVar args.(2)) id;
 				     tclTRY (Proofview.V82.of_tactic (Equality.rewriteRL (mkVar id)));
 				     intros_with_rewrite
@@ -778,7 +777,7 @@ and intros_with_rewrite_aux : tactic =
 			begin
 			  let id = pf_get_new_id (Id.of_string "y") g  in
 			  tclTHENSEQ[
-			    Proofview.V82.of_tactic (h_intro id);
+			    Proofview.V82.of_tactic (Simple.intro id);
 			    tclTRY (Proofview.V82.of_tactic (Equality.rewriteLR (mkVar id)));
 			    intros_with_rewrite
 			  ] g
@@ -787,12 +786,12 @@ and intros_with_rewrite_aux : tactic =
 		      Proofview.V82.of_tactic Tauto.tauto g
 		  | Case(_,_,v,_) ->
 		      tclTHENSEQ[
-			Proofview.V82.of_tactic (h_case false (v,NoBindings));
+			Proofview.V82.of_tactic (general_case_analysis false (v,NoBindings));
 			intros_with_rewrite
 		      ] g
 		  | LetIn _ ->
 		      tclTHENSEQ[
-			h_reduce
+			reduce
 			  (Genredexpr.Cbv
 			     {Redops.all_flags
 			      with Genredexpr.rDelta = false;
@@ -803,11 +802,11 @@ and intros_with_rewrite_aux : tactic =
 		      ] g
 		  | _ ->
 		      let id = pf_get_new_id (Id.of_string "y") g  in
-		      tclTHENSEQ [ Proofview.V82.of_tactic (h_intro id);intros_with_rewrite] g
+		      tclTHENSEQ [ Proofview.V82.of_tactic (Simple.intro id);intros_with_rewrite] g
 	      end
 	  | LetIn _ ->
 	      tclTHENSEQ[
-		h_reduce
+		reduce
 		  (Genredexpr.Cbv
 		     {Redops.all_flags
 		      with Genredexpr.rDelta = false;
@@ -824,7 +823,7 @@ let rec reflexivity_with_destruct_cases g =
       match kind_of_term (snd (destApp (pf_concl g))).(2) with
 	| Case(_,_,v,_) ->
 	    tclTHENSEQ[
-	      Proofview.V82.of_tactic (h_case false (v,NoBindings));
+	      Proofview.V82.of_tactic (general_case_analysis false (v,NoBindings));
 	      Proofview.V82.of_tactic intros;
 	      observe_tac "reflexivity_with_destruct_cases" reflexivity_with_destruct_cases
 	    ]
@@ -948,18 +947,18 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
 	  with Option.IsNone -> anomaly (Pp.str "Cannot find equation lemma")
 	in
 	tclTHENSEQ[
-	  tclMAP (fun id -> Proofview.V82.of_tactic (h_intro id)) ids;
+	  tclMAP (fun id -> Proofview.V82.of_tactic (Simple.intro id)) ids;
 	  Proofview.V82.of_tactic (Equality.rewriteLR (mkConst eq_lemma));
 	  (* Don't forget to $\zeta$ normlize the term since the principles
              have been $\zeta$-normalized *)
-	  h_reduce
+	  reduce
 	    (Genredexpr.Cbv
 	       {Redops.all_flags
 		with Genredexpr.rDelta = false;
 	       })
 	    Locusops.onConcl
 	  ;
-	  h_generalize (List.map mkVar ids);
+	  Simple.generalize (List.map mkVar ids);
 	  thin ids
 	]
       else
@@ -996,10 +995,10 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
     let params_names = fst (List.chop princ_infos.nparams args_names) in
     let params = List.map mkVar params_names in
     tclTHENSEQ
-      [ tclMAP (fun id -> Proofview.V82.of_tactic (h_intro id)) (args_names@[res;hres]);
+      [ tclMAP (fun id -> Proofview.V82.of_tactic (Simple.intro id)) (args_names@[res;hres]);
 	observe_tac "h_generalize"
-	(h_generalize [mkApp(applist(graph_principle,params),Array.map (fun c -> applist(c,params)) lemmas)]);
-	Proofview.V82.of_tactic (h_intro graph_principle_id);
+	(Simple.generalize [mkApp(applist(graph_principle,params),Array.map (fun c -> applist(c,params)) lemmas)]);
+	Proofview.V82.of_tactic (Simple.intro graph_principle_id);
 	observe_tac "" (tclTHEN_i
 	  (observe_tac "elim" (Proofview.V82.of_tactic ((elim false (mkVar hres,NoBindings) (Some (mkVar graph_principle_id,NoBindings))))))
 	  (fun i g -> observe_tac "prove_branche" (prove_branche i) g ))
@@ -1160,9 +1159,9 @@ let revert_graph kn post_tac hid g =
 		  let f_args,res = Array.chop (Array.length args - 1) args in
 		  tclTHENSEQ
 		    [
-		      h_generalize [applist(mkConst f_complete,(Array.to_list f_args)@[res.(0);mkVar hid])];
+		      Simple.generalize [applist(mkConst f_complete,(Array.to_list f_args)@[res.(0);mkVar hid])];
 		      thin [hid];
-		      Proofview.V82.of_tactic (h_intro hid);
+		      Proofview.V82.of_tactic (Simple.intro hid);
 		      post_tac hid
 		    ]
 		    g
@@ -1197,16 +1196,16 @@ let functional_inversion kn hid fconst f_correct : tactic =
 	  let pre_tac,f_args,res =
 	    match kind_of_term args.(1),kind_of_term args.(2) with
 	      | App(f,f_args),_ when eq_constr f fconst ->
-		  ((fun hid -> Proofview.V82.of_tactic (h_symmetry (Locusops.onHyp hid))),f_args,args.(2))
+		  ((fun hid -> Proofview.V82.of_tactic (intros_symmetry (Locusops.onHyp hid))),f_args,args.(2))
 	      |_,App(f,f_args) when eq_constr f fconst ->
 		 ((fun hid -> tclIDTAC),f_args,args.(1))
 	      | _ -> (fun hid -> tclFAIL 1 (mt ())),[||],args.(2)
 	  in
 	  tclTHENSEQ[
 	    pre_tac hid;
-	    h_generalize [applist(f_correct,(Array.to_list f_args)@[res;mkVar hid])];
+	    Simple.generalize [applist(f_correct,(Array.to_list f_args)@[res;mkVar hid])];
 	    thin [hid];
-	    Proofview.V82.of_tactic (h_intro hid);
+	    Proofview.V82.of_tactic (Simple.intro hid);
 	    Proofview.V82.of_tactic (Inv.inv FullInversion None (NamedHyp hid));
 	    (fun g ->
 	       let new_ids = List.filter (fun id -> not (Id.Set.mem id old_ids)) (pf_ids_of_hyps g) in
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 68ac62838..6afbff779 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -33,7 +33,6 @@ open Pfedit
 open Glob_term
 open Pretyping
 open Constrintern
-open Hiddentac
 open Misctypes
 open Genredexpr
 
@@ -257,8 +256,8 @@ let observe_tac s tac g =
 let tclUSER tac is_mes l g =
   let clear_tac =
     match l with
-      | None -> h_clear false []
-      | Some l -> tclMAP (fun id -> tclTRY (h_clear false [id])) (List.rev l)
+      | None -> clear []
+      | Some l -> tclMAP (fun id -> tclTRY (clear [id])) (List.rev l)
   in
   tclTHENSEQ
     [
@@ -276,8 +275,8 @@ let tclUSER tac is_mes l g =
 
 let tclUSER_if_not_mes concl_tac is_mes names_to_suppress =
   if is_mes
-  then tclCOMPLETE (h_simplest_apply (delayed_force well_founded_ltof))
-  else tclTHEN (h_simplest_apply (delayed_force acc_intro_generator_function) ) (tclUSER concl_tac is_mes names_to_suppress)
+  then tclCOMPLETE (Simple.apply (delayed_force well_founded_ltof))
+  else tclTHEN (Simple.apply (delayed_force acc_intro_generator_function) ) (tclUSER concl_tac is_mes names_to_suppress)
 
 
 
@@ -518,7 +517,7 @@ let rec prove_lt hyple g =
 	(
 	  tclTHENLIST[
 	    apply (delayed_force lt_S_n);
-	    (observe_tac (str "assumption: " ++ Printer.pr_goal g) (Proofview.V82.of_tactic h_assumption))
+	    (observe_tac (str "assumption: " ++ Printer.pr_goal g) (Proofview.V82.of_tactic assumption))
 	  ])
       )
   end
@@ -566,7 +565,7 @@ let rec destruct_bounds_aux infos (bound,hyple,rechyps) lbounds g =
 			 
 			 (observe_tac (str "finishing") 
 			    (tclORELSE
-			       (Proofview.V82.of_tactic h_reflexivity)
+			       (Proofview.V82.of_tactic intros_reflexivity)
 			       (observe_tac (str "calling prove_lt") (prove_lt hyple))))])
 		   ]
 	      ]
@@ -575,7 +574,7 @@ let rec destruct_bounds_aux infos (bound,hyple,rechyps) lbounds g =
       | (_,v_bound)::l -> 
       tclTHENLIST[
 	Proofview.V82.of_tactic (simplest_elim (mkVar v_bound));
-	h_clear false [v_bound];
+	clear [v_bound];
 	tclDO 2 (Proofview.V82.of_tactic intro);
 	onNthHypId 1 
 	  (fun p_hyp -> 
@@ -663,7 +662,7 @@ let mkDestructEq :
   let new_hyps = mkApp(Lazy.force refl_equal, [|type_of_expr; expr|])::
            to_revert_constr in
     tclTHENLIST
-     [h_generalize new_hyps;
+     [Simple.generalize new_hyps;
       (fun g2 ->
 	change_in_concl None
 	  (pattern_occs [Locus.AllOccurrencesBut [1], expr] (pf_env g2) Evd.empty (pf_concl g2)) g2);
@@ -758,7 +757,7 @@ let terminate_app_rec (f,args) expr_info continuation_tac _ =
 	    tclTHENS (* proof of args < formal args *)
 	      (apply (Lazy.force expr_info.acc_inv))
 	      [ 
-		observe_tac (str "h_assumption") (Proofview.V82.of_tactic h_assumption);
+		observe_tac (str "assumption") (Proofview.V82.of_tactic assumption);
 		tclTHENLIST
 		  [
 		    tclTRY(list_rewrite true 
@@ -803,7 +802,7 @@ let rec prove_le g =
     (List.hd args,List.hd (List.tl args))
   in 
   tclFIRST[
-    Proofview.V82.of_tactic h_assumption;
+    Proofview.V82.of_tactic assumption;
     apply (delayed_force le_n);
     begin
       try
@@ -881,7 +880,7 @@ let make_rewrite expr_info l hp max =
 	   
 	   (list_rewrite true 
 	      (List.map (fun e -> mkVar e,true) expr_info.eqs));
-	   (observe_tac (str "h_reflexivity") (Proofview.V82.of_tactic h_reflexivity))]))
+	   (observe_tac (str "h_reflexivity") (Proofview.V82.of_tactic intros_reflexivity))]))
        ;
 	 tclTHENLIST[ (* x < S (S max) proof *)
 	 apply (delayed_force le_lt_SS);
@@ -1074,7 +1073,7 @@ let termination_proof_header is_mes input_type ids args_id relation
 		 (* this gives the accessibility argument *)
 		 observe_tac
 		   (str "apply wf_thm")
-		   (h_simplest_apply (mkApp(mkVar wf_thm,[|mkVar rec_arg_id|]))
+		   (Simple.apply (mkApp(mkVar wf_thm,[|mkVar rec_arg_id|]))
 		   )
 	       ]
 	     ;
@@ -1083,12 +1082,12 @@ let termination_proof_header is_mes input_type ids args_id relation
 	       [observe_tac (str "generalize")
 		  (onNLastHypsId (nargs+1)
 		     (tclMAP (fun id ->
-			tclTHEN (h_generalize [mkVar id]) (h_clear false [id]))
+			tclTHEN (Tactics.Simple.generalize [mkVar id]) (clear [id]))
 		     ))
 	       ;
-		observe_tac (str "h_fix") (h_fix (Some hrec) (nargs+1));
+		observe_tac (str "fix") (fix (Some hrec) (nargs+1));
 		h_intros args_id;
-		Proofview.V82.of_tactic (h_intro wf_rec_arg);
+		Proofview.V82.of_tactic (Simple.intro wf_rec_arg);
 		observe_tac (str "tac") (tac wf_rec_arg hrec wf_rec_arg acc_inv)
 	       ]
 	   ]
@@ -1272,8 +1271,8 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_
 	   let hid = next_ident_away_in_goal h_id (pf_ids_of_hyps gls) in
 	   tclTHENSEQ
 	     [
-	       h_generalize [lemma];
-	       Proofview.V82.of_tactic (h_intro hid);
+	       Simple.generalize [lemma];
+	       Proofview.V82.of_tactic (Simple.intro hid);
 	       (fun g ->
 		  let ids = pf_ids_of_hyps g in
 		  tclTHEN
@@ -1333,7 +1332,7 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_
 	 	     (fun c ->
 	 		tclTHENSEQ
 	 		  [Proofview.V82.of_tactic intros;
-	 		   h_simplest_apply (interp_constr Evd.empty (Global.env()) c);
+	 		   Simple.apply (interp_constr Evd.empty (Global.env()) c);
 	 		   tclCOMPLETE (Proofview.V82.of_tactic Auto.default_auto)
 	 		  ]
 	 	     )
diff --git a/tactics/auto.ml b/tactics/auto.ml
index e87158bdd..9156e1f04 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -29,7 +29,6 @@ open Tacred
 open Tactics
 open Tacticals
 open Clenv
-open Hiddentac
 open Libnames
 open Globnames
 open Nametab
@@ -1345,7 +1344,7 @@ and tac_of_hint dbg db_list local_db concl (flags, ({pat=p; code=t})) =
     | Unfold_nth c ->
       Proofview.V82.tactic (fun gl ->
        if exists_evaluable_reference (pf_env gl) c then
-	 tclPROGRESS (h_reduce (Unfold [AllOccurrences,c]) Locusops.onConcl) gl
+	 tclPROGRESS (reduce (Unfold [AllOccurrences,c]) Locusops.onConcl) gl
        else tclFAIL 0 (str"Unbound reference") gl)
     | Extern tacast -> conclPattern concl p tacast
   in
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index 369107f6c..256f84ba4 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -23,7 +23,6 @@ open Patternops
 open Clenv
 open Auto
 open Genredexpr
-open Hiddentac
 open Tacexpr
 open Misctypes
 open Locus
@@ -59,8 +58,8 @@ let registered_e_assumption gl =
 
 let one_step l gl =
   [Proofview.V82.of_tactic Tactics.intro]
-  @ (List.map h_simplest_eapply (List.map mkVar (pf_ids_of_hyps gl)))
-  @ (List.map h_simplest_eapply l)
+  @ (List.map Tactics.Simple.eapply (List.map mkVar (pf_ids_of_hyps gl)))
+  @ (List.map Tactics.Simple.eapply l)
   @ (List.map assumption (pf_ids_of_hyps gl))
 
 let rec prolog l n gl =
@@ -95,7 +94,7 @@ let priority l = List.map snd (List.filter (fun (pr,_) -> Int.equal pr 0) l)
 let unify_e_resolve flags (c,clenv) gls =
   let clenv' = connect_clenv gls clenv in
   let _ = clenv_unique_resolver ~flags clenv' gls in
-  h_simplest_eapply c gls
+  Tactics.Simple.eapply c gls
 
 let rec e_trivial_fail_db db_list local_db goal =
   let tacl =
@@ -133,7 +132,7 @@ and e_my_find_search db_list local_db hdc concl =
 	   | Res_pf_THEN_trivial_fail (term,cl) ->
                tclTHEN (unify_e_resolve st (term,cl))
 		 (e_trivial_fail_db db_list local_db)
-	   | Unfold_nth c -> h_reduce (Unfold [AllOccurrences,c]) onConcl
+	   | Unfold_nth c -> reduce (Unfold [AllOccurrences,c]) onConcl
 	   | Extern tacast -> Proofview.V82.of_tactic (conclPattern concl p tacast)
        in
        (tac,lazy (pr_autotactic t)))
diff --git a/tactics/eqdecide.ml4 b/tactics/eqdecide.ml4
index 1389e1de2..cb518a03a 100644
--- a/tactics/eqdecide.ml4
+++ b/tactics/eqdecide.ml4
@@ -22,7 +22,6 @@ open Term
 open Declarations
 open Tactics
 open Tacticals
-open Hiddentac
 open Auto
 open Matching
 open Hipattern
@@ -54,16 +53,22 @@ open Coqlib
 let clear_last = (onLastHyp (fun c -> (clear [destVar c])))
 
 let choose_eq eqonleft =
-  if eqonleft then h_simplest_left else h_simplest_right
+  if eqonleft then
+    left_with_bindings false Misctypes.NoBindings
+  else
+    right_with_bindings false Misctypes.NoBindings
 let choose_noteq eqonleft =
-  if eqonleft then h_simplest_right else h_simplest_left
+  if eqonleft then
+    right_with_bindings false Misctypes.NoBindings
+  else
+    left_with_bindings false Misctypes.NoBindings
 
 let mkBranches c1 c2 =
   Tacticals.New.tclTHENLIST
     [Proofview.V82.tactic (generalize [c2]);
-     h_simplest_elim c1;
+     Simple.elim c1;
      intros;
-     Tacticals.New.onLastHyp h_simplest_case;
+     Tacticals.New.onLastHyp Simple.case;
      Proofview.V82.tactic clear_last;
      intros]
 
@@ -105,7 +110,7 @@ let diseqCase eqonleft =
   (Tacticals.New.tclTHEN (choose_noteq eqonleft)
   (Tacticals.New.tclTHEN  (Proofview.V82.tactic red_in_concl)
   (Tacticals.New.tclTHEN  (intro_using absurd)
-  (Tacticals.New.tclTHEN  (Proofview.V82.tactic (h_simplest_apply (mkVar diseq)))
+  (Tacticals.New.tclTHEN  (Proofview.V82.tactic (Simple.apply (mkVar diseq)))
   (Tacticals.New.tclTHEN  (Extratactics.injHyp absurd)
             (full_trivial [])))))))
 
@@ -128,7 +133,7 @@ let solveArg eqonleft op a1 a2 tac =
   let subtacs =
     if eqonleft then [eqCase tac;diseqCase eqonleft;default_auto]
     else [diseqCase eqonleft;eqCase tac;default_auto] in
-  (Tacticals.New.tclTHENS (Proofview.V82.tactic (h_elim_type decide)) subtacs)
+  (Tacticals.New.tclTHENS (Proofview.V82.tactic (elim_type decide)) subtacs)
   end
 
 let solveEqBranch rectype =
@@ -144,7 +149,7 @@ let solveEqBranch rectype =
           and largs   = getargs lhs in
           List.fold_right2
             (solveArg eqonleft op) largs rargs
-            (Tacticals.New.tclTHEN (choose_eq eqonleft) h_reflexivity)
+            (Tacticals.New.tclTHEN (choose_eq eqonleft) intros_reflexivity)
       end
     end
     begin function
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 094cb6b19..1c7b8d49f 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -669,7 +669,7 @@ let  mkCaseEq a  : unit Proofview.tactic =
   Proofview.Goal.enter begin fun gl ->
     let type_of_a = Tacmach.New.of_old (fun g -> Tacmach.pf_type_of g a) gl in
        Tacticals.New.tclTHENLIST
-         [Proofview.V82.tactic (Hiddentac.h_generalize [mkApp(delayed_force refl_equal, [| type_of_a; a|])]);
+         [Proofview.V82.tactic (Tactics.Simple.generalize [mkApp(delayed_force refl_equal, [| type_of_a; a|])]);
           Proofview.Goal.enter begin fun gl ->
             let concl = Proofview.Goal.concl gl in
             let env = Proofview.Goal.env gl in
diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml
deleted file mode 100644
index e61922d07..000000000
--- a/tactics/hiddentac.ml
+++ /dev/null
@@ -1,96 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-open Tactics
-open Util
-open Locus
-open Misctypes
-
-(* Basic tactics *)
-let h_intro_move = intro_move
-let h_intro x = h_intro_move (Some x) MoveLast
-let h_intros_until = intros_until
-let h_assumption = assumption
-let h_exact = exact_check
-let h_exact_no_check = exact_no_check
-let h_vm_cast_no_check = vm_cast_no_check
-let h_apply = apply_with_bindings_gen
-let h_apply_in simple ev cb (id,ipat) = apply_in simple ev id cb ipat
-let h_elim = elim
-let h_elim_type = elim_type
-let h_case = general_case_analysis
-let h_case_type = case_type
-let h_fix = fix
-let h_mutual_fix id n l = mutual_fix id n l 0
-
-let h_cofix = cofix
-let h_mutual_cofix id l = mutual_cofix id l 0
-
-let h_cut = cut
-let h_generalize_gen cl =
-  generalize_gen (List.map (on_fst Redexpr.out_with_occurrences) cl)
-let h_generalize cl =
-  h_generalize_gen (List.map (fun c -> ((AllOccurrences,c),Names.Anonymous))
-    cl)
-let h_generalize_dep = generalize_dep
-let h_let_tac b na c cl eqpat =
-  let id = Option.default (Loc.ghost,IntroAnonymous) eqpat in
-  let with_eq = if b then None else Some (true,id) in
-  letin_tac with_eq na c None cl
-let h_let_pat_tac b na c cl eqpat =
-  let id = Option.default (Loc.ghost,IntroAnonymous) eqpat in
-  let with_eq = if b then None else Some (true,id) in
-  letin_pat_tac with_eq na c None cl
-
-(* Derived basic tactics *)
-let h_simple_induction_destruct isrec h =
-  if isrec then (simple_induct h) else (simple_destruct h)
-let h_simple_induction = h_simple_induction_destruct true
-let h_simple_destruct = h_simple_induction_destruct false
-
-let h_induction_destruct = induction_destruct
-let h_new_induction ev c idl e cl =
-  h_induction_destruct true ev ([c,idl],e,cl)
-let h_new_destruct ev c idl e cl = h_induction_destruct false ev ([c,idl],e,cl)
-
-let h_specialize = specialize
-let h_lapply = cut_and_apply
-
-(* Context management *)
-let h_clear b l = (if b then keep else clear) l
-let h_clear_body = clear_body
-let h_move = move_hyp
-let h_rename = rename_hyp
-let h_revert = revert
-
-(* Constructors *)
-let h_left = left_with_bindings
-let h_right = right_with_bindings
-let h_split = split_with_bindings
-
-let h_constructor ev n l = constructor_tac ev None n l
-let h_one_constructor n = one_constructor n NoBindings
-let h_simplest_left   = h_left false NoBindings
-let h_simplest_right  = h_right false NoBindings
-
-(* Conversion *)
-let h_reduce = reduce
-let h_change = change
-
-(* Equivalence relations *)
-let h_reflexivity = intros_reflexivity
-let h_symmetry = intros_symmetry
-let h_transitivity = intros_transitivity
-
-let h_simplest_apply c = h_apply false false [Loc.ghost,(c,NoBindings)]
-let h_simplest_eapply c = h_apply false true [Loc.ghost,(c,NoBindings)]
-let h_simplest_elim c   = h_elim false (c,NoBindings) None
-let h_simplest_case   c = h_case false (c,NoBindings)
-
-let h_intro_patterns = intro_patterns
-
diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli
deleted file mode 100644
index ad7654374..000000000
--- a/tactics/hiddentac.mli
+++ /dev/null
@@ -1,125 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-open Loc
-open Names
-open Pp
-open Term
-open Proof_type
-open Tacmach
-open Genarg
-open Tacexpr
-open Glob_term
-open Evd
-open Clenv
-open Termops
-open Misctypes
-
-(** Tactics for the interpreter. They used to left a trace in the proof tree
-   when they are called. *)
-
-(** Basic tactics *)
-
-val h_intro_move      : Id.t option -> Id.t move_location -> unit Proofview.tactic
-val h_intro           : Id.t -> unit Proofview.tactic
-val h_intros_until    : quantified_hypothesis -> unit Proofview.tactic
-
-val h_assumption      : unit Proofview.tactic
-val h_exact           : constr -> tactic
-val h_exact_no_check  : constr -> tactic
-val h_vm_cast_no_check  : constr -> tactic
-
-val h_apply           : advanced_flag -> evars_flag ->
-  constr with_bindings located list -> tactic
-val h_apply_in        : advanced_flag -> evars_flag ->
-  constr with_bindings located list ->
-  Id.t * intro_pattern_expr located option -> unit Proofview.tactic
-
-val h_elim            : evars_flag -> constr with_bindings ->
-                        constr with_bindings option -> unit Proofview.tactic
-val h_elim_type       : constr -> tactic
-val h_case            : evars_flag -> constr with_bindings -> unit Proofview.tactic
-val h_case_type       : constr -> tactic
-
-val h_mutual_fix      : Id.t -> int ->
-                        (Id.t * int * constr) list -> tactic
-val h_fix             : Id.t option -> int -> tactic
-val h_mutual_cofix    : Id.t -> (Id.t * constr) list -> tactic
-val h_cofix           : Id.t option -> tactic
-
-val h_cut             : constr -> tactic
-val h_generalize      : constr list -> tactic
-val h_generalize_gen  : (constr Locus.with_occurrences * Name.t) list -> tactic
-val h_generalize_dep  : ?with_let:bool -> constr -> tactic
-val h_let_tac         : letin_flag -> Name.t -> constr -> Locus.clause ->
-                        intro_pattern_expr located option -> unit Proofview.tactic
-val h_let_pat_tac     : letin_flag -> Name.t -> evar_map * constr ->
-                        Locus.clause -> intro_pattern_expr located option ->
-                        unit Proofview.tactic
-
-(** Derived basic tactics *)
-
-val h_simple_induction   : quantified_hypothesis -> unit Proofview.tactic
-val h_simple_destruct    : quantified_hypothesis -> unit Proofview.tactic
-val h_simple_induction_destruct : rec_flag -> quantified_hypothesis -> unit Proofview.tactic
-val h_new_induction   : evars_flag ->
-  (evar_map * constr with_bindings) induction_arg ->
-  intro_pattern_expr located option * intro_pattern_expr located option ->
-  constr with_bindings option ->
-  Locus.clause option -> unit Proofview.tactic
-val h_new_destruct    : evars_flag ->
-  (evar_map * constr with_bindings) induction_arg ->
-  intro_pattern_expr located option * intro_pattern_expr located option ->
-  constr with_bindings option ->
-  Locus.clause option -> unit Proofview.tactic
-val h_induction_destruct : rec_flag -> evars_flag ->
-  ((evar_map * constr with_bindings) induction_arg *
-   (intro_pattern_expr located option * intro_pattern_expr located option)) list
-    * constr with_bindings option
-    * Locus.clause option -> unit Proofview.tactic
-
-val h_specialize      : int option -> constr with_bindings -> tactic
-val h_lapply          : constr -> tactic
-
-(** Automation tactic : see Auto *)
-
-
-(** Context management *)
-val h_clear           : bool -> Id.t list -> tactic
-val h_clear_body      : Id.t list -> tactic
-val h_move            : bool -> Id.t -> Id.t move_location -> tactic
-val h_rename          : (Id.t*Id.t) list -> tactic
-val h_revert          : Id.t list -> tactic
-
-(** Constructors *)
-val h_constructor     : evars_flag -> int -> constr bindings -> unit Proofview.tactic
-val h_left            : evars_flag -> constr bindings -> unit Proofview.tactic
-val h_right           : evars_flag -> constr bindings -> unit Proofview.tactic
-val h_split           : evars_flag -> constr bindings list -> unit Proofview.tactic
-
-val h_one_constructor : int -> unit Proofview.tactic
-val h_simplest_left   : unit Proofview.tactic
-val h_simplest_right  : unit Proofview.tactic
-
-
-(** Conversion *)
-val h_reduce          : Redexpr.red_expr -> Locus.clause -> tactic
-val h_change          :
-  Pattern.constr_pattern option -> constr -> Locus.clause -> tactic
-
-(** Equivalence relations *)
-val h_reflexivity     : unit Proofview.tactic
-val h_symmetry        : Locus.clause -> unit Proofview.tactic
-val h_transitivity    : constr option -> unit Proofview.tactic
-
-val h_simplest_apply  : constr -> tactic
-val h_simplest_eapply : constr -> tactic
-val h_simplest_elim   : constr -> unit Proofview.tactic
-val h_simplest_case   : constr -> unit Proofview.tactic
-
-val h_intro_patterns  : intro_pattern_expr located list -> unit Proofview.tactic
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 083426531..4e20c2fa9 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -31,7 +31,6 @@ open Constrexpr
 open Term
 open Termops
 open Tacexpr
-open Hiddentac
 open Genarg
 open Stdarg
 open Constrarg
@@ -1445,26 +1444,26 @@ and interp_atomic ist tac =
       Proofview.Goal.enter begin fun gl ->
         let env = Proofview.Goal.env gl in
         let patterns = interp_intro_pattern_list_as_list ist env l in
-        h_intro_patterns patterns
+        Tactics.intro_patterns patterns
       end
   | TacIntrosUntil hyp ->
       begin try (* interp_quantified_hypothesis can raise an exception *)
-        h_intros_until (interp_quantified_hypothesis ist hyp)
+        Tactics.intros_until (interp_quantified_hypothesis ist hyp)
       with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
       end
   | TacIntroMove (ido,hto) ->
       Proofview.Goal.enter begin fun gl ->
         let env = Proofview.Goal.env gl in
         let mloc = interp_move_location ist env hto in
-        h_intro_move (Option.map (interp_fresh_ident ist env) ido) mloc
+        Tactics.intro_move (Option.map (interp_fresh_ident ist env) ido) mloc
       end
-  | TacAssumption -> h_assumption
+  | TacAssumption -> Tactics.assumption
   | TacExact c ->
       Proofview.V82.tactic begin fun gl -> 
         let (sigma,c_interp) = pf_interp_casted_constr ist gl c in
         tclTHEN
 	  (tclEVARS sigma)
-	  (h_exact c_interp)
+	  (Tactics.exact_check c_interp)
           gl
       end
   | TacExactNoCheck c ->
@@ -1472,7 +1471,7 @@ and interp_atomic ist tac =
         let (sigma,c_interp) = pf_interp_constr ist gl c in
         tclTHEN
 	  (tclEVARS sigma)
-	  (h_exact_no_check c_interp)
+	  (Tactics.exact_no_check c_interp)
           gl
       end
   | TacVmCastNoCheck c ->
@@ -1480,7 +1479,7 @@ and interp_atomic ist tac =
         let (sigma,c_interp) = pf_interp_constr ist gl c in
         tclTHEN
 	  (tclEVARS sigma)
-	  (h_vm_cast_no_check c_interp)
+	  (Tactics.vm_cast_no_check c_interp)
           gl
       end
   | TacApply (a,ev,cb,cl) ->
@@ -1492,13 +1491,13 @@ and interp_atomic ist tac =
             List.fold_map (interp_open_constr_with_bindings_loc ist env) sigma cb
           in
           let tac = match cl with
-            | None -> fun l -> Proofview.V82.tactic (h_apply a ev l)
+            | None -> fun l -> Proofview.V82.tactic (Tactics.apply_with_bindings_gen a ev l)
             | Some cl ->
                 (fun l ->
                   Proofview.Goal.enter begin fun gl ->
                     let env = Proofview.Goal.env gl in
-                    let cl = interp_in_hyp_as ist env cl in
-                    h_apply_in a ev l cl
+                    let (id,cl) = interp_in_hyp_as ist env cl in
+                    Tactics.apply_in a ev id l cl
                   end) in
           Tacticals.New.tclWITHHOLES ev tac sigma l
         with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
@@ -1510,7 +1509,7 @@ and interp_atomic ist tac =
         try (* interpretation functions may raise exceptions *)
           let sigma, cb = interp_constr_with_bindings ist env sigma cb in
           let sigma, cbo = Option.fold_map (interp_constr_with_bindings ist env) sigma cbo in
-          Tacticals.New.tclWITHHOLES ev (h_elim ev cb) sigma cbo
+          Tacticals.New.tclWITHHOLES ev (Tactics.elim ev cb) sigma cbo
         with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
       end
   | TacElimType c ->
@@ -1518,7 +1517,7 @@ and interp_atomic ist tac =
         let (sigma,c_interp) = pf_interp_type ist gl c in
         tclTHEN
 	  (tclEVARS sigma)
-	  (h_elim_type c_interp)
+	  (Tactics.elim_type c_interp)
           gl
       end
   | TacCase (ev,cb) ->
@@ -1526,20 +1525,20 @@ and interp_atomic ist tac =
         let sigma = Proofview.Goal.sigma gl in
         let env = Proofview.Goal.env gl in
         let sigma, cb = interp_constr_with_bindings ist env sigma cb in
-        Tacticals.New.tclWITHHOLES ev (h_case ev) sigma cb
+        Tacticals.New.tclWITHHOLES ev (Tactics.general_case_analysis ev) sigma cb
       end
   | TacCaseType c ->
       Proofview.V82.tactic begin fun gl -> 
         let (sigma,c_interp) = pf_interp_type ist gl c in
         tclTHEN
 	  (tclEVARS sigma)
-	  (h_case_type c_interp)
+	  (Tactics.case_type c_interp)
           gl
       end
   | TacFix (idopt,n) ->
       Proofview.Goal.enter begin fun gl ->
         let env = Proofview.Goal.env gl in
-        Proofview.V82.tactic (h_fix (Option.map (interp_fresh_ident ist env) idopt) n)
+        Proofview.V82.tactic (Tactics.fix (Option.map (interp_fresh_ident ist env) idopt) n)
       end
   | TacMutualFix (id,n,l) ->
       Proofview.V82.tactic begin fun gl ->
@@ -1555,13 +1554,13 @@ and interp_atomic ist tac =
         in
         tclTHEN
 	  (tclEVARS sigma)
-	  (h_mutual_fix (interp_fresh_ident ist env id) n l_interp)
+	  (Tactics.mutual_fix (interp_fresh_ident ist env id) n l_interp 0)
           gl
       end
   | TacCofix idopt ->
       Proofview.Goal.enter begin fun gl ->
         let env = Proofview.Goal.env gl in
-        Proofview.V82.tactic (h_cofix (Option.map (interp_fresh_ident ist env) idopt))
+        Proofview.V82.tactic (Tactics.cofix (Option.map (interp_fresh_ident ist env) idopt))
       end
   | TacMutualCofix (id,l) ->
       Proofview.V82.tactic begin fun gl ->
@@ -1577,7 +1576,7 @@ and interp_atomic ist tac =
         in
         tclTHEN
 	  (tclEVARS sigma)
-	  (h_mutual_cofix (interp_fresh_ident ist env id) l_interp)
+	  (Tactics.mutual_cofix (interp_fresh_ident ist env id) l_interp 0)
           gl
       end
   | TacCut c ->
@@ -1585,7 +1584,7 @@ and interp_atomic ist tac =
         let (sigma,c_interp) = pf_interp_type ist gl c in
         tclTHEN
 	  (tclEVARS sigma)
-	  (h_cut c_interp)
+	  (Tactics.cut c_interp)
           gl
       end
   | TacAssert (t,ipat,c) ->
@@ -1608,14 +1607,14 @@ and interp_atomic ist tac =
         let sigma = project gl in
         let env = pf_env gl in
         let sigma, cl = interp_constr_with_occurrences_and_name_as_list ist env sigma cl in
-        tclWITHHOLES false (h_generalize_gen) sigma cl gl
+        tclWITHHOLES false (Tactics.Simple.generalize_gen) sigma cl gl
       end
   | TacGeneralizeDep c ->
       Proofview.V82.tactic begin fun gl -> 
         let (sigma,c_interp) = pf_interp_constr ist gl c in
         tclTHEN
 	  (tclEVARS sigma)
-	  (h_generalize_dep c_interp)
+	  (Tactics.generalize_dep c_interp)
           gl
       end
   | TacLetTac (na,c,clp,b,eqpat) ->
@@ -1630,13 +1629,23 @@ and interp_atomic ist tac =
           let (sigma,c_interp) =
             Tacmach.New.of_old (fun gl -> pf_interp_constr ist gl c) gl
           in
-	Tacticals.New.tclTHEN
-	  (Proofview.V82.tclEVARS sigma)
-          (h_let_tac b (interp_fresh_name ist env na) c_interp clp eqpat)
+          let let_tac b na c cl eqpat =
+            let id = Option.default (Loc.ghost,IntroAnonymous) eqpat in
+            let with_eq = if b then None else Some (true,id) in
+            Tactics.letin_tac with_eq na c None cl
+          in
+	  Tacticals.New.tclTHEN
+	    (Proofview.V82.tclEVARS sigma)
+            (let_tac b (interp_fresh_name ist env na) c_interp clp eqpat)
         else
         (* We try to keep the pattern structure as much as possible *)
           begin try
-                  h_let_pat_tac b (interp_fresh_name ist env na)
+                  let let_pat_tac b na c cl eqpat =
+                    let id = Option.default (Loc.ghost,IntroAnonymous) eqpat in
+                    let with_eq = if b then None else Some (true,id) in
+                    Tactics.letin_pat_tac with_eq na c None cl
+                  in
+                  let_pat_tac b (interp_fresh_name ist env na)
                     (interp_pure_open_constr ist env sigma c) clp eqpat
             with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
           end
@@ -1662,7 +1671,8 @@ and interp_atomic ist tac =
 
   (* Derived basic tactics *)
   | TacSimpleInductionDestruct (isrec,h) ->
-      h_simple_induction_destruct isrec (interp_quantified_hypothesis ist h)
+      let h = interp_quantified_hypothesis ist h in
+      if isrec then Tactics.simple_induct h else Tactics.simple_destruct h
   | TacInductionDestruct (isrec,ev,(l,el,cls)) ->
       (* spiwack: some unknown part of destruct needs the goal to be
          prenormalised. *)
@@ -1683,7 +1693,7 @@ and interp_atomic ist tac =
           Option.fold_map (interp_constr_with_bindings ist env) sigma el in
         let interp_clause = interp_clause ist env in
         let cls = Option.map interp_clause cls in
-        Tacticals.New.tclWITHHOLES ev (h_induction_destruct isrec ev) sigma (l,el,cls)
+        Tacticals.New.tclWITHHOLES ev (Tactics.induction_destruct isrec ev) sigma (l,el,cls)
       end
   | TacDoubleInduction (h1,h2) ->
       let h1 = interp_quantified_hypothesis ist h1 in
@@ -1717,7 +1727,7 @@ and interp_atomic ist tac =
         let sigma = Proofview.Goal.sigma gl in
         Proofview.V82.tactic begin fun gl -> 
           let sigma, cb = interp_constr_with_bindings ist env sigma cb in
-          tclWITHHOLES false (h_specialize n) sigma cb gl
+          tclWITHHOLES false (Tactics.specialize n) sigma cb gl
         end
       end
   | TacLApply c ->
@@ -1725,36 +1735,37 @@ and interp_atomic ist tac =
         let (sigma,c_interp) = pf_interp_constr ist gl c in
         tclTHEN
 	  (tclEVARS sigma)
-	  (h_lapply c_interp)
+	  (Tactics.cut_and_apply c_interp)
           gl
       end
 
   (* Context management *)
   | TacClear (b,l) ->
       Proofview.V82.tactic begin fun gl ->
-        h_clear b (interp_hyp_list ist (pf_env gl) l) gl
+        let l = interp_hyp_list ist (pf_env gl) l in
+        if b then Tactics.keep l gl else Tactics.clear l gl
       end
   | TacClearBody l ->
       Proofview.V82.tactic begin fun gl ->
-        h_clear_body (interp_hyp_list ist (pf_env gl) l) gl
+        Tactics.clear_body (interp_hyp_list ist (pf_env gl) l) gl
       end
   | TacMove (dep,id1,id2) ->
       Proofview.V82.tactic begin fun gl -> 
-        h_move dep (interp_hyp ist (pf_env gl) id1)
+        Tactics.move_hyp dep (interp_hyp ist (pf_env gl) id1)
                    (interp_move_location ist (pf_env gl) id2)
                    gl
       end
   | TacRename l ->
       Proofview.V82.tactic begin fun gl ->
         let env = pf_env gl in
-        h_rename (List.map (fun (id1,id2) ->
+        Tactics.rename_hyp (List.map (fun (id1,id2) ->
 	  interp_hyp ist env id1,
 	  interp_fresh_ident ist env (snd id2)) l)
           gl
       end
   | TacRevert l ->
       Proofview.V82.tactic begin fun gl -> 
-        h_revert (interp_hyp_list ist (pf_env gl) l) gl
+        Tactics.revert (interp_hyp_list ist (pf_env gl) l) gl
       end
 
   (* Constructors *)
@@ -1763,21 +1774,21 @@ and interp_atomic ist tac =
         let env = Proofview.Goal.env gl in
         let sigma = Proofview.Goal.sigma gl in
         let sigma, bl = interp_bindings ist env sigma bl in
-        Tacticals.New.tclWITHHOLES ev (h_left ev) sigma bl
+        Tacticals.New.tclWITHHOLES ev (Tactics.left_with_bindings ev) sigma bl
       end
   | TacRight (ev,bl) ->
       Proofview.Goal.enter begin fun gl ->
         let env = Proofview.Goal.env gl in
         let sigma = Proofview.Goal.sigma gl in
         let sigma, bl = interp_bindings ist env sigma bl in
-        Tacticals.New.tclWITHHOLES ev (h_right ev) sigma bl
+        Tacticals.New.tclWITHHOLES ev (Tactics.right_with_bindings ev) sigma bl
       end
   | TacSplit (ev,_,bll) ->
       Proofview.Goal.enter begin fun gl ->
         let env = Proofview.Goal.env gl in
         let sigma = Proofview.Goal.sigma gl in
         let sigma, bll = List.fold_map (interp_bindings ist env) sigma bll in
-        Tacticals.New.tclWITHHOLES ev (h_split ev) sigma bll
+        Tacticals.New.tclWITHHOLES ev (Tactics.split_with_bindings ev) sigma bll
       end
   | TacAnyConstructor (ev,t) ->
       Tactics.any_constructor ev (Option.map (interp_tactic ist) t)
@@ -1786,7 +1797,8 @@ and interp_atomic ist tac =
         let env = Proofview.Goal.env gl in
         let sigma = Proofview.Goal.sigma gl in
         let sigma, bl = interp_bindings ist env sigma bl in
-        Tacticals.New.tclWITHHOLES ev (h_constructor ev (interp_int_or_var ist n)) sigma bl
+        Tacticals.New.tclWITHHOLES ev
+          (Tactics.constructor_tac ev None (interp_int_or_var ist n)) sigma bl
       end
 
   (* Conversion *)
@@ -1795,7 +1807,7 @@ and interp_atomic ist tac =
         let (sigma,r_interp) = interp_red_expr ist (project gl) (pf_env gl) r in
         tclTHEN
 	  (tclEVARS sigma)
-	  (h_reduce r_interp (interp_clause ist (pf_env gl) cl))
+	  (Tactics.reduce r_interp (interp_clause ist (pf_env gl) cl))
           gl
       end
   | TacChange (None,c,cl) ->
@@ -1816,7 +1828,7 @@ and interp_atomic ist tac =
         in
         tclTHEN
 	  (tclEVARS sigma)
-	  (h_change None c_interp (interp_clause ist (pf_env gl) cl))
+	  (Tactics.change None c_interp (interp_clause ist (pf_env gl) cl))
           gl
       end
   | TacChange (Some op,c,cl) ->
@@ -1838,22 +1850,22 @@ and interp_atomic ist tac =
           in
           tclTHEN
 	    (tclEVARS sigma)
-	    (h_change (Some op) c_interp (interp_clause ist env cl))
+	    (Tactics.change (Some op) c_interp (interp_clause ist env cl))
             gl
         end
       end
 
   (* Equivalence relations *)
-  | TacReflexivity -> h_reflexivity
+  | TacReflexivity -> Tactics.intros_reflexivity
   | TacSymmetry c ->
       Proofview.Goal.enter begin fun gl ->
         let env = Proofview.Goal.env gl in
         let cl = interp_clause ist env c in
-        h_symmetry cl
+        Tactics.intros_symmetry cl
       end
   | TacTransitivity c ->
       begin match c with
-      | None -> h_transitivity None
+      | None -> Tactics.intros_transitivity None
       | Some c ->
           Proofview.Goal.enter begin fun gl ->
           let (sigma,c_interp) =
@@ -1861,7 +1873,7 @@ and interp_atomic ist tac =
           in
           Tacticals.New.tclTHEN
 	    (Proofview.V82.tclEVARS sigma)
-	    (h_transitivity (Some c_interp))
+	    (Tactics.intros_transitivity (Some c_interp))
           end
       end
 
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 720d46201..7e65e20c5 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -3881,6 +3881,24 @@ let emit_side_effects eff gl =
     eff;
   { it = [gl.it] ; sigma = Evd.emit_side_effects eff gl.sigma; }
 
+module Simple = struct
+  (** Simplified version of some of the above tactics *)
+
+  let intro x = intro_move (Some x) MoveLast
+
+  let generalize_gen cl =
+    generalize_gen (List.map (on_fst Redexpr.out_with_occurrences) cl)
+  let generalize cl =
+    generalize_gen (List.map (fun c -> ((AllOccurrences,c),Names.Anonymous))
+                        cl)
+
+  let apply c = apply_with_bindings_gen false false [Loc.ghost,(c,NoBindings)]
+  let eapply c = apply_with_bindings_gen false true [Loc.ghost,(c,NoBindings)]
+  let elim c   = elim false (c,NoBindings) None
+  let case   c = general_case_analysis false (c,NoBindings)
+
+end
+
 (** Tacticals defined directly in term of Proofview *)
 module New = struct
   open Proofview.Notations
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index c3df47215..21948f9ae 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -406,6 +406,20 @@ val declare_intro_decomp_eq :
 
 val emit_side_effects : Declareops.side_effects -> tactic
 
+module Simple : sig
+  (** Simplified version of some of the above tactics *)
+
+  val intro           : Id.t -> unit Proofview.tactic
+  val generalize      : constr list -> tactic
+  val generalize_gen  : (constr Locus.with_occurrences * Name.t) list -> tactic
+
+  val apply  : constr -> tactic
+  val eapply : constr -> tactic
+  val elim   : constr -> unit Proofview.tactic
+  val case   : constr -> unit Proofview.tactic
+
+end
+
 (** Tacticals defined directly in term of Proofview *)
 module New : sig
 
diff --git a/tactics/tactics.mllib b/tactics/tactics.mllib
index 7fe584ec1..a4de9e2b4 100644
--- a/tactics/tactics.mllib
+++ b/tactics/tactics.mllib
@@ -8,7 +8,6 @@ Ind_tables
 Eqschemes
 Elimschemes
 Tactics
-Hiddentac
 Elim
 Auto
 Equality
diff --git a/toplevel/lemmas.ml b/toplevel/lemmas.ml
index 91886e076..20b792cc0 100644
--- a/toplevel/lemmas.ml
+++ b/toplevel/lemmas.ml
@@ -300,7 +300,7 @@ let start_proof id kind c ?init_tac ?(compute_guard=[]) hook =
 let rec_tac_initializer finite guard thms snl =
   if finite then
     match List.map (fun (id,(t,_)) -> (id,t)) thms with
-    | (id,_)::l -> Hiddentac.h_mutual_cofix id l
+    | (id,_)::l -> Tactics.mutual_cofix id l 0
     | _ -> assert false
   else
     (* nl is dummy: it will be recomputed at Qed-time *)
@@ -308,7 +308,7 @@ let rec_tac_initializer finite guard thms snl =
      | None -> List.map succ (List.map List.last guard)
      | Some nl -> nl
     in match List.map2 (fun (id,(t,_)) n -> (id,n,t)) thms nl with
-       | (id,n,_)::l -> Hiddentac.h_mutual_fix id n l
+       | (id,n,_)::l -> Tactics.mutual_fix id n l 0
        | _ -> assert false
 
 let start_proof_with_initialization kind recguard thms snl hook =