diff options
| -rw-r--r-- | tools/coq_tex.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/tools/coq_tex.ml b/tools/coq_tex.ml index e2d66b4ab..78cd801a4 100644 --- a/tools/coq_tex.ml +++ b/tools/coq_tex.ml @@ -171,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; + 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 ("Coq < " ^ s); + 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; |