aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Numbers
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2016-04-10 18:31:25 +0200
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2016-06-16 17:30:18 +0200
commite09062253640add21f395f688f927a26cf38106e (patch)
treee5e712a4fc1247ac49898831018d6032105490f1 /theories/Numbers
parente2d4490b12514362af8e1f0b8b89cf0550f78130 (diff)
Being defensive in printing implicit arguments also with manual
implicit arguments when in beautification mode.
Diffstat (limited to 'theories/Numbers')
0 files changed, 0 insertions, 0 deletions