Gabriel Scherer issues

Repositories
Issues
Comments

Results 172 issues of


                                            Gabriel Scherer

the `extensionality` tactic (added in 8.7) is undocumented

#### Version I'm looking at the [reman 8.8.2 tactic index](https://coq.inria.fr/distrib/V8.8.2/refman/coq-tacindex.html). #### Description of the problem The `extensionality` tactic, added in 8.7 (according to CHANGES) is undocumented.

kind: documentation

API: long lists of `document` arguments are hard to guess from type output

I often rely on type feedback from my editor to navigate APIs. For `PPrint` this does not work well, due to the large number of combinators that take a long...