aboutsummaryrefslogtreecommitdiff
path: root/plugins/syntax/string_syntax.ml
diff options
context:
space:
mode:
authorherbelin2012-12-04 23:26:25 +0000
committerherbelin2012-12-04 23:26:25 +0000
commit379e5862f0faa8328fe11ffa6a8467503c503bc0 (patch)
tree089554e1d1a3f4f6b13a7ac100e75d2d335b03f2 /plugins/syntax/string_syntax.ml
parente2da4d5758d0167cb621f2b57bb61708a2d6dbe4 (diff)
Fixing a comment.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16020 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/syntax/string_syntax.ml')
0 files changed, 0 insertions, 0 deletions