coq - The formal proof system

Age	Commit message (Collapse)	Author
2016-09-07	micromega : more robust generation of proof terms	Frédéric Besson
	- 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)
2016-08-31	Fix Bug #5005 : micromega tactics is now robust to failure of 'abstract'.	Frédéric Besson
	If 'abstract' fails e.g. if there are existentials. The tactic runs an abstract-free alternative.
2016-08-30	plugin micromega : nra also handles non-linear rational arithmetic over Q ↵	Frédéric Besson
	(Fixed #4985) Lqa.v defines the tactics lra and nra working over Q. Lra.v defines the tactics lra and nra working over R.