diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-06-17 11:17:31 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-06-17 11:17:31 +0200 |
| commit | d62354b7e9ff8e20aa959984b392a27e26f9fc24 (patch) | |
| tree | 913a9153fd13b328dbba08e4b8b01838fef3c430 /pretyping/indrec.mli | |
| parent | dfbfa6abc74199d88747430bdfc78f6ebda09dcb (diff) | |
| parent | 2369b095a38f08e7c28e8a5dc2591476986e89c0 (diff) | |
Merge PR #7749: [doc] Disable smartquotes conversion
Diffstat (limited to 'pretyping/indrec.mli')
0 files changed, 0 insertions, 0 deletions