diff options
| author |  glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-09-28 15:32:01 +0000 |
|---|---|---|
| committer | glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-09-28 15:32:01 +0000 |
| commit | 86919192359dee7e274ab4af17bd32efe11a5f44 (patch) | |
| tree | d09d9174894559ce1f34b078e3ae163e9e09515d /parsing/pptactic.ml | |
| parent | 013bc34fd828a5eb4eacd721a8021b64abf8a822 (diff) | |
Remove "init" label from Termops.it_mk* specialized functions
These functions are applied much more often without labels than with
them (the alternate of adding the label wherever relevant changes 124
lines instead of 41). Moreover, this is more consistent with the Term
module and there is no ambiguity in argument types. This commit goes
towards elimination of occurrences of OCaml warning 6.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13468 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/pptactic.ml')
0 files changed, 0 insertions, 0 deletions