diff options
| author | letouzey | 2005-08-19 19:51:02 +0000 |
|---|---|---|
| committer | letouzey | 2005-08-19 19:51:02 +0000 |
| commit | be6ee173206a929ad664ff507334ad5add7ad157 (patch) | |
| tree | bfc3228af152a38598bc09798c5602d5e5953148 /dev/header | |
| parent | 66a2d880e14c1635f29cef0ad0113185cba29a18 (diff) | |
Sur le conseil de X.Leroy: x=[||] devient Array.length x=0
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7305 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'dev/header')
0 files changed, 0 insertions, 0 deletions