Skip to content

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.

Sign up for GitHub

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

95 Open 145 Closed
95 Open 145 Closed
Author
Filter by author
Loading
Label
Filter by label
Loading
Use alt + click/return to exclude labels
or ⇧ + click/return for logical OR
Projects
Filter by project
Loading
Milestones
Filter by milestone
Loading
Assignee
Filter by who’s assigned
Sort
Sort by
Newest Oldest Most commented Least commented Recently updated Least recently updated Best match
Most reactions
👍 👎 😄 🎉 😕 ❤️ 🚀 👀

Issues list

"with" word withing comments spills into outline
#267 opened Mar 27, 2024 by vzaliva
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
2
Improve (company-coq-occur) to cope with non-one-liner statements?
#259 opened Apr 5, 2022 by erikmd
2
Feedback from Coq Community Survey 2022.
#258 opened Mar 25, 2022 by Zimmi48
Is there a way to disable the documentation buffer?
#256 opened Nov 9, 2021 by damif94
7
Incorrect use of Unicode symbol in error message for Coq
#255 opened Oct 25, 2021 by fblanqui
1
Tutorial outdated
#254 opened Oct 11, 2021 by Matafou
Completion becomes slower over time
#252 opened Jul 13, 2021 by anton0xf
4
new hyps not proposed for completion when in diff mode.
#250 opened Jul 2, 2021 by Matafou
6
feature wish: highlight the corresponding hyp in the goals buffer when completing.
#249 opened Jun 16, 2021 by Matafou
jump to definition: new window
#245 opened Jan 6, 2021 by aa755
Compile Before Require not working anymore
#244 opened Dec 22, 2020 by viampietro
2
company-coq-lemma-from-goal should be adapted w.r.t. Coq Diffs
#239 opened Jun 3, 2020 by erikmd
Feature Request: Outline mode with TOC
#236 opened Apr 23, 2020 by ghost
3
Feature Request: exclude . and ; from prettified symbols
#234 opened Feb 21, 2020 by soraros
Fuzzy selection
#233 opened Feb 1, 2020 by beta-ziliani
2
Subscript bikeshedding
#231 opened Jan 24, 2020 by Ptival
1
Is there a way to have unicode characters working like idents?
#230 opened Jan 23, 2020 by beta-ziliani
5
M-. failure
#225 opened Sep 27, 2019 by vzaliva
1
6
Feature Request: fold pattern matching in Gallina
#224 opened Sep 16, 2019 by liyishuai
"Definition came from this buffer, but precise location is unknown."
#223 opened Aug 28, 2019 by vzaliva
3
company-coq-diff-unification-error: Stack overflow in regexp matcher
#222 opened Jul 23, 2019 by vzaliva
10
Company-coq shows two doc buffers
#221 opened Jun 5, 2019 by santifa
1
Notation in the where part of an Inductive command is not prettified.
#209 opened Oct 29, 2018 by Lysxia
1
ProTip! Add no:assignee to see everything that’s not assigned.