I recently came across the Context vernacular in a Coq development. I gather from context that it is similar to Hypothesis and Variable, but I haven’t actually found any documentation of this command in the reference manual. I am interested in particular in how it differs from those two vernacular commands.
Oops, it turns out I was looking in the wrong section of the manual. Here is the relevant spot in the manual for those wondering the same thing: https://coq.inria.fr/refman/addendum/type-classes.html#sections-and-contexts
Indeed, the documentation is quite out of place: all of this should be documented in the same place, which explains the section mechanism. I just opened an issue about this: https://github.com/coq/coq/issues/9704. If someone wants to take a stab at fixing it, they would be most welcome. We also have another open issue about Context: https://github.com/coq/coq/issues/9393 (Context lacks examples).
BTW, even when things are not documented where there should be, you can quickly locate them by using the indexes. In this case, that would be the command index: https://coq.inria.fr/refman/coq-cmdindex.html.
This thread motivated me to make this PR to the manual (adding a reference to Context under Variable): https://github.com/coq/coq/pull/9789
1 Like