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.
*	Micromega: qualify Coq.micromega.Tauto (avoid coqdep warnings about new ↵	Pierre Letouzey	2016-05-19
\| \| \| \|	Init/Tauto.v)
*	Update copyright headers.	Maxime Dénès	2016-01-20
\|
*	Update headers.	Maxime Dénès	2015-01-12
\|
*	micromega : vm_compute; reflexivity -> vm_cast_no_check (eq_refl true)	Frédéric Besson	2014-08-01
\| \| \| \|	* Thanks to G. Melquiond for pointing out that 'abstract' already performs type-checking
*	micromega : improve efficiency/termination of type-checking	Frédéric Besson	2014-08-01
\| \| \| \| \|	* unused terms are generalised * proof is abstract
*	micromega: removal of spurious Export; addition of Lia.v encapsulating lia ↵	Frédéric Besson	2013-12-20
	and nia.