diff options
Diffstat (limited to 'tactics/tactics.mli')
| -rw-r--r-- | tactics/tactics.mli | 23 |
1 files changed, 16 insertions, 7 deletions
diff --git a/tactics/tactics.mli b/tactics/tactics.mli index b17330f13..57f20d2ff 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -18,7 +18,6 @@ open Clenv open Redexpr open Pattern open Unification -open Misctypes open Tactypes open Locus open Ltac_pretype @@ -56,8 +55,8 @@ val find_intro_names : rel_context -> goal sigma -> Id.t list 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.Set.t -> Id.t move_location -> unit Proofview.tactic +val intro_move : Id.t option -> Id.t Logic.move_location -> unit Proofview.tactic +val intro_move_avoid : Id.t option -> Id.Set.t -> Id.t Logic.move_location -> unit Proofview.tactic (** [intro_avoiding idl] acts as intro but prevents the new Id.t to belong to [idl] *) @@ -91,6 +90,11 @@ val intros_clearing : bool list -> unit Proofview.tactic val try_intros_until : (Id.t -> unit Proofview.tactic) -> quantified_hypothesis -> unit Proofview.tactic +type evars_flag = bool (* true = pose evars false = fail on evars *) +type rec_flag = bool (* true = recursive false = not recursive *) +type advanced_flag = bool (* true = advanced false = basic *) +type clear_flag = bool option (* true = clear hyp, false = keep hyp, None = use default *) + (** Apply a tactic on a quantified hypothesis, an hypothesis in context or a term with bindings *) @@ -117,11 +121,11 @@ val use_clear_hyp_by_default : unit -> bool (** {6 Introduction tactics with eliminations. } *) val intro_patterns : evars_flag -> intro_patterns -> unit Proofview.tactic -val intro_patterns_to : evars_flag -> Id.t move_location -> intro_patterns -> +val intro_patterns_to : evars_flag -> Id.t Logic.move_location -> intro_patterns -> unit Proofview.tactic -val intro_patterns_bound_to : evars_flag -> int -> Id.t move_location -> intro_patterns -> +val intro_patterns_bound_to : evars_flag -> int -> Id.t Logic.move_location -> intro_patterns -> unit Proofview.tactic -val intro_pattern_to : evars_flag -> Id.t move_location -> delayed_open_constr intro_pattern_expr -> +val intro_pattern_to : evars_flag -> Id.t Logic.move_location -> delayed_open_constr intro_pattern_expr -> unit Proofview.tactic (** Implements user-level "intros", with [] standing for "**" *) @@ -188,7 +192,7 @@ val apply_clear_request : clear_flag -> bool -> constr -> unit Proofview.tactic val specialize : constr with_bindings -> intro_pattern option -> unit Proofview.tactic -val move_hyp : Id.t -> Id.t move_location -> unit Proofview.tactic +val move_hyp : Id.t -> Id.t Logic.move_location -> unit Proofview.tactic val rename_hyp : (Id.t * Id.t) list -> unit Proofview.tactic val revert : Id.t list -> unit Proofview.tactic @@ -405,6 +409,11 @@ val generalize_dep : ?with_let:bool (** Don't lose let bindings *) -> constr - (** {6 Other tactics. } *) +(** Syntactic equality up to universes. With [strict] the universe + constraints must be already true to succeed, without [strict] they + are added to the evar map. *) +val constr_eq : strict:bool -> constr -> constr -> unit Proofview.tactic + val unify : ?state:Names.transparent_state -> constr -> constr -> unit Proofview.tactic val cache_term_by_tactic_then : opaque:bool -> ?goal_type:(constr option) -> Id.t -> Decl_kinds.goal_kind -> unit Proofview.tactic -> (constr -> constr list -> unit Proofview.tactic) -> unit Proofview.tactic |