Here's a random idea for a fun (but certainly not critical nor particularly F*-specific) feature: In my current code, I have a number of inductive types with a long list of possible constructors. When I later write a match statement for such a type, I have to type in all of the possible constructors (and arguments). Knowing very little about how emacs extensions are written, I imagine it could be possible to have such match statements populated automatically, or even interactively (in case I only want to handle a few cases explicitly).
Here's a random idea for a fun (but certainly not critical nor particularly F*-specific) feature: In my current code, I have a number of inductive types with a long list of possible constructors. When I later write a match statement for such a type, I have to type in all of the possible constructors (and arguments). Knowing very little about how emacs extensions are written, I imagine it could be possible to have such match statements populated automatically, or even interactively (in case I only want to handle a few cases explicitly).