diff options
| author | Théo Zimmermann | 2017-01-29 18:42:33 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2017-01-29 18:42:33 +0100 |
| commit | e69f8622d1b844f77d14e3ba4db797f7c64e6bed (patch) | |
| tree | df474c2cb991e41ee9a45f1125a15d16c17f180c /dev/base_include | |
| parent | c7a0568967a8a6e40888a2106b9b59325f2f09a5 (diff) | |
Remove outdated comment from 2002.
The comment was arguing against the "Proof proof_term." syntax.
This syntax is still there 15 years later (while the alternative
proposition uses outdated syntax).
Diffstat (limited to 'dev/base_include')
0 files changed, 0 insertions, 0 deletions