From a9f3607ae72517156301570a4ffa05908609b7e0 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Thu, 30 Jul 2015 08:30:00 +0200
Subject: Fix width of underscore in coq_tex output.

---
 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 8218f84f1f..dbdc2e9db1 100644
--- a/tools/coq_tex.ml
+++ b/tools/coq_tex.ml
@@ -66,7 +66,8 @@ let extract texfile inputv =
 let tex_escaped s =
   let delims = Str.regexp "[_{}&%#$\\^~ <>'`]" in
   let adapt_delim = function
-    | "_" | "{" | "}" | "&" | "%" | "#" | "$" as c -> "\\"^c
+    | "{" | "}" | "&" | "%" | "#" | "$" as c -> "\\"^c
+    | "_" -> "{\\char`\\_}"
     | "\\" -> "{\\char'134}"
     | "^" -> "{\\char'136}"
     | "~" -> "{\\char'176}"
-- 
cgit v1.2.3