Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Adding a bit of documentation in the mli. | Pierre-Marie Pédrot | 2016-06-09 |
| | |||
* | Update copyright headers. | Maxime Dénès | 2016-01-20 |
| | |||
* | Proof using: let-in policy, optional auto-clear, forward closure* | Enrico Tassi | 2015-10-08 |
| | | | | | | | | | | | | | - "Proof using p*" means: use p and any section var about p. - Simplify the grammar/parser for proof using <expression>. - Section variables with a body (let-in) are pulled in automatically since they are safe to be used (add no extra quantification) - automatic clear of "unused" section variables made optional: Set Proof Using Clear Unused. since clearing section hypotheses does not "always work" (e.g. hint databases are not really cleaned) - term_typing: trigger a "suggest proof using" message also for Let theorems. | ||
* | Update headers. | Maxime Dénès | 2015-01-12 |
| | |||
* | Proof using: New vernacular to name sets of section variables | Enrico Tassi | 2014-12-18 |
| | |||
* | Proof_using: new syntax + suggestion | Enrico Tassi | 2014-01-05 |
Proof using can be followed by: - All : all variables - Type : all variables occurring in the type - expr: - (a b .. c) : set - expr + expr : set union - expr - expr : set difference - -expr : set complement (All - expr) Exceptions: - a singleton set can be written without parentheses. This also allows the implementation of named sets sharing the same name space of section hyps ans write - bla - x : where bla is defined as (a b .. x y) elsewhere. - if expr is just a set, then parentheses can be omitted This module also implements some AI to tell the user how he could decorate "Proof" with a "using BLA" clause. Finally, one can Set Default Proof Using "str" to any string that is used whenever the "using ..." part is missing. The coding of this sucks a little since it is the parser that applies the default. |