Imported Upstream version 8.5~beta1+dfsg

1 files changed, 246 insertions, 193 deletions

diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index e82ee021..6025883f 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -1,133 +1,139 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Util
+open Loc
 open Names
 open Term
+open Context
 open Environ
-open Sign
-open Tacmach
 open Proof_type
-open Reduction
 open Evd
-open Evar_refiner
 open Clenv
 open Redexpr
-open Tacticals
-open Libnames
-open Genarg
+open Globnames
 open Tacexpr
-open Nametab
-open Glob_term
 open Pattern
-open Termops
 open Unification
+open Misctypes
+open Locus
 
 (** Main tactics. *)
 
 (** {6 General functions. } *)
 
-val string_of_inductive : constr -> string
-val head_constr       : constr -> constr * constr list
-val head_constr_bound : constr -> constr * constr list
-val is_quantified_hypothesis : identifier -> goal sigma -> bool
-
-exception Bound
+val is_quantified_hypothesis : Id.t -> goal sigma -> bool
 
 (** {6 Primitive tactics. } *)
 
-val introduction    : identifier -> tactic
+val introduction    : ?check:bool -> Id.t -> unit Proofview.tactic
 val refine          : constr -> tactic
-val convert_concl   : constr -> cast_kind -> tactic
-val convert_hyp     : named_declaration -> tactic
-val thin            : identifier list -> tactic
+val convert_concl   : ?check:bool -> types -> cast_kind -> unit Proofview.tactic
+val convert_hyp     : ?check:bool -> named_declaration -> unit Proofview.tactic
+val convert_concl_no_check : types -> cast_kind -> unit Proofview.tactic
+val convert_hyp_no_check : named_declaration -> unit Proofview.tactic
+val thin            : Id.t list -> tactic
 val mutual_fix      :
-  identifier -> int -> (identifier * int * constr) list -> int -> tactic
-val fix             : identifier option -> int -> tactic
-val mutual_cofix    : identifier -> (identifier * constr) list -> int -> tactic
-val cofix           : identifier option -> tactic
+  Id.t -> int -> (Id.t * int * constr) list -> int -> tactic
+val fix             : Id.t option -> int -> tactic
+val mutual_cofix    : Id.t -> (Id.t * constr) list -> int -> tactic
+val cofix           : Id.t option -> tactic
+
+val convert         : constr -> constr -> unit Proofview.tactic
+val convert_leq     : constr -> constr -> unit Proofview.tactic
 
 (** {6 Introduction tactics. } *)
 
-val fresh_id_in_env : identifier list -> identifier -> env -> identifier
-val fresh_id : identifier list -> identifier -> goal sigma -> identifier
-val find_intro_names : rel_context -> goal sigma -> identifier list
+val fresh_id_in_env : Id.t list -> Id.t -> env -> Id.t
+val fresh_id : Id.t list -> Id.t -> goal sigma -> Id.t
+val find_intro_names : rel_context -> goal sigma -> Id.t list
 
-val intro                : tactic
-val introf               : tactic
-val intro_move        : identifier option -> identifier move_location -> tactic
+val intro                : unit Proofview.tactic
+val introf               : unit Proofview.tactic
+val intro_move        : Id.t option -> Id.t move_location -> unit Proofview.tactic
+val intro_move_avoid  : Id.t option -> Id.t list -> Id.t move_location -> unit Proofview.tactic
 
