aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2017-09-23 16:18:10 +0200
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2017-09-23 16:23:54 +0200
commit22a3a79f32d5f795143bd808810aba890c630313 (patch)
treeea3cb660d8beafa3aca5cb472a5f876e906f510f /tools
parent2f3cd62d5118efe95330ddc06fdb43ee717ef993 (diff)
Discharge.ml: cosmetic renaming of some variables.
The point is to emphasize stronglier when we are talking about contexts or about arguments.
Diffstat (limited to 'tools')
0 files changed, 0 insertions, 0 deletions