From 056a969e5d4cd5752bfccf7797ba46c4bcf0b70d Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Mon, 28 Apr 2014 16:04:13 +0200
Subject: Prevent coq_tex from generating curly quotes. (Partial fix for bug
 #2964)

---
 tools/coq_tex.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'tools')

diff --git a/tools/coq_tex.ml b/tools/coq_tex.ml
index c47be6e770..e2d66b4abc 100644
--- a/tools/coq_tex.ml
+++ b/tools/coq_tex.ml
@@ -79,7 +79,7 @@ let expos   = Str.regexp "^"
 
 let tex_escaped s =
   let dollar = "\\$" and  backslash = "\\\\" and expon = "\\^" in
-  let delims = Str.regexp ("[_{}&%#" ^ dollar ^ backslash ^ expon ^"~ <>]") in
+  let delims = Str.regexp ("[_{}&%#" ^ dollar ^ backslash ^ expon ^"~ <>']") in
   let adapt_delim = function
     | "_" | "{" | "}" | "&" | "%" | "#" | "$" as c -> "\\"^c
     | "\\" -> "{\\char'134}"
@@ -88,6 +88,7 @@ let tex_escaped s =
     | " " -> "~"
     | "<" -> "{<}"
     | ">" -> "{>}"
+    | "'" -> "{\\textquotesingle}"
     | _ -> assert false
   in
   let adapt = function
-- 
cgit v1.2.3