coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge PR#531: Fixing bug #5420 and many similar bugs due to the presence of l...	Maxime Dénès	2017-04-28
\|\
* \	Merge PR#414: Some more theory on powerRZ.	Maxime Dénès	2017-04-27
\|\ \
* \ \	Merge PR#583: [toplevel] More work on error handling.	Maxime Dénès	2017-04-27
\|\ \ \
* \ \ \	Merge PR#586: trivial cleanup commits which does not change Coq API	Maxime Dénès	2017-04-27
\|\ \ \ \
* \ \ \ \	Merge PR#568: Remove tactic compatibility layer	Maxime Dénès	2017-04-27
\|\ \ \ \ \
\| * \| \| \| \|	Document the API changes.	Pierre-Marie Pédrot	2017-04-27
* \| \| \| \| \|	Merge PR#584: Give andb_prop a simpler proof	Maxime Dénès	2017-04-27
\|\ \ \ \ \ \
* \ \ \ \ \ \	Merge PR#585: Small typo in comment	Maxime Dénès	2017-04-27
\|\ \ \ \ \ \ \
* \ \ \ \ \ \ \	Merge branch 'v8.6'	Pierre-Marie Pédrot	2017-04-27
\|\ \ \ \ \ \ \ \
\| \| \| \| \| * \| \| \|	contracting the type of "Pfedit.solve_by_implicit_tactic"	Matej Košík	2017-04-27
\| \|_\|_\|_\|/ / / / \|/\| \| \| \| \| \| \|
\| \| * \| \| \| \| \|	Small typo in comment	Vadim Zaliva	2017-04-26
\| \|/ / / / / / \|/\| \| \| \| \| \|
\| \| * \| \| \| \|	Give andb_prop a simpler proof	Jason Gross	2017-04-25
\| \|/ / / / / \|/\| \| \| \| \|
\| \| \| * \| \|	[toplevel] Remove unused parameter from `Vernac.process_expr`.	Emilio Jesus Gallego Arias	2017-04-25
\| \| \| * \| \|	[toplevel] Use exception information for error printing.	Emilio Jesus Gallego Arias	2017-04-25
\| * \| \| \| \|	Fix an optimization failure in tclPROGRESS.	Pierre-Marie Pédrot	2017-04-25
* \| \| \| \| \|	Fix an optimization failure in tclPROGRESS.	Pierre-Marie Pédrot	2017-04-25
\| * \| \| \| \|	Merge PR#567: Fix bug #5377: @? patterns broken.	Maxime Dénès	2017-04-25
\| \|\ \ \ \ \
* \| \ \ \ \ \	Merge PR#578: Fix nsatz not recognizing real literals.	Maxime Dénès	2017-04-25
\|\ \ \ \ \ \ \
\| \| \| \| \| * \| \|	[toplevel] Don't check proofs in -quick mode.	Emilio Jesus Gallego Arias	2017-04-24
\| \| \| \| \| * \| \|	[toplevel] Don't mask critical exceptions in vernac interpretation.	Emilio Jesus Gallego Arias	2017-04-24
\| \|_\|_\|_\|/ / / \|/\| \| \| \| \| \|
\| \| \| \| * \| \|	Adding a dedicated travis overlay for fiat-parsers.	Pierre-Marie Pédrot	2017-04-24
\| \| \| \| * \| \|	Removing various tactic compatibility layers in core tactics.	Pierre-Marie Pédrot	2017-04-24
\| \| \| \| * \| \|	Porting the firstorder plugin to the new tactic API.	Pierre-Marie Pédrot	2017-04-24
\| \| \| \| * \| \|	Removing compatibility layer in Leminv.	Pierre-Marie Pédrot	2017-04-24
\| \| \| \| * \| \|	Removing tactic compatibility layer in Command.	Pierre-Marie Pédrot	2017-04-24
\| \| \| \| * \| \|	Removing tactic compatibility layer in congruence.	Pierre-Marie Pédrot	2017-04-24
\| \| \| \| * \| \|	Removing tactic compatibility layer in Micromega.	Pierre-Marie Pédrot	2017-04-24
\| \| \| \| * \| \|	Fix the API of the new pf_constr_of_global.	Pierre-Marie Pédrot	2017-04-24
\| \| \| \| * \| \|	Removing trivial compatibility layer in refl_omega.	Pierre-Marie Pédrot	2017-04-24
\| \| \| \| * \| \|	Porting omega to the new tactic API.	Pierre-Marie Pédrot	2017-04-24
\| \| \| \| * \| \|	Removing trivial compatibility layer in omega.	Pierre-Marie Pédrot	2017-04-24
\| \| \| \| * \| \|	Porting generalize_dep to the new tactic engine.	Pierre-Marie Pédrot	2017-04-24
\| \| \| \| * \| \|	Removing the tclWEAK_PROGRESS tactical.	Pierre-Marie Pédrot	2017-04-24
\| \| \| \| * \| \|	Removing the tclNOTSAMEGOAL primitive from the API.	Pierre-Marie Pédrot	2017-04-24
\| \|_\|_\|/ / / \|/\| \| \| \| \|
* \| \| \| \| \|	Merge PR#579: [flags] Deprecate is_silent/is_verbose in favor of single flag.	Maxime Dénès	2017-04-24
\|\ \ \ \ \ \
* \ \ \ \ \ \	Merge PR#574: Fix bug #5476: Ltac has an inconsistent view of hypotheses.	Maxime Dénès	2017-04-24
\|\ \ \ \ \ \ \
* \ \ \ \ \ \ \	Merge PR#552: Miscelaneous commits	Maxime Dénès	2017-04-24
\|\ \ \ \ \ \ \ \
\| \| \| \| \| * \ \ \	Merge PR#577: Add bedrock targets src and facade to Travis CI	Maxime Dénès	2017-04-24
\| \| \| \| \| \|\ \ \ \
* \| \| \| \| \| \ \ \ \	Merge PR#569: Documenting EConstr for developpers.	Maxime Dénès	2017-04-24
\|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \	Merge PR#565: Remove VernacError	Maxime Dénès	2017-04-24
\|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \	Merge PR#580: [ide] Fix #5482 "location for query commands" in IDE.	Maxime Dénès	2017-04-24
\|\ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \	Merge PR#581: [toplevel] [emacs] Don't quote errors in emacs mode.	Maxime Dénès	2017-04-24
\|\ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR#492: [travis] Pin camlp5 to the minimal version 6.14 for 4.02.3	Maxime Dénès	2017-04-24
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR#576: [ide] Rely less on `Stateid.dummy`	Maxime Dénès	2017-04-24
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\| \| * \| \| \| \| \| \| \| \| \| \| \| \| \|	[travis] Pin camlp5 to the minimal version 6.14 for 4.02.3	Emilio Jesus Gallego Arias	2017-04-24
\| \| \| * \| \| \| \| \| \| \| \| \| \| \| \|	[toplevel] [emacs] Don't quote errors in emacs mode.	Emilio Jesus Gallego Arias	2017-04-23
\| \| \|/ / / / / / / / / / / / /
* \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge branch v8.6 into trunk	Hugo Herbelin	2017-04-22
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \| \| \|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / / \| \|/\| \| \| \| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Removing TODO file which is unused for more than 10 years.	Hugo Herbelin	2017-04-22
\| \|_\|/ / / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| * \| \| \| \| \| \| \| \| \| \|	[ide] Fix #5482 "location for query commands" in IDE.	Emilio Jesus Gallego Arias	2017-04-21
\| \|_\|/ / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| * \| \| \| \| \| \| \| \| \|	Remove VernacError	Gaetan Gilbert	2017-04-21
\| \|_\|/ / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \|