search

affeldt-aist / coq2html

An HTML documentation generator for Coq source files
GNU General Public License v2.0
1 stars 3 forks source link

Notation after closing parenthesis #42

Open yoshihiro503 opened 5 months ago

yoshihiro503 commented 5 months ago

For example, in the following code, the second -> is not correctly linked.

Definition ty := (bool -> nat) -> unit.

This is because the location of the glob file starts two places off from the actual -> location and points to the ) -> part. 

R29:33 Coq.Init.Logic <> ::type_scope:x_'->'_x not
proux01 commented 5 months ago

If this is a bug in Coq when it generates glob files, it should be reported upstream. Or even better, open a pull request there with a fix (look for dump_glob to find out where glob files get generated).