coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Update headers following #6543.	Théo Zimmermann	2018-02-27
\|
*	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
\|
*	micromega : more robust generation of proof terms	Frédéric Besson	2016-09-07
\| \| \| \| \| \| \|	- Assert a purely arihtmetic sub-goal that is proved independently by reflexion. (This reduces the stress on the conversion test) - Does not use 'abstract' anymore (more natural proof-term) - Fix a parsing bug (certain terms in Prop where not recognized)
*	Fix Bug #5005 : micromega tactics is now robust to failure of 'abstract'.	Frédéric Besson	2016-08-31
\| \| \| \|	If 'abstract' fails e.g. if there are existentials. The tactic runs an abstract-free alternative.
*	plugin micromega : nra also handles non-linear rational arithmetic over Q ↵	Frédéric Besson	2016-08-30
	(Fixed #4985) Lqa.v defines the tactics lra and nra working over Q. Lra.v defines the tactics lra and nra working over R.