coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-06-28
\|\
\| *	Fix bug #4254 with the help of J.H. Jourdan	Matthieu Sozeau	2015-06-26
* \|	Merge remote-tracking branch 'forge/v8.5'	Pierre Boutillier	2015-06-22
\|\\|
\| *	Add test-suite file for bug #3446.	Matthieu Sozeau	2015-06-11
\| *	Adding a test for bug #4057.	Pierre-Marie Pédrot	2015-06-02
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-06-01
\|\\|
\| *	Test for bug #4116.	Pierre-Marie Pédrot	2015-05-19
\| *	Removing test for opened bugs that were already present in the closed test-su...	Pierre-Marie Pédrot	2015-05-18
\| *	Tentative fix for #3461: Anomaly: Uncaught exception Pretype_errors.PretypeEr...	Pierre-Marie Pédrot	2015-05-18
* \|	Removing option -no-native-compiler from test #3539 since this option is now	Hugo Herbelin	2015-05-18
\| *	Removing option -no-native-compiler from test #3539 since this option is now	Hugo Herbelin	2015-05-15
* \|	Merge v8.5 into trunk	Hugo Herbelin	2015-05-15
\|\\|
* \|	#3953 now closed.	Hugo Herbelin	2015-05-14
\| *	Fixing bug #4216:	Pierre-Marie Pédrot	2015-05-13
\| *	Better fixing #4198 such that the term to match is looked for before	Hugo Herbelin	2015-05-13
\| *	Test for bug #4234.	Pierre-Marie Pédrot	2015-05-12
\| *	Test for bug #4232.	Pierre-Marie Pédrot	2015-05-11
\| *	Adjusting test-suite after 5cbc018fe9347 (subst as in 8.4 by default).	Hugo Herbelin	2015-05-09
\| *	Adding a flag "Set Regular Subst Tactic" off by default in v8.5 for	Hugo Herbelin	2015-05-09
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-05-05
\|\\|
\| *	Fixing computation of implicit arguments by position in fixpoints (#4217).	Hugo Herbelin	2015-05-01
\| *	Giving to "subst" a more natural semantic (fixing #4214) by using all	Hugo Herbelin	2015-05-01
\| *	Tactical `progress` compares term up to potentially equalisable universes.	Arnaud Spiwack	2015-04-22
\| *	Test for #4198 (appcontext in return clause of match).	Hugo Herbelin	2015-04-22
\| *	Fixing #3376 and #4191 (wrong index of maximally-inserted implicit argument	Hugo Herbelin	2015-04-21
\| *	Extra fix to 934761875 and f4ee7ee31e4 on optimizing Import of several	Hugo Herbelin	2015-04-17
\| *	Test for bug #4190.	Pierre-Marie Pédrot	2015-04-16
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-04-15
\|\\|
\| *	Test for bug #3199.	Pierre-Marie Pédrot	2015-04-10
\| *	Better test-suite files, removing reliance on admit.	Matthieu Sozeau	2015-04-09
\| *	Fix declarations of instances to perform restriction of universe	Matthieu Sozeau	2015-04-09
\| *	Add test-suite file for bug #4120.	Matthieu Sozeau	2015-04-09
* \|	Merge branch 'v8.5' into trunk	Pierre Letouzey	2015-04-09
\|\\|
\| *	Test for bug #3815.	Pierre-Marie Pédrot	2015-04-06
\| *	Fixing test-suite.	Pierre-Marie Pédrot	2015-03-31
* \|	Merge branch 'v8.5' into trunk	Enrico Tassi	2015-03-30
\|\\|
\| *	Adding test for bug #4165.	Pierre-Marie Pédrot	2015-03-29
\| *	Updating test-suite (see previous commit).	Hugo Herbelin	2015-03-24
\| *	Fixing computation of non-recursively uniform arguments in the	Hugo Herbelin	2015-03-24
* \|	Merge branch 'v8.5' into trunk	Arnaud Spiwack	2015-03-13
\|\\|
\| *	Fix regression in HoTT_coq_014.v	Enrico Tassi	2015-03-11
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-03-11
\|\\|
\| *	admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032)	Enrico Tassi	2015-03-11
\| *	Test for bug #2951.	Pierre-Marie Pédrot	2015-03-08
\| *	Test for #4035 (dependent destruction from Ltac).	Hugo Herbelin	2015-03-07
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-03-04
\|\\|
\| *	Fix test-suite file, this is open.	Matthieu Sozeau	2015-03-03
\| *	Fix bug #3732: firstorder was using detyping to build existential	Matthieu Sozeau	2015-03-03
\| *	Add missing test-suite files and update gitignore.	Matthieu Sozeau	2015-03-03
\| *	Fix test-suite file, this is currently a wontfix, but keep the	Matthieu Sozeau	2015-03-03