-  (** [intro_avoiding idl] acts as intro but prevents the new identifier
+  (** [intro_avoiding idl] acts as intro but prevents the new Id.t
      to belong to [idl] *)
-val intro_avoiding       : identifier list -> tactic
+val intro_avoiding       : Id.t list -> unit Proofview.tactic
 
-val intro_replacing      : identifier -> tactic
-val intro_using          : identifier -> tactic
-val intro_mustbe_force   : identifier -> tactic
-val intro_then           : (identifier -> tactic) -> tactic
-val intros_using         : identifier list -> tactic
-val intro_erasing        : identifier -> tactic
-val intros_replacing     : identifier list -> tactic
+val intro_replacing      : Id.t -> unit Proofview.tactic
+val intro_using          : Id.t -> unit Proofview.tactic
+val intro_mustbe_force   : Id.t -> unit Proofview.tactic
+val intro_then           : (Id.t -> unit Proofview.tactic) -> unit Proofview.tactic
+val intros_using         : Id.t list -> unit Proofview.tactic
+val intros_replacing     : Id.t list -> unit Proofview.tactic
+val intros_possibly_replacing : Id.t list -> unit Proofview.tactic
 
-val intros               : tactic
+val intros               : unit Proofview.tactic
 
 (** [depth_of_quantified_hypothesis b h g] returns the index of [h] in
    the conclusion of goal [g], up to head-reduction if [b] is [true] *)
 val depth_of_quantified_hypothesis :
   bool -> quantified_hypothesis -> goal sigma -> int
 
-val intros_until_n_wored : int -> tactic
-val intros_until         : quantified_hypothesis -> tactic
+val intros_until         : quantified_hypothesis -> unit Proofview.tactic
 
-val intros_clearing      : bool list -> tactic
+val intros_clearing      : bool list -> unit Proofview.tactic
 
-(** Assuming a tactic [tac] depending on an hypothesis identifier,
+(** Assuming a tactic [tac] depending on an hypothesis Id.t,
    [try_intros_until tac arg] first assumes that arg denotes a
    quantified hypothesis (denoted by name or by index) and try to
    introduce it in context before to apply [tac], otherwise assume the
    hypothesis is already in context and directly apply [tac] *)
 
 val try_intros_until :
-  (identifier -> tactic) -> quantified_hypothesis -> tactic
+  (Id.t -> unit Proofview.tactic) -> quantified_hypothesis -> unit Proofview.tactic
 
 (** Apply a tactic on a quantified hypothesis, an hypothesis in context
    or a term with bindings *)
 
 val onInductionArg :
-  (constr with_bindings -> tactic) ->
-    constr with_bindings induction_arg -> tactic
+  (clear_flag -> constr with_bindings -> unit Proofview.tactic) ->
+    constr with_bindings induction_arg -> unit Proofview.tactic
+
+(** Tell if a used hypothesis should be cleared by default or not *)
+
+val use_clear_hyp_by_default : unit -> bool
 
 (** {6 Introduction tactics with eliminations. } *)
 
-val intro_pattern  : identifier move_location -> intro_pattern_expr -> tactic
-val intro_patterns : intro_pattern_expr located list -> tactic
-val intros_pattern :
-  identifier move_location -> intro_pattern_expr located list -> tactic
+val intro_patterns : intro_patterns -> unit Proofview.tactic
+val intro_patterns_to : Id.t move_location -> intro_patterns ->
+  unit Proofview.tactic
+val intro_patterns_bound_to : int -> Id.t move_location -> intro_patterns ->
+  unit Proofview.tactic
+val intro_pattern_to : Id.t move_location -> delayed_open_constr intro_pattern_expr ->
+  unit Proofview.tactic
+
+(** Implements user-level "intros", with [] standing for "**" *)
+val intros_patterns : intro_patterns -> unit Proofview.tactic
 
 (** {6 Exact tactics. } *)
 
-val assumption       : tactic
+val assumption       : unit Proofview.tactic
 val exact_no_check   : constr -> tactic
 val vm_cast_no_check : constr -> tactic
-val exact_check      : constr -> tactic
-val exact_proof      : Topconstr.constr_expr -> tactic
+val exact_check      : constr -> unit Proofview.tactic
+val exact_proof      : Constrexpr.constr_expr -> tactic
 
 (** {6 Reduction tactics. } *)
 
 type tactic_reduction = env -> evar_map -> constr -> constr
 
-val reduct_in_hyp     : tactic_reduction -> hyp_location -> tactic
-val reduct_option     : tactic_reduction * cast_kind -> goal_location -> tactic
+type change_arg = evar_map -> evar_map * constr
+
+val reduct_in_hyp     : ?check:bool -> tactic_reduction -> hyp_location -> tactic
+val reduct_option     : ?check:bool -> tactic_reduction * cast_kind -> goal_location -> tactic
 val reduct_in_concl   : tactic_reduction * cast_kind -> tactic
-val change_in_concl   : (occurrences * constr_pattern) option -> constr -> 
-                        tactic
-val change_in_hyp     : (occurrences * constr_pattern) option -> constr ->
-                        hyp_location -> tactic
+val change_in_concl   : (occurrences * constr_pattern) option -> change_arg -> unit Proofview.tactic
+val change_concl      : constr -> unit Proofview.tactic
+val change_in_hyp     : (occurrences * constr_pattern) option -> change_arg ->
+                        hyp_location -> unit Proofview.tactic
 val red_in_concl      : tactic
 val red_in_hyp        : hyp_location -> tactic
 val red_option        : goal_location -> tactic
@@ -148,7 +154,7 @@ val unfold_in_hyp     :
 val unfold_option     :
   (occurrences * evaluable_global_reference) list -> goal_location -> tactic
 val change            :
-  constr_pattern option -> constr -> clause -> tactic
+  constr_pattern option -> change_arg -> clause -> tactic
 val pattern_option    :
   (occurrences * constr) list -> goal_location -> tactic
 val reduce            : red_expr -> clause -> tactic
@@ -156,44 +162,50 @@ val unfold_constr     : global_reference -> tactic
 
 (** {6 Modification of the local context. } *)
 
-val clear         : identifier list -> tactic
-val clear_body    : identifier list -> tactic
-val keep          : identifier list -> tactic
+val clear         : Id.t list -> tactic
+val clear_body    : Id.t list -> unit Proofview.tactic
+val unfold_body   : Id.t -> tactic
+val keep          : Id.t list -> unit Proofview.tactic
+val apply_clear_request : clear_flag -> bool -> constr -> unit Proofview.tactic
 
-val specialize    : int option -> constr with_bindings -> tactic
+val specialize    : constr with_bindings -> tactic
 
-val move_hyp      : bool -> identifier -> identifier move_location -> tactic
-val rename_hyp    : (identifier * identifier) list -> tactic
+val move_hyp      : Id.t -> Id.t move_location -> tactic
+val rename_hyp    : (Id.t * Id.t) list -> unit Proofview.tactic
 
-val revert        : identifier list -> tactic
+val revert        : Id.t list -> unit Proofview.tactic
 
 (** {6 Resolution tactics. } *)
 
 val apply_type : constr -> constr list -> tactic
-val apply_term : constr -> constr list -> tactic
-val bring_hyps : named_context -> tactic
+val bring_hyps : named_context -> unit Proofview.tactic
 
-val apply                 : constr -> tactic
-val eapply                : constr -> tactic
+val apply                 : constr -> unit Proofview.tactic
+val eapply                : constr -> unit Proofview.tactic
 
 val apply_with_bindings_gen :
-  advanced_flag -> evars_flag -> constr with_bindings located list -> tactic
+  advanced_flag -> evars_flag -> (clear_flag * constr with_bindings located) list -> unit Proofview.tactic
 
-val apply_with_bindings   : constr with_bindings -> tactic
-val eapply_with_bindings  : constr with_bindings -> tactic
+val apply_with_delayed_bindings_gen :
+  advanced_flag -> evars_flag -> (clear_flag * delayed_open_constr_with_bindings located) list -> unit Proofview.tactic
 
-val cut_and_apply         : constr -> tactic
+val apply_with_bindings   : constr with_bindings -> unit Proofview.tactic
+val eapply_with_bindings  : constr with_bindings -> unit Proofview.tactic
+
+val cut_and_apply         : constr -> unit Proofview.tactic
 
 val apply_in :
-  advanced_flag -> evars_flag -> identifier -> 
-    constr with_bindings located list ->
-    intro_pattern_expr located option -> tactic
+  advanced_flag -> evars_flag -> clear_flag -> Id.t -> 
+    (clear_flag * constr with_bindings located) list ->
+    intro_pattern option -> unit Proofview.tactic
 
-val simple_apply_in : identifier -> constr -> tactic
+val apply_delayed_in :
+  advanced_flag -> evars_flag -> clear_flag -> Id.t -> 
+    (clear_flag * delayed_open_constr_with_bindings located) list ->
+    intro_pattern option -> unit Proofview.tactic
 
 (** {6 Elimination tactics. } *)
 
-
 (*
    The general form of an induction principle is the following:
 
@@ -223,7 +235,6 @@ type elim_scheme = {
   elimc: constr with_bindings option;
   elimt: types;
   indref: global_reference option;
-  index: int;              (** index of the elimination type in the scheme *)
   params: rel_context;     (** (prm1,tprm1);(prm2,tprm2)...(prmp,tprmp) *)
   nparams: int;            (** number of parameters *)
   predicates: rel_context; (** (Qq, (Tq_1 -> Tq_2 ->...-> Tq_nq)), (Q1,...) *)
@@ -240,150 +251,192 @@ type elim_scheme = {
   farg_in_concl: bool;     (** true if (f...) appears at the end of conclusion *)
 }
 
-
 val compute_elim_sig : ?elimc: constr with_bindings -> types -> elim_scheme
-val rebuild_elimtype_from_scheme: elim_scheme -> types
 
 (** elim principle with the index of its inductive arg *)
 type eliminator = {
   elimindex : int option;  (** None = find it automatically *)
+  elimrename : (bool * int array) option; (** None = don't rename Prop hyps with H-names *)
   elimbody : constr with_bindings
 }
 
-val elimination_clause_scheme : evars_flag -> ?flags:unify_flags -> 
-  int -> clausenv -> clausenv -> tactic
+val general_elim  : evars_flag -> clear_flag ->
+  constr with_bindings -> eliminator -> unit Proofview.tactic
 
-val elimination_in_clause_scheme : evars_flag -> ?flags:unify_flags -> 
-  identifier -> int -> clausenv -> clausenv -> tactic
+val general_elim_clause : evars_flag -> unify_flags -> identifier option ->
+  clausenv -> eliminator -> unit Proofview.tactic
 
-val general_elim_clause_gen : (int -> Clenv.clausenv -> 'a -> tactic) ->
-  'a -> eliminator -> tactic
-
-val general_elim  : evars_flag ->
-  constr with_bindings -> eliminator -> tactic
-val general_elim_in : evars_flag -> identifier ->
-  constr with_bindings -> eliminator -> tactic
-
-val default_elim  : evars_flag -> constr with_bindings -> tactic
-val simplest_elim : constr -> tactic
+val default_elim  : evars_flag -> clear_flag -> constr with_bindings ->
+  unit Proofview.tactic
+val simplest_elim : constr -> unit Proofview.tactic
 val elim :
-  evars_flag -> constr with_bindings -> constr with_bindings option -> tactic
+  evars_flag -> clear_flag -> constr with_bindings -> constr with_bindings option -> unit Proofview.tactic
 
-val simple_induct : quantified_hypothesis -> tactic
+val simple_induct : quantified_hypothesis -> unit Proofview.tactic
 
-val new_induct : evars_flag -> 
-  (evar_map * constr with_bindings) induction_arg list ->
-  constr with_bindings option ->
-    intro_pattern_expr located option * intro_pattern_expr located option ->
-      clause option -> tactic
+val induction : evars_flag -> clear_flag -> constr -> or_and_intro_pattern option ->
+  constr with_bindings option -> unit Proofview.tactic
 
 (** {6 Case analysis tactics. } *)
 
-val general_case_analysis : evars_flag -> constr with_bindings ->  tactic
-val simplest_case         : constr -> tactic
+val general_case_analysis : evars_flag -> clear_flag -> constr with_bindings ->  unit Proofview.tactic
+val simplest_case         : constr -> unit Proofview.tactic
 
-val simple_destruct          : quantified_hypothesis -> tactic
-val new_destruct : evars_flag ->
-  (evar_map * constr with_bindings) induction_arg list ->
-  constr with_bindings option ->
-    intro_pattern_expr located option * intro_pattern_expr located option ->
-      clause option -> tactic
+val simple_destruct       : quantified_hypothesis -> unit Proofview.tactic
+val destruct : evars_flag -> clear_flag -> constr -> or_and_intro_pattern option ->
+  constr with_bindings option -> unit Proofview.tactic
 
 (** {6 Generic case analysis / induction tactics. } *)
 
+(** Implements user-level "destruct" and "induction" *)
+
 val 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 *
-  clause option -> tactic
+  (delayed_open_constr_with_bindings induction_arg
+   * (intro_pattern_naming option * or_and_intro_pattern option)
+   * clause option) list *
+  constr with_bindings option -> unit Proofview.tactic
 
 (** {6 Eliminations giving the type instead of the proof. } *)
 
-val case_type         : constr  -> tactic
-val elim_type         : constr  -> tactic
+val case_type         : types -> unit Proofview.tactic
+val elim_type         : types -> unit Proofview.tactic
 
-(** {6 Some eliminations which are frequently used. } *)
+(** {6 Constructor tactics. } *)
 
-val impE : identifier -> tactic
-val andE : identifier -> tactic
-val orE  : identifier -> tactic
-val dImp : clause -> tactic
-val dAnd : clause -> tactic
-val dorE : bool -> clause ->tactic
+val constructor_tac      : evars_flag -> int option -> int ->
+  constr bindings -> unit Proofview.tactic
+val any_constructor      : evars_flag -> unit Proofview.tactic option -> unit Proofview.tactic
+val one_constructor      : int -> constr bindings  -> unit Proofview.tactic
 
+val left                 : constr bindings -> unit Proofview.tactic
+val right                : constr bindings -> unit Proofview.tactic
+val split                : constr bindings -> unit Proofview.tactic
 
-(** {6 Introduction tactics. } *)
+val left_with_bindings  : evars_flag -> constr bindings -> unit Proofview.tactic
+val right_with_bindings : evars_flag -> constr bindings -> unit Proofview.tactic
+val split_with_bindings : evars_flag -> constr bindings list -> unit Proofview.tactic
 
-val constructor_tac      : evars_flag -> int option -> int ->
-  constr bindings -> tactic
-val any_constructor      : evars_flag -> tactic option -> tactic
-val one_constructor      : int -> constr bindings  -> tactic
-
-val left                 : constr bindings -> tactic
-val right                : constr bindings -> tactic
-val split                : constr bindings -> tactic
-
-val left_with_bindings  : evars_flag -> constr bindings -> tactic
-val right_with_bindings : evars_flag -> constr bindings -> tactic
-val split_with_bindings : evars_flag -> constr bindings list -> tactic
-
-val simplest_left        : tactic
-val simplest_right       : tactic
-val simplest_split       : tactic
-
-(** {6 Logical connective tactics. } *)
-
-val register_setoid_reflexivity : tactic -> unit
-val reflexivity_red             : bool -> tactic
-val reflexivity                 : tactic
-val intros_reflexivity          : tactic
-
-val register_setoid_symmetry : tactic -> unit
-val symmetry_red                : bool -> tactic
-val symmetry                    : tactic
-val register_setoid_symmetry_in : (identifier -> tactic) -> unit
-val symmetry_in                 : identifier -> tactic
-val intros_symmetry             : clause -> tactic
-
-val register_setoid_transitivity : (constr option -> tactic) -> unit
-val transitivity_red            : bool -> constr option -> tactic
-val transitivity                : constr -> tactic
-val etransitivity               : tactic
-val intros_transitivity         : constr option -> tactic
-
-val cut                         : constr -> tactic
-val cut_intro                   : constr -> tactic
-val assert_replacing            : identifier -> types -> tactic -> tactic
-val cut_replacing               : identifier -> types -> tactic -> tactic
-val cut_in_parallel             : constr list -> tactic
-
-val assert_as : bool -> intro_pattern_expr located option -> constr -> tactic
-val forward   : tactic option -> intro_pattern_expr located option -> constr -> tactic
-val letin_tac : (bool * intro_pattern_expr located) option -> name ->
-  constr -> types option -> clause -> tactic
-val letin_pat_tac : (bool * intro_pattern_expr located) option -> name ->
-  evar_map * constr -> types option -> clause -> tactic
-val assert_tac : name -> types -> tactic
-val assert_by  : name -> types -> tactic -> tactic
-val pose_proof : name -> constr -> tactic
+val simplest_left        : unit Proofview.tactic
+val simplest_right       : unit Proofview.tactic
+val simplest_split       : unit Proofview.tactic
+
+(** {6 Equality tactics. } *)
+
+val setoid_reflexivity : unit Proofview.tactic Hook.t
+val reflexivity_red             : bool -> unit Proofview.tactic
+val reflexivity                 : unit Proofview.tactic
+val intros_reflexivity          : unit Proofview.tactic
+
+val setoid_symmetry : unit Proofview.tactic Hook.t
+val symmetry_red                : bool -> unit Proofview.tactic
+val symmetry                    : unit Proofview.tactic
+val setoid_symmetry_in : (Id.t -> unit Proofview.tactic) Hook.t
+val intros_symmetry             : clause -> unit Proofview.tactic
+
+val setoid_transitivity : (constr option -> unit Proofview.tactic) Hook.t
+val transitivity_red            : bool -> constr option -> unit Proofview.tactic
+val transitivity                : constr -> unit Proofview.tactic
+val etransitivity               : unit Proofview.tactic
+val intros_transitivity         : constr option -> unit Proofview.tactic
+
+(** {6 Cut tactics. } *)
+
+val assert_before_replacing: Id.t -> types -> unit Proofview.tactic
+val assert_after_replacing : Id.t -> types -> unit Proofview.tactic
+val assert_before : Name.t -> types -> unit Proofview.tactic
+val assert_after  : Name.t -> types -> unit Proofview.tactic
+
+val assert_as     : (* true = before *) bool ->
+  intro_pattern option -> constr -> unit Proofview.tactic
+
+(** Implements the tactics assert, enough and pose proof; note that "by"
+    applies on the first goal for both assert and enough *)
+
+val assert_by  : Name.t -> types -> unit Proofview.tactic ->
+  unit Proofview.tactic
+val enough_by  : Name.t -> types -> unit Proofview.tactic ->
+  unit Proofview.tactic
+val pose_proof : Name.t -> constr ->
+  unit Proofview.tactic
+
+(** Common entry point for user-level "assert", "enough" and "pose proof" *)
+
+val forward   : bool -> unit Proofview.tactic option ->
+  intro_pattern option -> constr -> unit Proofview.tactic
+
+(** Implements the tactic cut, actually a modus ponens rule *)
+
+val cut        : types -> unit Proofview.tactic
+
+(** {6 Tactics for adding local definitions. } *)
+
+val letin_tac : (bool * intro_pattern_naming) option ->
+  Name.t -> constr -> types option -> clause -> unit Proofview.tactic
+
+(** Common entry point for user-level "set", "pose" and "remember" *)
+
+val letin_pat_tac : (bool * intro_pattern_naming) option ->
+  Name.t -> pending_constr -> clause -> unit Proofview.tactic
+
+(** {6 Generalize tactics. } *)
 
 val generalize      : constr list -> tactic
-val generalize_gen  : ((occurrences * constr) * name) list -> tactic
+val generalize_gen  : ((occurrences * constr) * Name.t) list -> tactic
+val new_generalize  : constr list -> unit Proofview.tactic
+val new_generalize_gen  : ((occurrences * constr) * Name.t) list -> unit Proofview.tactic
+
 val generalize_dep  : ?with_let:bool (** Don't lose let bindings *) -> constr  -> tactic
 
-val unify           : ?state:Names.transparent_state -> constr -> constr -> tactic
-val resolve_classes : tactic
+(** {6 Other tactics. } *)
+
+val unify           : ?state:Names.transparent_state -> constr -> constr -> unit Proofview.tactic
+
+val tclABSTRACT : Id.t option -> unit Proofview.tactic -> unit Proofview.tactic
+
+val admit_as_an_axiom : unit Proofview.tactic
+
+val abstract_generalize : ?generalize_vars:bool -> ?force_dep:bool -> Id.t -> unit Proofview.tactic
+val specialize_eqs : Id.t -> tactic
+
+val general_rewrite_clause :
+  (bool -> evars_flag -> constr with_bindings -> clause -> unit Proofview.tactic) Hook.t
+
+val subst_one :
+  (bool -> Id.t -> Id.t * constr * bool -> unit Proofview.tactic) Hook.t
+
+val declare_intro_decomp_eq :
+  ((int -> unit Proofview.tactic) -> Coqlib.coq_eq_data * types *
+   (types * constr * constr) ->
+   constr * types -> unit Proofview.tactic) -> unit
+
+(** {6 Simple form of basic tactics. } *)
+
+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 -> unit Proofview.tactic
+  val eapply : constr -> unit Proofview.tactic
+  val elim   : constr -> unit Proofview.tactic
+  val case   : constr -> unit Proofview.tactic
+  val apply_in : identifier -> constr -> unit Proofview.tactic
+
+end
 
-val tclABSTRACT : identifier option -> tactic -> tactic
+(** {6 Tacticals defined directly in term of Proofview} *)
 
-val admit_as_an_axiom : tactic
+module New : sig
 
-val abstract_generalize : ?generalize_vars:bool -> ?force_dep:bool -> identifier -> tactic
-val specialize_eqs : identifier -> tactic
+  val refine : ?unsafe:bool -> (Evd.evar_map -> Evd.evar_map*constr) -> unit Proofview.tactic
+  (** [refine ?unsafe c] is [Proofview.Refine.refine ?unsafe c]
+      followed by beta-iota-reduction of the conclusion. *)
 
-val register_general_multi_rewrite :
-  (bool -> evars_flag -> constr with_bindings -> clause -> tactic) -> unit
+  val reduce_after_refine : unit Proofview.tactic
+  (** The reducing tactic called after {!refine}. *)
 
-val register_subst_one :
-  (bool -> identifier -> identifier * constr * bool -> tactic) -> unit
+  open Proofview
+  val exact_proof : Constrexpr.constr_expr -> unit tactic
+end