diff options
Diffstat (limited to 'tactics/tactics.mli')
| -rw-r--r-- | tactics/tactics.mli | 29 |
1 files changed, 16 insertions, 13 deletions
diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 7809dbf48..8d4302450 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -16,10 +16,8 @@ open Proof_type open Evd open Clenv open Redexpr -open Globnames open Pattern open Unification -open Misctypes open Tactypes open Locus open Ltac_pretype @@ -35,16 +33,16 @@ val is_quantified_hypothesis : Id.t -> Proofview.Goal.t -> bool (** {6 Primitive tactics. } *) -val introduction : ?check:bool -> Id.t -> unit Proofview.tactic +val introduction : Id.t -> unit Proofview.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 mutual_fix : Id.t -> int -> (Id.t * int * constr) list -> int -> unit Proofview.tactic -val fix : Id.t option -> int -> unit Proofview.tactic +val fix : Id.t -> int -> unit Proofview.tactic val mutual_cofix : Id.t -> (Id.t * constr) list -> int -> unit Proofview.tactic -val cofix : Id.t option -> unit Proofview.tactic +val cofix : Id.t -> unit Proofview.tactic val convert : constr -> constr -> unit Proofview.tactic val convert_leq : constr -> constr -> unit Proofview.tactic @@ -57,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] *) @@ -92,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 *) @@ -118,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 "**" *) @@ -177,7 +180,7 @@ val change : val pattern_option : (occurrences * constr) list -> goal_location -> unit Proofview.tactic val reduce : red_expr -> clause -> unit Proofview.tactic -val unfold_constr : global_reference -> unit Proofview.tactic +val unfold_constr : GlobRef.t -> unit Proofview.tactic (** {6 Modification of the local context. } *) @@ -189,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 @@ -253,7 +256,7 @@ val apply_delayed_in : type elim_scheme = { elimc: constr with_bindings option; elimt: types; - indref: global_reference option; + indref: GlobRef.t option; 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,...) *) |