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.

10 files changed, 109 insertions, 284 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index e87158bdde..9156e1f04d 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 369107f6c8..256f84ba4c 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 1389e1de2b..cb518a03a3 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 094cb6b19e..1c7b8d49f6 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 e61922d07a..0000000000
--- 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 ad76543744..0000000000
--- 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 083426531e..4e20c2fa9f 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 720d462010..7e65e20c5f 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 c3df47215a..21948f9ae7 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 7fe584ec17..a4de9e2b4a 100644
--- a/tactics/tactics.mllib
+++ b/tactics/tactics.mllib
@@ -8,7 +8,6 @@ Ind_tables
 Eqschemes
 Elimschemes
 Tactics
-Hiddentac
 Elim
 Auto
 Equality