diff options
| author | bertot | 2004-01-22 11:19:01 +0000 |
|---|---|---|
| committer | bertot | 2004-01-22 11:19:01 +0000 |
| commit | aa9fb2fb35ee0b1a409a72135ba60086bef625bd (patch) | |
| tree | 9c63d87b0bba832c372ce5faa8f623d4c305d97b /dev | |
| parent | 1746785fc4efcbee56d5561e8e878a6455746bad (diff) | |
adds the notations in inductive definitions, improves the consistency between
induction et destruct, takes the extra argument for fail and idtac into
account
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5233 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions