Prevent Latex from messing with backticks. (Fix for bug #3871)

1 files changed, 2 insertions, 1 deletions

diff --git a/tools/coq_tex.ml b/tools/coq_tex.ml
index 383a68df87..a2cc8384c6 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}"
@@ -89,6 +89,7 @@ let tex_escaped s =
     | "<" -> "{<}"
     | ">" -> "{>}"
     | "'" -> "{\\textquotesingle}"
+    | "`" -> "\\`{}"
     | _ -> assert false
   in
   let adapt = function