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 /ide/coq.lang | |
| 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 'ide/coq.lang')
0 files changed, 0 insertions, 0 deletions