diff options
| author | herbelin | 2009-01-02 12:22:09 +0000 |
|---|---|---|
| committer | herbelin | 2009-01-02 12:22:09 +0000 |
| commit | a3b9f0dda44975a0e5e757d35d7870595a4f4460 (patch) | |
| tree | 4c84c31c73037501bb645febd3d31166d318ee27 /doc/tutorial | |
| parent | a2aa673e87859464be0ae57841b1313701dbe912 (diff) | |
- Temptative change to notations like "as [|n H]_eqn" or "as [|n H]_eqn:H",
and, with a now generic intropattern "[]", also "as []_eqn", "as []_eqn:H"
for "destruct" with equality keeping.
- Fixed an accuracy loss in error location.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11732 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'doc/tutorial')
0 files changed, 0 insertions, 0 deletions