diff options
Diffstat (limited to 'tactics/tactics.mli')
| -rw-r--r-- | tactics/tactics.mli | 88 |
1 files changed, 44 insertions, 44 deletions
diff --git a/tactics/tactics.mli b/tactics/tactics.mli index f33ef1bc5..041edd250 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -38,44 +38,44 @@ open Locus 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 +val is_quantified_hypothesis : Id.t -> goal sigma -> bool exception Bound (** {6 Primitive tactics. } *) -val introduction : identifier -> tactic +val introduction : Id.t -> tactic val refine : constr -> tactic val convert_concl : constr -> cast_kind -> tactic val convert_hyp : named_declaration -> tactic -val thin : identifier list -> 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 (** {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_move : Id.t option -> Id.t move_location -> 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 -> 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 -> 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_erasing : Id.t -> tactic +val intros_replacing : Id.t list -> tactic val intros : tactic @@ -96,7 +96,7 @@ val intros_clearing : bool list -> tactic hypothesis is already in context and directly apply [tac] *) val try_intros_until : - (identifier -> tactic) -> quantified_hypothesis -> tactic + (Id.t -> tactic) -> quantified_hypothesis -> tactic (** Apply a tactic on a quantified hypothesis, an hypothesis in context or a term with bindings *) @@ -107,10 +107,10 @@ val onInductionArg : (** {6 Introduction tactics with eliminations. } *) -val intro_pattern : identifier move_location -> intro_pattern_expr -> tactic +val intro_pattern : Id.t 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 + Id.t move_location -> intro_pattern_expr located list -> tactic (** {6 Exact tactics. } *) @@ -159,16 +159,16 @@ 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 -> tactic +val keep : Id.t list -> tactic val specialize : int option -> constr with_bindings -> tactic -val move_hyp : bool -> identifier -> identifier move_location -> tactic -val rename_hyp : (identifier * identifier) list -> tactic +val move_hyp : bool -> Id.t -> Id.t move_location -> tactic +val rename_hyp : (Id.t * Id.t) list -> tactic -val revert : identifier list -> tactic +val revert : Id.t list -> tactic (** {6 Resolution tactics. } *) @@ -188,11 +188,11 @@ val eapply_with_bindings : constr with_bindings -> tactic val cut_and_apply : constr -> tactic val apply_in : - advanced_flag -> evars_flag -> identifier -> + advanced_flag -> evars_flag -> Id.t -> constr with_bindings located list -> intro_pattern_expr located option -> tactic -val simple_apply_in : identifier -> constr -> tactic +val simple_apply_in : Id.t -> constr -> tactic (** {6 Elimination tactics. } *) @@ -257,14 +257,14 @@ val elimination_clause_scheme : evars_flag -> ?flags:unify_flags -> int -> clausenv -> clausenv -> tactic val elimination_in_clause_scheme : evars_flag -> ?flags:unify_flags -> - identifier -> int -> clausenv -> clausenv -> tactic + Id.t -> int -> clausenv -> clausenv -> 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 -> +val general_elim_in : evars_flag -> Id.t -> constr with_bindings -> eliminator -> tactic val default_elim : evars_flag -> constr with_bindings -> tactic @@ -308,9 +308,9 @@ val elim_type : constr -> tactic (** {6 Some eliminations which are frequently used. } *) -val impE : identifier -> tactic -val andE : identifier -> tactic -val orE : identifier -> tactic +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 @@ -345,8 +345,8 @@ 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 register_setoid_symmetry_in : (Id.t -> tactic) -> unit +val symmetry_in : Id.t -> tactic val intros_symmetry : clause -> tactic val register_setoid_transitivity : (constr option -> tactic) -> unit @@ -357,8 +357,8 @@ 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 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 @@ -378,15 +378,15 @@ 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 : identifier option -> tactic -> tactic +val tclABSTRACT : Id.t option -> tactic -> tactic val admit_as_an_axiom : tactic -val abstract_generalize : ?generalize_vars:bool -> ?force_dep:bool -> identifier -> tactic -val specialize_eqs : identifier -> tactic +val abstract_generalize : ?generalize_vars:bool -> ?force_dep:bool -> Id.t -> tactic +val specialize_eqs : Id.t -> tactic val register_general_multi_rewrite : (bool -> evars_flag -> constr with_bindings -> clause -> tactic) -> unit val register_subst_one : - (bool -> identifier -> identifier * constr * bool -> tactic) -> unit + (bool -> Id.t -> Id.t * constr * bool -> tactic) -> unit |