coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-05-02
\|\
\| *	An example for cd139311e, showing a consequence of not converting	Hugo Herbelin	2016-04-28
* \|	Fixing a "This clause is redundant" error when interpreting the "in"	Hugo Herbelin	2016-04-27
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-04-09
\|\\|
* \|	Fixing printing of Tactic Notations with tactic arguments.	Pierre-Marie Pédrot	2016-04-08
* \|	An example which failed in 8.5 and that d670c6b6 fixes.	Hugo Herbelin	2016-04-07
\| *	Add -compat 8.4 econstructor tactics, and tests	Jason Gross	2016-04-05
* \|	Fixing an incorrect use of prod_appvect on a term which was not a	Hugo Herbelin	2016-03-28
* \|	Test suite file for a bug in BigQ arithmetic fixed a while ago.	Maxime Dénès	2016-03-25
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-03-18
\|\\|
\| *	Fix bug when a sort is ascribed to a Record	Matthieu Sozeau	2016-03-15
* \|	Adopting the same rules for interpreting @, abbreviations and	Hugo Herbelin	2016-03-13
* \|	Adding a file summarizing the inconsistencies in interpreting implicit	Hugo Herbelin	2016-03-13
\| *	Primitive projections: protect kernel from erroneous definitions.	Matthieu Sozeau	2016-03-10
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-03-09
\|\\|
\| *	Fix strategy of Keyed Unification	Matthieu Sozeau	2016-03-09
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-03-05
\|\\|
* \|	Using build_selector from Equality as a replacement of the selector	Hugo Herbelin	2016-03-05
* \|	Making parentheses mandatory in tactic scopes.	Pierre-Marie Pédrot	2016-03-04
\| *	Document differences of Hint Resolve and Hint Extern	Matthieu Sozeau	2016-02-23
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-02-13
\|\\|
\| *	Do not give a name to anonymous evars anymore. See bug #4547.	Pierre-Marie Pédrot	2016-02-13
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-21
\|\\|
* \|	Stronger invariants on the use of the introduction pattern (pat1,...,patn).	Hugo Herbelin	2016-01-21
* \|	Fixing some problems with double induction.	Hugo Herbelin	2016-01-21
* \|	Fixing a bug with introduction patterns over inductive types containing let-ins.	Hugo Herbelin	2016-02-18
\| *	Update copyright headers.	Maxime Dénès	2016-01-20
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-13
\|\\|
\| *	Fixing #4467 (continued).	Hugo Herbelin	2016-01-13
\| *	Extend last commit: keyed unification uses full conversions on the applied co...	Matthieu Sozeau	2016-01-12
\| *	Extend Keyed Unification tests with the one from R. Krebbers.	Matthieu Sozeau	2016-01-12
* \|	Fixing a bug in the order of side conditions for introduction pattern -> and <-.	Hugo Herbelin	2015-12-25
* \|	Fixing an "injection as" bug in the presence of side conditions.	Hugo Herbelin	2015-12-25
* \|	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
\| *	Fix test-suite files after change in refine tactic.	Maxime Dénès	2015-12-15
\| *	Adding a test for the unshelve tactical.	Pierre-Marie Pédrot	2015-12-15
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-12-15
\|\\|
\| *	extraction_impl.v: fix a typo	Pierre Letouzey	2015-12-14
\| *	A test file for Extraction Implicit (including bugs #4243 and #4228)	Pierre Letouzey	2015-12-14
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-12-11
\|\\|
\| *	Fixing a pat%constr bug. Thanks to Enrico for reporting.	Hugo Herbelin	2015-12-10
\| *	Changing syntax of pat/constr1.../constrn into pat%constr1...%constrn.	Hugo Herbelin	2015-12-10
\| *	bug fixes to vm computation + test cases.	Gregory Malecha	2015-12-09
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-12-08
\|\\|
\| *	Changing "destruct !hyp" into "destruct (hyp)" (and similarly for induction)	Hugo Herbelin	2015-12-05
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-12-03
\|\\|
\| *	Improving syntax of pat/constr introduction pattern so that	Hugo Herbelin	2015-12-02
\| *	Changing syntax "$(tactic)$" into "ltac:(tactic)", as discussed in WG.	Hugo Herbelin	2015-12-02
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-11-29
\|\\|