aboutsummaryrefslogtreecommitdiff
path: root/kernel/type_errors.ml
diff options
context:
space:
mode:
authorHugo Herbelin2017-08-11 06:06:54 +0200
committerHugo Herbelin2018-02-20 10:03:03 +0100
commit7ef99814a02a0eb7c37dd28fb9ce603e70501745 (patch)
tree907e369c7f2a3cc98f3174636559ae48e695648b /kernel/type_errors.ml
parent9324dcf528f16be420b08c376a6580c8987f50fd (diff)
Minor clarifying of name variables in constrintern.ml.
- renaming lvar into ntnvars when relevant, for consistency - renaming sometimes genv into env (intern_env) so as to remain consistent with other parts of the code
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions