diff options
Diffstat (limited to 'tactics/tactics.mli')
| -rw-r--r-- | tactics/tactics.mli | 9 |
1 files changed, 4 insertions, 5 deletions
diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 1c3b75e91..079baa3ef 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -8,7 +8,6 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -open Loc open Names open Constr open EConstr @@ -196,10 +195,10 @@ val apply : constr -> unit Proofview.tactic val eapply : constr -> unit Proofview.tactic val apply_with_bindings_gen : - advanced_flag -> evars_flag -> (clear_flag * constr with_bindings located) list -> unit Proofview.tactic + advanced_flag -> evars_flag -> (clear_flag * constr with_bindings CAst.t) list -> unit Proofview.tactic val apply_with_delayed_bindings_gen : - advanced_flag -> evars_flag -> (clear_flag * delayed_open_constr_with_bindings located) list -> unit Proofview.tactic + advanced_flag -> evars_flag -> (clear_flag * delayed_open_constr_with_bindings CAst.t) list -> unit Proofview.tactic val apply_with_bindings : constr with_bindings -> unit Proofview.tactic val eapply_with_bindings : constr with_bindings -> unit Proofview.tactic @@ -208,12 +207,12 @@ val cut_and_apply : constr -> unit Proofview.tactic val apply_in : advanced_flag -> evars_flag -> Id.t -> - (clear_flag * constr with_bindings located) list -> + (clear_flag * constr with_bindings CAst.t) list -> intro_pattern option -> unit Proofview.tactic val apply_delayed_in : advanced_flag -> evars_flag -> Id.t -> - (clear_flag * delayed_open_constr_with_bindings located) list -> + (clear_flag * delayed_open_constr_with_bindings CAst.t) list -> intro_pattern option -> unit Proofview.tactic (** {6 Elimination tactics. } *) |