aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools/coqdoc
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-08-20 21:01:34 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-08-20 21:01:34 +0200
commit69a35378d37b8eb7e1019d24ab5e0fd27f25b6bc (patch)
tree55a6d17a0de13244a6454263ae3de6bc5b3c2374 /tools/coqdoc
parent1af95525a2a791889e6d72dfc150ff8f09a21e21 (diff)
More standard naming for the Imparg.with_implicits function.
Diffstat (limited to 'tools/coqdoc')
0 files changed, 0 insertions, 0 deletions