aboutsummaryrefslogtreecommitdiffhomepage
path: root/printing
diff options
context:
space:
mode:
authorGravatar Pierre Letouzey <pierre.letouzey@inria.fr>2017-06-13 12:04:34 +0200
committerGravatar Pierre Letouzey <pierre.letouzey@inria.fr>2017-06-14 12:02:35 +0200
commit930662915d75af750db7da1043f9feda321095b3 (patch)
tree7fd1e2430e6effc06d9c591d1276cdb2cff3d2c2 /printing
parenta4faac6d24d28ae49ff38477f92f85aef6759075 (diff)
Recdef do now a Require Export FunInd (better compat)
Diffstat (limited to 'printing')
0 files changed, 0 insertions, 0 deletions