diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-08-20 21:01:34 +0200 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-08-20 21:01:34 +0200 |
commit | 69a35378d37b8eb7e1019d24ab5e0fd27f25b6bc (patch) | |
tree | 55a6d17a0de13244a6454263ae3de6bc5b3c2374 /tools/coqdoc | |
parent | 1af95525a2a791889e6d72dfc150ff8f09a21e21 (diff) |
More standard naming for the Imparg.with_implicits function.
Diffstat (limited to 'tools/coqdoc')
0 files changed, 0 insertions, 0 deletions