coq - the Coq proof assistant

	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.