cpitclaudel/company-coq

Issues

• corfu

  #268 opened 11 days ago by jgarte
  0

• "with" word withing comments spills into outline

  #267 opened 8 months ago by vzaliva
  0

• definitions with #[local]/#[global] attributes are not shown in outline

  #266 opened 8 months ago by vzaliva
  0

• jump to definition fails for constructors of Variants

  #253 opened 2 years ago by aa755
  0

• "SPP" for "Set Printing Parentheses" is useful, should be added.

  #262 opened 2 years ago by zhengpushi
  3

• Feedback from Coq Community Survey 2022.

  #258 opened 3 years ago by Zimmi48
  0

• Requesting support for .vos (in addition to .vio) files

  #260 opened 2 years ago by yoichi-at-bedrock
  2

• Improve (company-coq-occur) to cope with non-one-liner statements?

  #259 opened 3 years ago by erikmd
  2

• company-coq-go-to-point fails

  #248 opened 3 years ago by vzaliva
  11

• "Definition came from this buffer, but precise location is unknown."

  #223 opened 5 years ago by vzaliva
  3

• Is there a way to disable the documentation buffer?

  #256 opened 3 years ago by damif94
  7

• Incorrect use of Unicode symbol in error message for Coq

  #255 opened 3 years ago by fblanqui
  1

• Tutorial outdated

  #254 opened 3 years ago by Matafou
  0

• Completion becomes slower over time

  #252 opened 3 years ago by anton0xf
  4

• new hyps not proposed for completion when in diff mode.

  #250 opened 3 years ago by Matafou
  6

• PG init commands not performed when company-coq enabled before coq starts.

  #251 opened 3 years ago by Matafou
  4

• feature wish: highlight the corresponding hyp in the goals buffer when completing.

  #249 opened 3 years ago by Matafou
  0

• New subscript syntax?

  #246 opened 4 years ago by liyishuai
  2

• jump to definition: new window

  #245 opened 4 years ago by aa755
  0

• Compile Before Require not working anymore

  #244 opened 4 years ago by viampietro
  2

• broken Layout when using Tex

  #243 opened 4 years ago by gaxiiiiiiiiiiii
  1

• `M-.` and notations

  #241 opened 4 years ago by vzaliva
  1

• No match when installing this package from MELPA

  #240 opened 4 years ago by PalindromeLeung
  4

• jump to definition in current file fails if no _CoqProject or no -Q

  #238 opened 4 years ago by aa755
  9

• company-coq-lemma-from-goal should be adapted w.r.t. Coq Diffs

  #239 opened 4 years ago by erikmd
  0

• company-coq won't install from melpa

  #237 opened 5 years ago by jonleivent
  5

• Feature Request: Outline mode with TOC

  #236 opened 5 years ago
  3

• company-coq-diff-unification-error: Stack overflow in regexp matcher

  #222 opened 5 years ago by vzaliva
  10

• Feature Request: exclude . and ; from prettified symbols

  #234 opened 5 years ago by soraros
  0

• Is there a way to have unicode characters working like idents?

  #230 opened 5 years ago by beta-ziliani
  5

• Fuzzy selection

  #233 opened 5 years ago by beta-ziliani
  2

• How can I turn off the documentation presentation(the company-coq : documentation buffer) at completion

  #229 opened 5 years ago by shrubbroom
  2

• \square not included?

  #232 opened 5 years ago by beta-ziliani
  5

• Subscript bikeshedding

  #231 opened 5 years ago by Ptival
  1

• `M-.` failure

  #225 opened 5 years ago by vzaliva
  6

• How can i stop auto-completion of points?

  #228 opened 5 years ago by RobertoEnC
  4

• company-coq is overriding my `company-idle-delay` setting

  #227 opened 5 years ago by rgrinberg
  1

• Feature Request: fold pattern matching in Gallina

  #224 opened 5 years ago by liyishuai
  0

• Update Proof General installation procedure ?

  #212 opened 5 years ago by atrieu
  4

• Company-coq shows two doc buffers

  #221 opened 5 years ago by santifa
  1

• symbol prettification and smart subscripts become enabled despite setting upon opening second coq buffer

  #219 opened 6 years ago by ingvar-lynn
  2

• displaying a large-ish hypothesis above the line is much slower than displaying it below the line

  #218 opened 6 years ago by samuelgruetter
  8

• Show Section endings in `company-coq-occur`

  #215 opened 6 years ago by vzaliva
  3

• `M-.` error

  #213 opened 6 years ago by vzaliva
  8

• Disable the feature that adds `(* *)` to a new line when pressing Enter in a comment?

  #211 opened 6 years ago by Ptival
  7

• Notation in the `where` part of an `Inductive` command is not prettified.

  #209 opened 6 years ago by Lysxia
  1

• Newline without auto-indentation

  #206 opened 6 years ago by pseudohuman92
  3

• Where does proof-shell come from?

  #208 opened 6 years ago by tarsius
  2

• Request: Semantic highlighting

  #207 opened 6 years ago by sethomsen
  10

• Loading company-coq prevents PG context menu to appear

  #205 opened 6 years ago by erikmd
  2