diff options
| author | Guillaume Melquiond | 2015-07-28 15:55:49 +0200 |
|---|---|---|
| committer | Guillaume Melquiond | 2015-07-28 15:56:15 +0200 |
| commit | c544167584024513648b23052db1aa9dcd993c01 (patch) | |
| tree | 76d0b2f1ad2bf93db6c8eb4ae82bc1c27e827218 /tools/coq_tex.ml | |
| parent | d0ec5640994fefe6674c5abb6f7c7001305073cd (diff) | |
Make coq-tex aware of lines ending with "}", so as to fix the FAQ.
This is only a heuristic and it might cause the tool to become awfully
confused if a line ends with "}" yet this is not the end of a tactic
block. Fixing it would require a full-blown Coq parser inside coq-tex.
Example of crazy output:
Coq < Goal { True }
Coq < 1 subgoal
============================
{True} + {False}
Coq < + { False }.
Diffstat (limited to 'tools/coq_tex.ml')
| -rw-r--r-- | tools/coq_tex.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tools/coq_tex.ml b/tools/coq_tex.ml index 7f2fe741e9..fc652f584c 100644 --- a/tools/coq_tex.ml +++ b/tools/coq_tex.ml @@ -68,7 +68,7 @@ let begin_coq_example = let begin_coq_eval = Str.regexp "\\\\begin{coq_eval}[ \t]*$" let end_coq_example = Str.regexp "\\\\end{coq_\\(example\\|example\\*\\|example\\#\\)}[ \t]*$" let end_coq_eval = Str.regexp "\\\\end{coq_eval}[ \t]*$" -let dot_end_line = Str.regexp "\\.[ \t]*\\((\\*.*\\*)\\)?[ \t]*$" +let dot_end_line = Str.regexp "\\(\\.\\|}\\)[ \t]*\\((\\*.*\\*)\\)?[ \t]*$" let has_match r s = try let _ = Str.search_forward r s 0 in true with Not_found -> false |