diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-02-14 06:57:40 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-03-09 23:23:40 +0100 |
| commit | 4af41a12a0e7e6b17d25a71568641bd03d5e1f94 (patch) | |
| tree | 9ffa30a21f0d5b80aaeae66955e652f185929498 /tactics/tactics.mli | |
| parent | 5f989f48eaaf5e13568fce9849f40bc554ca0166 (diff) | |
[located] More work towards using CAst.t
We continue with the work of #402 and #6745 and update most of the
remaining parts of the AST:
- module declarations
- intro patterns
- top-level sentences
Now, parsed documents should be full annotated by `CAst` nodes.
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. } *) |