summaryrefslogtreecommitdiff
path: root/tactics/tactics.mli
diff options
context:
space:
mode:
Diffstat (limited to 'tactics/tactics.mli')
-rw-r--r--tactics/tactics.mli439
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