Imported Upstream version 8.5~beta1+dfsg

1 files changed, 11 insertions, 9 deletions

diff --git a/tools/coq_tex.ml b/tools/coq_tex.ml
index ca21f706..383a68df 100644
--- a/tools/coq_tex.ml
+++ b/tools/coq_tex.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -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
@@ -116,7 +117,7 @@ let insert texfile coq_output result =
   let next_block k =
     if !last_read = "" then last_read := input_line c_coq;
     (* skip k prompts *)
-    for i = 1 to k do
+    for _i = 1 to k do
       last_read := remove_prompt !last_read;
     done;
     (* read and return the following lines until a prompt is found *)
@@ -170,9 +171,10 @@ let insert texfile coq_output result =
     if Str.string_match end_coq_example s 0 then begin
       just_after ()
     end else begin
-      if !verbose then Printf.printf "Coq < %s\n" s;
-      if (not first_block) & k=0 then output_string c_out "\\medskip\n";
-      if show_questions then encapsule false c_out ("Coq < " ^ s);
+      let prompt = if k = 0 then "Coq < " else "      " in
+      if !verbose then Printf.printf "%s%s\n" prompt s;
+      if (not first_block) && k=0 then output_string c_out "\\medskip\n";
+      if show_questions then encapsule false c_out (prompt ^ s);
       if has_match dot_end_line s then begin
 	let bl = next_block (succ k) in
 	if !verbose then List.iter print_endline bl;
@@ -209,7 +211,7 @@ let insert texfile coq_output result =
 
 (* Process of one TeX file *)
 
-let rm f = try Sys.remove f with _ -> ()
+let rm f = try Sys.remove f with any -> ()
 
 let one_file texfile =
   let inputv = Filename.temp_file "coq_tex" ".v" in
@@ -233,9 +235,9 @@ let one_file texfile =
     insert texfile coq_output result;
     (* 4. clean up *)
     rm inputv; rm coq_output
-  with e -> begin
+  with reraise -> begin
     rm inputv; rm coq_output;
-    raise e
+    raise reraise
   end
 
 (* Parsing of the command line, check of the Coq command and process