Jason Gross

Goal line blinks when the cursor sits over it

2

 Thought you might want to know, and fix it if it's fixable.

company-coq-mode deletes the goals line

5

In emacs 25.2.50.1:  In emacs 24.5.1: 

company-coq is 2x slower than vanilla PG

2

If I go to the end of the line at https://github.com/mit-plv/fiat/blob/13fecc64d7ec3ae4f969f807c73b26d123020abc/src/Parsers/Refinement/IndexedAndAtMostOneNonTerminalReflective.v#L668 and execute `proof-goto-point`, vanilla PG takes 5-6 seconds, while PG + company-coq takes 10-12 seconds. (This is consistent across...

How do I get a unification diff from console emacs?

1

On something like this:  ```coq Unable to unify "wff (flatten_binding_list ?M1499 ?M1500) (smart_interp_flat_map (fun (t : base_type_code) (x : exprf base_type_code op (Tbase t)) => x) ()%expr (fun (A...

Does company-coq leak?

13

I find that company-coq seems to get slower and slower the longer I've had emacs running, to the point where it can be many orders of magnitude slower than vanilla...

Enhancement: inline docs (M-f12) should display implicit status information

4

M-f12 is a great replacement for looking up information about constants. However, I generally want to know which arguments are implicit and which are not, so it'd be useful to...

inline docs (M-f12) do not work for a constant on the last line when there is no newline at the end of the file

1

It instead complains "No newline at end of file"

Feature Request: autoreplacing [intuition]

1

There is the following procedure for speeding up Coq developments and making them more robust to changes which is crying out for automation. I'm not sure if company-coq is the...

Missing completions

9

I'm going to make this issue and add things to it as I find them missing. Do you want to leave this issue open (or something) so there's a single...