aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/typing.ml
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2018-06-17 11:17:31 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2018-06-17 11:17:31 +0200
commitd62354b7e9ff8e20aa959984b392a27e26f9fc24 (patch)
tree913a9153fd13b328dbba08e4b8b01838fef3c430 /pretyping/typing.ml
parentdfbfa6abc74199d88747430bdfc78f6ebda09dcb (diff)
parent2369b095a38f08e7c28e8a5dc2591476986e89c0 (diff)
Merge PR #7749: [doc] Disable smartquotes conversion
Diffstat (limited to 'pretyping/typing.ml')
0 files changed, 0 insertions, 0 deletions