aboutsummaryrefslogtreecommitdiff
path: root/plugins/syntax/string_notation.ml
diff options
context:
space:
mode:
authorErik Martin-Dorel2019-04-25 15:12:42 +0200
committerErik Martin-Dorel2019-04-25 15:12:42 +0200
commit05adb6e2574fa4851f6dfbcc5aa7c73254049e5c (patch)
tree8182eb25298a4a7fba35db0ea775816ea27653cf /plugins/syntax/string_notation.ml
parent47f202605b4ef1795a31312b3ff2eda006fa46a6 (diff)
Add a typing colon in the output of the Search ssreflect vernacular
See also PR math-comp/math-comp#73
Diffstat (limited to 'plugins/syntax/string_notation.ml')
0 files changed, 0 insertions, 0 deletions