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

Clear current search query, filters, and sorts
95 Open 144 Closed
95 Open 144 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

Inline Docs
#21 opened Aug 12, 2015 by Kethku updated Aug 13, 2015
2
Fields of Inductive/Record/Class not available in completion
#14 opened May 13, 2015 by wilcoxjay updated Dec 22, 2015
2
Feature wish: real-time extraction buffer
#35 opened Dec 23, 2015 by jonleivent updated Dec 27, 2015
26
Folding doesn't work on last line of proof
#40 opened Jan 4, 2016 by cpitclaudel updated Jan 4, 2016
"?" should not count as operator character when followed by alphanumeric
#37 opened Dec 25, 2015 by jonleivent updated Jan 5, 2016
2
Naming hypotheses for lemma extraction enhancement
#64 opened Jan 24, 2016 by nickgian updated Jan 25, 2016
@cpitclaudel
20
visual diff of goals before/after tactic
#29 opened Dec 18, 2015 by jonleivent updated Jan 26, 2016
26
An even better lemma extraction? enhancement question
#68 opened Jan 28, 2016 by Zimmi48 updated Jan 28, 2016
@cpitclaudel
4
Control-Click in Aquamacs
#70 opened Jan 29, 2016 by vzaliva updated Jan 30, 2016
16
Folding eats comments before next definition enhancement help wanted question
#91 opened Feb 24, 2016 by wilcoxjay updated Feb 24, 2016
1
Feature request: fully qualify module names on completion enhancement
#90 opened Feb 23, 2016 by JasonGross updated Feb 29, 2016
1
Feature request: fully qualify all module names at once enhancement
#89 opened Feb 23, 2016 by JasonGross updated Feb 29, 2016
Request: electric bullets enhancement
#82 opened Feb 16, 2016 by jonleivent updated Feb 29, 2016
3
Evaluation of company-coq-tutorial hangs on Require Import Omega. bug
#87 opened Feb 22, 2016 by dredozubov updated Feb 29, 2016
12
folding throws off auto set printing width
#97 opened Mar 6, 2016 by jonleivent updated Mar 6, 2016
Delayed/slow scrolling bug help wanted
#80 opened Feb 13, 2016 by alxest updated Apr 12, 2016
9
Feature request: don't disable multiword completions after space enhancement
#49 opened Jan 13, 2016 by JasonGross updated Apr 25, 2016
17
Import has completions for files but not for modules
#113 opened May 4, 2016 by JasonGross updated May 4, 2016
3
Show Obligation Tactic.
#114 opened May 9, 2016 by vzaliva updated May 10, 2016
1
Feature request: resolve local module aliases in M-.
#116 opened May 11, 2016 by wilcoxjay updated May 11, 2016
1
company-coq slows down pasting from system clipboard bug question
#108 opened Apr 22, 2016 by jstolarek updated May 12, 2016
4
incorrectly colorized "pose proof" within a comment
#100 opened Mar 22, 2016 by jonleivent updated May 12, 2016
1
Missing completion for hint databases enhancement
#115 opened May 10, 2016 by JasonGross updated May 12, 2016
2
Extra newline inserted after autocompletion bug
#106 opened Apr 18, 2016 by jstolarek updated May 12, 2016
3
Parameter Inline is not a completion option
#119 opened Jun 2, 2016 by JasonGross updated Jun 2, 2016
1
ProTip! Exclude everything labeled bug with -label:bug.