Jason Gross

Sounds good. I'm in my office now and will be until 4.

After in-person debugging with @cpitclaudel, this seems to be related to https://debbugs.gnu.org/cgi/bugreport.cgi?bug=21028.

Oh, I see, this is just `Print`. I was thinking you assembled it yourself, and could do `About id | grep '^Arguments'` or something

If it's not, that's a bug, and it should be. (At the very least, it's in the [commit message for the feature](http://lists.gforge.inria.fr/pipermail/coq-commits/2014-September/013300.html).)

[Bug #4551](https://coq.inria.fr/bugs/show_bug.cgi?id=4551)

The following options exist in the source code (grepping for `optkey`), but not in the tactics index: ``` Asymmetric Patterns Atomic Load Bullet Behavior Compat Notations Congruence Depth Congruence Verbose...

Note that `Scheme Minimality` and `Scheme ident := Equality ...` are not currently literally documented as variants. If it'd be helpful, I can open a bug report or submit a...

New databases can appear on `Require`, `Import`: a `Hint` command with a colon with a name not yet known, and by `Create HintDb`. It might be a fairly cheap call...

None that I know of, but it's probably an easy patch to write (look at `.env_modules.module_path`, I think?).

I think that would take time for my fingers to learn; I tend to acquire these by typing less and less of the keyword as I go along. Is completion...