diff options
Diffstat (limited to 'tactics/tactics.mli')
| -rw-r--r-- | tactics/tactics.mli | 167 |
1 files changed, 87 insertions, 80 deletions
diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 7acd803bd..dff606fe1 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -61,49 +61,49 @@ 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 : Id.t option -> Id.t 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 (** [intro_avoiding idl] acts as intro but prevents the new Id.t to belong to [idl] *) -val intro_avoiding : Id.t list -> tactic +val intro_avoiding : Id.t list -> unit Proofview.tactic val intro_replacing : Id.t -> tactic -val intro_using : Id.t -> tactic -val intro_mustbe_force : Id.t -> tactic -val intro_then : (Id.t -> tactic) -> tactic -val intros_using : Id.t list -> 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 intro_erasing : Id.t -> tactic -val intros_replacing : Id.t list -> tactic +val intros_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_n_wored : int -> unit Proofview.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 : - (Id.t -> 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 + (constr with_bindings -> unit Proofview.tactic) -> + constr with_bindings induction_arg -> unit Proofview.tactic (** Complete intro_patterns up to some length; fails if more patterns than required *) @@ -113,10 +113,10 @@ val adjust_intro_patterns : int -> intro_pattern_expr located list -> (** {6 Introduction tactics with eliminations. } *) -val intro_pattern : Id.t move_location -> intro_pattern_expr -> tactic -val intro_patterns : intro_pattern_expr located list -> tactic +val intro_pattern : Id.t move_location -> intro_pattern_expr -> unit Proofview.tactic +val intro_patterns : intro_pattern_expr located list -> unit Proofview.tactic val intros_pattern : - Id.t move_location -> intro_pattern_expr located list -> tactic + Id.t move_location -> intro_pattern_expr located list -> unit Proofview.tactic (** {6 Exact tactics. } *) @@ -197,9 +197,9 @@ val cut_and_apply : constr -> tactic val apply_in : advanced_flag -> evars_flag -> Id.t -> constr with_bindings located list -> - intro_pattern_expr located option -> tactic + intro_pattern_expr located option -> unit Proofview.tactic -val simple_apply_in : Id.t -> constr -> tactic +val simple_apply_in : Id.t -> constr -> unit Proofview.tactic (** {6 Elimination tactics. } *) @@ -274,30 +274,30 @@ val general_elim : evars_flag -> val general_elim_in : evars_flag -> Id.t -> constr with_bindings -> eliminator -> tactic -val default_elim : evars_flag -> constr with_bindings -> tactic -val simplest_elim : constr -> tactic +val default_elim : evars_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 -> 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 + clause 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 -> constr with_bindings -> unit Proofview.tactic +val simplest_case : constr -> unit Proofview.tactic -val simple_destruct : quantified_hypothesis -> tactic +val simple_destruct : quantified_hypothesis -> unit Proofview.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 + clause option -> unit Proofview.tactic (** {6 Generic case analysis / induction tactics. } *) @@ -306,7 +306,7 @@ val induction_destruct : rec_flag -> evars_flag -> (intro_pattern_expr located option * intro_pattern_expr located option)) list * constr with_bindings option * - clause option -> tactic + clause option -> unit Proofview.tactic (** {6 Eliminations giving the type instead of the proof. } *) @@ -315,68 +315,68 @@ val elim_type : constr -> tactic (** {6 Some eliminations which are frequently used. } *) -val impE : Id.t -> tactic -val andE : Id.t -> tactic -val orE : Id.t -> tactic -val dImp : clause -> tactic -val dAnd : clause -> tactic -val dorE : bool -> clause ->tactic +val impE : Id.t -> unit Proofview.tactic +val andE : Id.t -> unit Proofview.tactic +val orE : Id.t -> unit Proofview.tactic +val dImp : clause -> unit Proofview.tactic +val dAnd : clause -> unit Proofview.tactic +val dorE : bool -> clause -> unit Proofview.tactic (** {6 Introduction tactics. } *) 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 + 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 -> tactic -val right : constr bindings -> tactic -val split : constr bindings -> tactic +val left : constr bindings -> unit Proofview.tactic +val right : constr bindings -> unit Proofview.tactic +val split : constr bindings -> unit Proofview.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 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 simplest_left : tactic -val simplest_right : tactic -val simplest_split : tactic +val simplest_left : unit Proofview.tactic +val simplest_right : unit Proofview.tactic +val simplest_split : unit Proofview.tactic (** {6 Logical connective tactics. } *) -val setoid_reflexivity : tactic Hook.t -val reflexivity_red : bool -> tactic -val reflexivity : tactic -val intros_reflexivity : tactic +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 : tactic Hook.t -val symmetry_red : bool -> tactic -val symmetry : tactic -val setoid_symmetry_in : (Id.t -> tactic) Hook.t -val symmetry_in : Id.t -> tactic -val intros_symmetry : clause -> 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 symmetry_in : Id.t -> unit Proofview.tactic +val intros_symmetry : clause -> unit Proofview.tactic -val setoid_transitivity : (constr option -> tactic) Hook.t -val transitivity_red : bool -> constr option -> tactic -val transitivity : constr -> tactic -val etransitivity : tactic -val intros_transitivity : constr option -> 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 val cut : constr -> tactic -val cut_intro : constr -> tactic +val cut_intro : constr -> unit Proofview.tactic val assert_replacing : Id.t -> types -> tactic -> tactic val cut_replacing : Id.t -> 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 assert_as : bool -> intro_pattern_expr located option -> constr -> unit Proofview.tactic +val forward : unit Proofview.tactic option -> intro_pattern_expr located option -> constr -> unit Proofview.tactic val letin_tac : (bool * intro_pattern_expr located) option -> Name.t -> - constr -> types option -> clause -> tactic + constr -> types option -> clause -> unit Proofview.tactic val letin_pat_tac : (bool * intro_pattern_expr located) option -> Name.t -> - evar_map * constr -> types option -> clause -> tactic -val assert_tac : Name.t -> types -> tactic -val assert_by : Name.t -> types -> tactic -> tactic -val pose_proof : Name.t -> constr -> tactic + evar_map * constr -> types option -> clause -> unit Proofview.tactic +val assert_tac : Name.t -> types -> unit Proofview.tactic +val assert_by : Name.t -> types -> unit Proofview.tactic -> unit Proofview.tactic +val pose_proof : Name.t -> constr -> unit Proofview.tactic val generalize : constr list -> tactic val generalize_gen : ((occurrences * constr) * Name.t) list -> tactic @@ -385,23 +385,30 @@ val generalize_dep : ?with_let:bool (** Don't lose let bindings *) -> constr - val unify : ?state:Names.transparent_state -> constr -> constr -> tactic val resolve_classes : tactic -val tclABSTRACT : Id.t option -> tactic -> tactic +val tclABSTRACT : Id.t option -> unit Proofview.tactic -> tactic -val admit_as_an_axiom : tactic +val admit_as_an_axiom : unit Proofview.tactic -val abstract_generalize : ?generalize_vars:bool -> ?force_dep:bool -> Id.t -> tactic +val abstract_generalize : ?generalize_vars:bool -> ?force_dep:bool -> Id.t -> unit Proofview.tactic val specialize_eqs : Id.t -> tactic val general_multi_rewrite : - (bool -> evars_flag -> constr with_bindings -> clause -> tactic) Hook.t + (bool -> evars_flag -> constr with_bindings -> clause -> unit Proofview.tactic) Hook.t val subst_one : - (bool -> Id.t -> Id.t * constr * bool -> tactic) Hook.t + (bool -> Id.t -> Id.t * constr * bool -> unit Proofview.tactic) Hook.t val declare_intro_decomp_eq : - ((int -> tactic) -> Coqlib.coq_eq_data * types * + ((int -> unit Proofview.tactic) -> Coqlib.coq_eq_data * types * (types * constr * constr) -> - clausenv -> tactic) -> unit + clausenv -> unit Proofview.tactic) -> unit val emit_side_effects : Declareops.side_effects -> tactic + +(** Tacticals defined directly in term of Proofview *) +module New : sig + open Proofview + + val exact_proof : Constrexpr.constr_expr -> unit tactic +end |