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

2 files changed, 6 insertions, 5 deletions

diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex
index 3605a716e7..1eb40cd36d 100644
--- a/doc/refman/RefMan-ext.tex
+++ b/doc/refman/RefMan-ext.tex
@@ -1782,14 +1782,14 @@ This is useful for declaring the implicit type of a single variable.
 Implicit generalization is an automatic elaboration of a statement with
 free variables into a closed statement where these variables are
 quantified explicitly. Implicit generalization is done inside binders
-starting with a \verb|`| and terms delimited by \verb|`{ }| and
-\verb|`( )|, always introducing maximally inserted implicit arguments for
+starting with a \texttt{\`{}} and terms delimited by \texttt{\`{}\{ \}} and
+\texttt{\`{}( )}, always introducing maximally inserted implicit arguments for
 the generalized variables. Inside implicit generalization
 delimiters, free variables in the current context are automatically
 quantified using a product or a lambda abstraction to generate a closed
 term. In the following statement for example, the variables \texttt{n}
 and \texttt{m} are automatically generalized and become explicit
-arguments of the lemma as we are using \verb|`( )|:
+arguments of the lemma as we are using \texttt{\`{}( )}:
 
 \begin{coq_example}
 Generalizable All Variables.
@@ -1834,7 +1834,7 @@ Definition id `(x : A) : A := x.
 Print id.
 \end{coq_example}
 
-The generalizing binders \verb|`{ }| and \verb|`( )| work similarly to
+The generalizing binders \texttt{\`{}\{ \}} and \texttt{\`{}( )} work similarly to
 their explicit counterparts, only binding the generalized variables
 implicitly, as maximally-inserted arguments. In these binders, the
 binding name for the bound object is optional, whereas the type is
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