diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-04-28 09:41:41 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-04-28 09:41:41 +0200 |
| commit | 8d3c142ec750612b7d02777ff2d6fd5286fb683d (patch) | |
| tree | 881b08216045c3b4088ccd2f094e0b401142880c /tools/coqdoc/output.mli | |
| parent | 9eaf502657ae63f6b184d527eaf1c3b40be90a79 (diff) | |
Fixing coqdoc bug #3292 (unfortunate collision betweens the relative
locations found when parsing expressions in comments and the absolute
locations in the glob file).
As now, the glob file does not parse comment, so I removed the test
for location when parsing expressions in comments, which anyway are
not linkable, precisely because not parsed by coqc.
Diffstat (limited to 'tools/coqdoc/output.mli')
| -rw-r--r-- | tools/coqdoc/output.mli | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/tools/coqdoc/output.mli b/tools/coqdoc/output.mli index 80f390110..e7fc6a029 100644 --- a/tools/coqdoc/output.mli +++ b/tools/coqdoc/output.mli @@ -61,8 +61,9 @@ val rule : unit -> unit val nbsp : unit -> unit val char : char -> unit val keyword : string -> loc -> unit -val ident : string -> loc -> unit +val ident : string -> loc option -> unit val sublexer : char -> loc -> unit +val sublexer_in_doc : char -> unit val initialize : unit -> unit val proofbox : unit -> unit |