diff options
| author | herbelin | 2011-10-01 09:12:13 +0000 |
|---|---|---|
| committer | herbelin | 2011-10-01 09:12:13 +0000 |
| commit | 128c28511d62d60c203c16680fd8f7828bcdc6e1 (patch) | |
| tree | f5f55cc860806b4748da287f2a38779bee71f2d1 /kernel/term.mli | |
| parent | 8ce32469bc02e2ecf3f1dfee56f960f19412de9b (diff) | |
Moving never-used comments from Zhints.v to dev/doc so as not to
obfuscate the standard library.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14505 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/term.mli')
0 files changed, 0 insertions, 0 deletions