diff options
| author | Pierre-Marie Pédrot | 2017-08-02 01:59:32 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-08-02 02:00:42 +0200 |
| commit | c96b746b17a37e242fc01103d22fa0b852da84c5 (patch) | |
| tree | 26d9151e9413a68913aec575ba33f5297afe8908 /doc | |
| parent | 087012f8d3e5e31f489e35dce8397b5202c928b6 (diff) | |
Bindings use open constr quotations.
Diffstat (limited to 'doc')
0 files changed, 0 insertions, 0 deletions