diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-09-13 13:24:21 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-09-13 13:24:21 +0000 |
| commit | dce9fe9bd4cab3e560f41a8d7cbf447b27665e1f (patch) | |
| tree | b41dc8ddb21f8dd9511942010864b75b426e6cbc /CHANGES | |
| parent | 01258eb971a3ed22e65a0f9427a870be82f5ceb7 (diff) | |
- Inductive types in the "using" option of auto/eauto/firstorder are
interpreted as using the collection of their constructors as hints.
- Add support for both "using" and "with" in "firstorder". Made the
syntax of "using" compatible with the one of "auto" by separating
lemmas by commas. Did not fully merge the syntax: auto accepts
constr while firstorder accepts names (but are constr really useful?).
- Added "Reserved Infix" as a specific shortcut of the corresponding
"Reserved Notation".
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12325 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'CHANGES')
| -rw-r--r-- | CHANGES | 6 |
1 files changed, 6 insertions, 0 deletions
@@ -32,6 +32,10 @@ Tactics - Tactic "exists" and "eexists" supports iteration using comma-separated arguments. - Tactic "gappa" has been removed from the Dp plugin. +- Tactic "firstorder" now supports the combination of its "using" and + "with" options. +- An inductive type as argument of the "using" option of "auto/eauto/firstorder" + is interpreted as using the collection of its constructors. Tactic Language @@ -45,6 +49,8 @@ Vernacular commands - New support for local binders in the syntax of Record/Structure fields. - Most commands referring to constant (e.g. Print or About) now support referring to the constant by a notation string. +- Added "Reserved Infix" as a specific shortcut of the corresponding + "Reserved Notation". Tools |