The AST returned by Coq includes a final step with whatever white space and comments are found after the last step in the file. This step is currently being treated as a regular step. However, it is not possible to add steps after it because its range needs to be handled differently. We are not aware of other unexpected behaviours.
Changes should be made to how this step is handled, whether the last step should be ignored (it holds no relevant information) or if we should treat the last step differently where appropriate.
pcarrott
commented
11 months ago
The AST returned by Coq includes a final step with whatever white space and comments are found after the last step in the file. This step is currently being treated as a regular step. However, it is not possible to add steps after it because its range needs to be handled differently. We are not aware of other unexpected behaviours.
Changes should be made to how this step is handled, whether the last step should be ignored (it holds no relevant information) or if we should treat the last step differently where appropriate.