-
Notifications
You must be signed in to change notification settings - Fork 28
Issues: cpitclaudel/company-coq
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Author
Label
Projects
Milestones
Assignee
Sort
Issues list
definitions with #[local]/#[global] attributes are not shown in outline
#266
opened Mar 27, 2024 by
vzaliva
Requesting support for .vos (in addition to .vio) files
#260
opened May 30, 2022 by
yoichi-at-bedrock
Improve (company-coq-occur) to cope with non-one-liner statements?
#259
opened Apr 5, 2022 by
erikmd
feature wish: highlight the corresponding hyp in the goals buffer when completing.
#249
opened Jun 16, 2021 by
Matafou
Is there a way to have unicode characters working like idents?
#230
opened Jan 23, 2020 by
beta-ziliani
"Definition came from this buffer, but precise location is unknown."
#223
opened Aug 28, 2019 by
vzaliva
company-coq-diff-unification-error: Stack overflow in regexp matcher
#222
opened Jul 23, 2019 by
vzaliva
Notation in the
where
part of an Inductive
command is not prettified.
#209
opened Oct 29, 2018 by
Lysxia
Previous Next
ProTip!
Adding no:label will show everything without a label.