coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Removing auto from the tactic AST.	Pierre-Marie Pédrot	2015-12-24
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-12-17
\|\
\| *	Proof using: do not clear unused section hyps automatically	Enrico Tassi	2015-12-15
\| *	Refine tactic now shelves unifiable holes.	Pierre-Marie Pédrot	2015-12-15
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-12-15
\|\\|
\| *	Moved proof_admitted to its own file, named "AdmitAxiom.v".	Maxime Dénès	2015-12-14
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-12-11
\|\\|
\| *	Changing syntax of pat/constr1.../constrn into pat%constr1...%constrn.	Hugo Herbelin	2015-12-10
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-12-08
\|\\|
\| *	Fix some typos.	Guillaume Melquiond	2015-12-07
* \|	Fix to previous commit (ClassicalFacts.v).	Hugo Herbelin	2015-12-05
* \|	Adding proofs on the relation between excluded-middle and minimization.	Hugo Herbelin	2015-12-05
* \|	Experimenting removing strong normalization of the mid-statement in tactic cut.	Hugo Herbelin	2015-12-05
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-11-29
\|\\|
\| *	Univs: entirely disallow instantiation of polymorphic constants with	Matthieu Sozeau	2015-11-27
* \|	Updating Compat85.v after bd1c97653 on bracketing last or-and	Hugo Herbelin	2015-11-10
* \|	Adding an amazing property of Prop.	Hugo Herbelin	2015-11-07
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-11-05
\|\\|
\| *	Update compatibility file for some of bug #4392	Jason Gross	2015-11-03
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-15
\|\\|
\| *	Fix some typos.	Guillaume Melquiond	2015-10-14
\| *	Fix some typos.	Guillaume Melquiond	2015-10-13
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-09
\|\\|
\| *	Remove the "exists" overrides from Program. (Fix bug #4360)	Guillaume Melquiond	2015-10-07
\| *	Univs: add Strict Universe Declaration option (on by default)	Matthieu Sozeau	2015-10-07
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-02
\|\\|
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-02
\|\ \
\| \| *	Remove Print Universe directive.	Matthieu Sozeau	2015-10-02
\| \| *	Universes: enforce Set <= i for all Type occurrences.	Matthieu Sozeau	2015-10-02
\| \|/
\| *	Add compatibility files (feature 4319)	Jason Gross	2015-09-30
* \|	Merge remote-tracking branch 'origin/v8.5' into trunk	Hugo Herbelin	2015-09-09
\|\\|
\| *	Emphasizing that eta for vectors is an instance of caseS, as pointed	Hugo Herbelin	2015-09-08
\| *	Minor modifications to WeakFanTheorem.	Hugo Herbelin	2015-09-08
\| *	Adding a proof of eta on Vector.t of non-zero size.	Hugo Herbelin	2015-09-08
* \|	Adding a proof of surjective pairing on vectors.	Hugo Herbelin	2015-08-29
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-08-05
\|\\|
\| *	Reverting 16 last commits, committed mistakenly using the wrong push command.	Hugo Herbelin	2015-08-02
\| *	Adding a notation { x & P } for { x : _ & P }.	Hugo Herbelin	2015-08-02
\| *	Remove some outdated files and fix permissions.	Guillaume Melquiond	2015-07-31
* \|	Merge remote-tracking branch 'forge/v8.5'	Pierre Boutillier	2015-06-22
\|\\|
\| *	The "on_last_hyp" tactic now behaves as it should.	Cyprien Mangin	2015-06-12
* \|	Merge v8.5 into trunk	Hugo Herbelin	2015-05-15
\|\\|
\| *	List.nth_error directly produces Some/None instead of value/error	Pierre Letouzey	2015-05-12
\| *	Mark PreOrder as a consequence of Equivalence. (Fix bug #4213)	Guillaume Melquiond	2015-05-12
* \|	Tentatively setting cons and Some with 1st implicit argument maximal	Hugo Herbelin	2015-05-09
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-05-05
\|\\|
\| *	Giving to "subst" a more natural semantic (fixing #4214) by using all	Hugo Herbelin	2015-05-01
* \|	Merge branch 'v8.5' into trunk	Pierre Letouzey	2015-04-09
\|\\|
\| *	Prove [map_ext] using [map_ext_in].	Nickolai Zeldovich	2015-04-09
\| *	Add a [map_ext_in] lemma to List.v.	Nickolai Zeldovich	2015-04-09