Proof using: let-in policy, optional auto-clear, forward closure*

- "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.

0 files changed, 0 insertions, 0 deletions