diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-03-02 07:04:56 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-03-02 07:04:56 +0000 |
| commit | 8a1ddc270137f40cd8bbff20de4f41e284055891 (patch) | |
| tree | d3d41549bcd3cff2bbd0db1fb7824e05851941dd /tactics/inv.mli | |
| parent | 1a29faa00f1e2a6f2d71088a769fe2fbc823244a (diff) | |
Generalisation de la syntaxe de 'with_names' pour accepter 'as id' avec id variable de ltac substituable dans la pratique par un intro_case_pattern dans induction, destruct et inversion
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5415 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/inv.mli')
| -rw-r--r-- | tactics/inv.mli | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/tactics/inv.mli b/tactics/inv.mli index 4c3cb00f8..95bf4c6f7 100644 --- a/tactics/inv.mli +++ b/tactics/inv.mli @@ -21,19 +21,19 @@ type inversion_status = Dep of constr option | NoDep val inv_gen : bool -> inversion_kind -> inversion_status -> - case_intro_pattern_expr -> quantified_hypothesis -> tactic + intro_pattern_expr option -> quantified_hypothesis -> tactic val invIn_gen : - inversion_kind -> case_intro_pattern_expr -> identifier list -> + inversion_kind -> intro_pattern_expr option -> identifier list -> quantified_hypothesis -> tactic val inv_clause : - inversion_kind -> case_intro_pattern_expr -> identifier list -> + inversion_kind -> intro_pattern_expr option -> identifier list -> quantified_hypothesis -> tactic -val inv : inversion_kind -> case_intro_pattern_expr -> +val inv : inversion_kind -> intro_pattern_expr option -> quantified_hypothesis -> tactic -val dinv : inversion_kind -> constr option -> case_intro_pattern_expr -> +val dinv : inversion_kind -> constr option -> intro_pattern_expr option -> quantified_hypothesis -> tactic val half_inv_tac : identifier -> tactic |