diff options
| author |  Enrico Tassi <gareuselesinge@debian.org> | 2016-12-27 16:53:30 +0100 |
|---|---|---|
| committer | Enrico Tassi <gareuselesinge@debian.org> | 2016-12-27 16:53:30 +0100 |
| commit | a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 (patch) | |
| tree | 26dd9c4aa142597ee09c887ef161d5f0fa5077b6 /tools/coqdoc/output.ml | |
| parent | 164c6861860e6b52818c031f901ffeff91fca16a (diff) | |
Imported Upstream version 8.6upstream/8.6
Diffstat (limited to 'tools/coqdoc/output.ml')
| -rw-r--r-- | tools/coqdoc/output.ml | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml index 2b269096..82d3d62b 100644 --- a/tools/coqdoc/output.ml +++ b/tools/coqdoc/output.ml @@ -953,7 +953,7 @@ module TeXmacs = struct (*s Latex preamble *) - let (preamble : string Queue.t) = + let (_ : string Queue.t) = in_doc := false; Queue.create () let header () = @@ -1122,7 +1122,6 @@ module Raw = struct for i = 0 to String.length s - 1 do char s.[i] done let start_module () = () - let end_module () = () let start_latex_math () = () let stop_latex_math () = () |