From 579770c44251f2b8d01ecc6252810ec80da374f5 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 20 Nov 2014 19:52:30 +0100
Subject: Re-removing the Hiddentac module. For some reason it had been
 reintroduced by commit bf0185694.

---
 tactics/hiddentac.ml  |  96 --------------------------------------
 tactics/hiddentac.mli | 125 --------------------------------------------------
 2 files changed, 221 deletions(-)
 delete mode 100644 tactics/hiddentac.ml
 delete mode 100644 tactics/hiddentac.mli

diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml
deleted file mode 100644
index 806d373199..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,cl],e)
-let h_new_destruct ev c idl e cl = h_induction_destruct false ev ([c,idl,cl],e)
-
-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 e1e9ebaddc..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 -> tactic
-val h_intro           : Id.t -> tactic
-val h_intros_until    : quantified_hypothesis -> tactic
-
-val h_assumption      : 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 -> tactic
-
-val h_elim            : evars_flag -> constr with_bindings ->
-                        constr with_bindings option -> tactic
-val h_elim_type       : constr -> tactic
-val h_case            : evars_flag -> constr with_bindings -> 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 -> tactic
-val h_let_pat_tac     : letin_flag -> Name.t -> evar_map * constr ->
-                        Locus.clause -> intro_pattern_expr located option ->
-                        tactic
-
-(** Derived basic tactics *)
-
-val h_simple_induction   : quantified_hypothesis -> tactic
-val h_simple_destruct    : quantified_hypothesis -> tactic
-val h_simple_induction_destruct : rec_flag -> quantified_hypothesis -> 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 -> 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 -> 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) *
-    Locus.clause option) list *
-  constr with_bindings option -> 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 -> tactic
-val h_left            : evars_flag -> constr bindings -> tactic
-val h_right           : evars_flag -> constr bindings -> tactic
-val h_split           : evars_flag -> constr bindings list -> tactic
-
-val h_one_constructor : int -> tactic
-val h_simplest_left   : tactic
-val h_simplest_right  : 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     : tactic
-val h_symmetry        : Locus.clause -> tactic
-val h_transitivity    : constr option -> tactic
-
-val h_simplest_apply  : constr -> tactic
-val h_simplest_eapply : constr -> tactic
-val h_simplest_elim   : constr -> tactic
-val h_simplest_case   : constr -> tactic
-
-val h_intro_patterns  : intro_pattern_expr located list -> tactic
-- 
cgit v1.2.3