diff options
Diffstat (limited to 'tactics/tactics.mli')
| -rw-r--r-- | tactics/tactics.mli | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 896b33727..f5695ff06 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -126,7 +126,7 @@ val exact_proof : Constrexpr.constr_expr -> tactic type tactic_reduction = env -> evar_map -> constr -> constr -type change_arg = patvar_map -> evar_map -> evar_map * constr +type change_arg = patvar_map -> constr Sigma.run val make_change_arg : constr -> change_arg val reduct_in_hyp : ?check:bool -> tactic_reduction -> hyp_location -> tactic @@ -206,6 +206,8 @@ val apply_delayed_in : (clear_flag * delayed_open_constr_with_bindings located) list -> intro_pattern option -> unit Proofview.tactic +val run_delayed : Environ.env -> evar_map -> 'a delayed_open -> 'a * evar_map + (** {6 Elimination tactics. } *) (* @@ -384,7 +386,8 @@ val letin_pat_tac : (bool * intro_pattern_naming) option -> (** {6 Generalize tactics. } *) val generalize : constr list -> tactic -val generalize_gen : ((occurrences * constr) * Name.t) list -> tactic +val generalize_gen : (constr Locus.with_occurrences * Name.t) list -> tactic + val new_generalize : constr list -> unit Proofview.tactic val new_generalize_gen : ((occurrences * constr) * Name.t) list -> unit Proofview.tactic @@ -416,9 +419,6 @@ 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 @@ -431,7 +431,7 @@ end module New : sig - val refine : ?unsafe:bool -> (Evd.evar_map -> Evd.evar_map*constr) -> unit Proofview.tactic + val refine : ?unsafe:bool -> constr Sigma.run -> unit Proofview.tactic (** [refine ?unsafe c] is [Proofview.Refine.refine ?unsafe c] followed by beta-iota-reduction of the conclusion. *) |