Jason Gross

 It thought my `E` was a module, not a scope. I'm not sure if there's a nice way to fix this, though.

Clicking "fully qualify module names (no confirmation)" does not retract the buffer

1

Perhaps this is the desired behavior (that it just in-place edits without undoing other work), but if you do this on the last line, you can get PG to race...

`Parameter Inline` is not a completion option

1

(See 3 of https://coq.inria.fr/refman/Reference-Manual004.html#hevea_default104) 

Missing completion for hint databases

2

 You can get the names of hint databases by doing something like `Print Hint id.` (though this might miss databases that only have rewrite hints? I'm not sure)

`Import` has completions for files but not for modules

3


Feature request: don't disable multiword completions after space

17

If I type `Set P`, my completions are all gone. It'd be nice to still have completions for things like `Set Printing Implicit.`

If I have a long list of `Require Import`s, it'd be nice to fully qualify them all at once.

Feature request: fully qualify module names on completion

1

It'd be nice to have an option (enabled by default) which fully qualifies module names on pressing "enter" to insert them.

Suggestions about suggestion ordering

7

- [x] `reflexivity` should come before `refine ` - [x] `constructor` should come before `constructor num` - [ ] `discriminate` (with no arguments, possibly all the variants) should come before...

There is a way to print keywords from coqtop.byte, but not from coqtop / coqc. I cannot seem to run `coqtop.byte`, as I get ``` Fatal error: cannot load shared...