diff options
| author |  bertot <bertot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-01-28 08:32:21 +0000 |
|---|---|---|
| committer | bertot <bertot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-01-28 08:32:21 +0000 |
| commit | 1091a134df7d3af4cacde58b09c230619f7739a0 (patch) | |
| tree | 902b58f6c675a4ad541348f96df0267448b80a9e /library/library.ml | |
| parent | 81c7b237f71d571098371018fc903552768dab2a (diff) | |
make sure that 'in' clauses for reduction tactics are translated
once again re-organize the way intro patterns are translated: there is now
only one kind of pattern that can be used for both and and or constructs:
the use of the multiplet notation should only be a matter of notation.
un-capitalize a few tactic names for tactics represented using the TacExtend
construct.
corrects a bug in the way binders or coercion binders were used.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5260 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library/library.ml')
0 files changed, 0 insertions, 0 deletions