search

cpitclaudel / company-coq

A Coq IDE build on top of Proof General's Coq mode
GNU General Public License v3.0
353 stars 29 forks source link

[M-RET] Add support for "Inductive" #12

Closed Malabarba closed 9 years ago

Malabarba commented 9 years ago

First of all, thanks for this great extension.

Secondly, it would be great if company-coq-insert-match-rule-simple also worked on other situations that are similar to (but not the same as) match rules.

For instance hitting M-RET at the end of the following

Inductive day : Type :=
| monday : day

Could yield the following

Inductive day : Type :=
| monday : day
| _ :
cpitclaudel commented 9 years ago

Thanks for the nice comments! M-RET and M-S-RET can actually take a C-u prefix argument to insert inductive constructors; my reasoning for moving them to C-u was mostly that inductive constructors are not written as often as match cases.

I wonder if there are other situations in which M-RET would be needed, in which case a context aware version of insert-match-rule would be in order (but navigating Coq's syntax is tricky :/)

Malabarba commented 9 years ago

Oh, I wasn't aware of the prefix argument. That should do for now. :) I've only just started learnig, but I can imagine how complicated coq syntax can be.

cpitclaudel commented 9 years ago

Great; I'll close this then. Also: I'm a big fan of Endless Parentheses, so if you find things to improve in company-coq, feel free to share feature requests or patches; I'll be happy to look at them :)

Malabarba commented 9 years ago

Sure. If I end up using coq a lot, I'm sure I'll find something to PR. In the least, I'll probably mention this package on the blog over the next couple of weeks.

Cheers