diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-12-18 07:32:15 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-06-18 13:07:22 +0200 |
| commit | a34c17e0e4600d0c466f19b64c3dfb39376981fd (patch) | |
| tree | 06aeab8a503b8892d2a1fc4d66bd5add15038dd0 /tactics/tactics.mli | |
| parent | 42cbdfccf0c0500935d619dccaa00476690229f8 (diff) | |
Adding eintros to respect the e- prefix policy.
In pat%constr, creating new evars is now allowed only if "eintros" is
given, i.e. "intros" checks that no evars are created, and similarly
e.g. for "injection ... as ... pat%constr".
The form "eintros [...]" or "eintros ->" with the case analysis or
rewrite creating evars is now also supported.
This is not a commitment to say that it is good to have an e- modifier
to tactics. It is just to be consistent with the existing convention.
It seems to me that the "no e-" variants are good for beginners. However,
expert might prefer to use the e-variants by default. Opinions from
teachers and users would be useful.
To be possibly done: do that [= ...] work on hypotheses with side
conditions or parameters based on the idea that they apply the full
injection and not only the restriction of it to goals which are
exactly an equality, as it is today.
Diffstat (limited to 'tactics/tactics.mli')
| -rw-r--r-- | tactics/tactics.mli | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 142fdd3eb..e346a0d56 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -102,16 +102,16 @@ val use_clear_hyp_by_default : unit -> bool (** {6 Introduction tactics with eliminations. } *) -val intro_patterns : intro_patterns -> unit Proofview.tactic -val intro_patterns_to : Id.t move_location -> intro_patterns -> +val intro_patterns : evars_flag -> intro_patterns -> unit Proofview.tactic +val intro_patterns_to : evars_flag -> Id.t move_location -> intro_patterns -> unit Proofview.tactic -val intro_patterns_bound_to : int -> Id.t move_location -> intro_patterns -> +val intro_patterns_bound_to : evars_flag -> int -> Id.t move_location -> intro_patterns -> unit Proofview.tactic -val intro_pattern_to : Id.t move_location -> delayed_open_constr intro_pattern_expr -> +val intro_pattern_to : evars_flag -> Id.t move_location -> delayed_open_constr intro_pattern_expr -> unit Proofview.tactic (** Implements user-level "intros", with [] standing for "**" *) -val intros_patterns : intro_patterns -> unit Proofview.tactic +val intros_patterns : evars_flag -> intro_patterns -> unit Proofview.tactic (** {6 Exact tactics. } *) |