input from coqdoc fails to handle coqdoc-comments in the middle of tactics #19
Description
Original report by Jason Gross (Bitbucket: jasongross9, ).
The coqdoc reader seems to assume that a coqdoc comment automatically terminates a statement. This is not always the case, as
#!coq
Ltac foo := (** do x *) x.
is valid. This will break the rest of the file, as [foo] will not be defined for subsequent commands.