diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-12-08 20:44:56 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-12-08 20:44:56 +0000 |
| commit | ae276492f8749f4d1b2c938e976832ed3eaad986 (patch) | |
| tree | bde69c93bc55676ee599424d350b0be3bac9f911 /library/globnames.mli | |
| parent | 13f7729f5d448bcb8aecf21c8fad7a7506a0cf2a (diff) | |
Coqide: use labels for all labelled functions
This isn't mandatory, but it's a good practice.
For instance it allows to easily locate all ~callback arguments.
Cf. warning 6 of OCaml 4
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16051 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library/globnames.mli')
0 files changed, 0 insertions, 0 deletions