diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-04-04 14:55:47 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-04-04 14:55:47 +0000 |
| commit | 5a4cc30c737f113a7c57d14569137b3e06f5639f (patch) | |
| tree | 2a0114f494382fc30f50ad073eaf6ec5def2daed /tactics/tactics.mli | |
| parent | c464aab4c1aedad2ae919eb4776ced4d4d23d62a (diff) | |
Quelques améliorations des intro patterns:
- ajout de -> et <- pour substitution immédiate d'une égalité
(comportement à la subst si variable, à la rewrite in * sinon)
- ajout possibilité d'hypothèses avec paramètres
- correction d'un comportement bizarre de l'utilisation des noms dans
cas "[[|] H]" (cf CHANGES)
Ce serait bien d'avoir quelque chose comme "intros (H as <-) (H' as [ | ])"
pour décider de garder les noms, mais la syntaxe est assez
moche. Peut-être un "intros H: <- H': [ | ]" ?
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10753 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/tactics.mli')
| -rw-r--r-- | tactics/tactics.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 084aba9ef..1c64e47e8 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -338,3 +338,6 @@ val tclABSTRACT : identifier option -> tactic -> tactic val admit_as_an_axiom : tactic val abstract_generalize : identifier -> tactic + +val register_general_multi_rewrite : + (bool -> evars_flag -> constr with_ebindings -> clause -> tactic) -> unit |