coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Fast path in weak head reduction of applied atoms.	Pierre-Marie Pédrot	2017-04-08
*	Update the .mailmap file.	Guillaume Melquiond	2017-04-08
*	Merge PR#461: [camlpX] Remove camlp4 compat layer.	Maxime Dénès	2017-04-07
\|\
* \|	Fixes for Drop. to work (decl_mode removal and toplevel -> vernac)	Matthieu Sozeau	2017-04-07
* \|	Merge PR#485: Document Show Match	Maxime Dénès	2017-04-07
\|\ \
* \| \|	Remove a forgotten rule for decl_mode from the Makefile.	Pierre-Marie Pédrot	2017-04-07
\| \| *	[travis] Overlay for PR#461: Camlp4 removal.	Emilio Jesus Gallego Arias	2017-04-07
\| \| *	[camlpX] Enrico's changes to camlp4 removal.	Emilio Jesus Gallego Arias	2017-04-07
\| \| *	[camlpX] Remove camlp4 compat layer.	Emilio Jesus Gallego Arias	2017-04-07
\| \|/ \|/\|
* \|	Merge PR#530: [toplevel] Remove exception error printer in favor of feedback ...	Maxime Dénès	2017-04-07
\|\ \
* \ \	Merge PR#519: Faster side effects	Maxime Dénès	2017-04-07
\|\ \ \
\| * \| \|	Inline the only use of hcons_j in Term_typing.	Pierre-Marie Pédrot	2017-04-07
* \| \| \|	Merge PR#455: Farewell decl_mode	Maxime Dénès	2017-04-06
\|\ \ \ \
* \ \ \ \	Merge PR#488: Adding a documentation for the new proof engine.	Maxime Dénès	2017-04-06
\|\ \ \ \ \
\| * \| \| \| \|	Adding a documentation for the new proof engine.	Pierre-Marie Pédrot	2017-04-06
\|/ / / / /
\| \| * \| \|	Documenting the fact terms are only hashconsed outside of a section.	Pierre-Marie Pédrot	2017-04-06
* \| \| \| \|	Merge PR#508: Optimize pending evars	Maxime Dénès	2017-04-06
\|\ \ \ \ \
* \ \ \ \ \	Merge PR#542: [travis] Add webhook to Gitter.	Maxime Dénès	2017-04-06
\|\ \ \ \ \ \
\| * \| \| \| \| \|	[travis] Add webhook to Gitter.	Théo Zimmermann	2017-04-06
\| \| \| \| \| * \|	[toplevel] Remove exception error printer in favor of feedback printer.	Emilio Jesus Gallego Arias	2017-04-05
\| \|_\|_\|_\|/ / \|/\| \| \| \| \|
* \| \| \| \| \|	Merge PR#434: Optimizing array mapping in the kernel.	Maxime Dénès	2017-04-05
\|\ \ \ \ \ \
* \ \ \ \ \ \	Merge PR#502: [pp] Add anomaly header to error messages.	Maxime Dénès	2017-04-04
\|\ \ \ \ \ \ \
* \ \ \ \ \ \ \	Merge branch 'v8.6' into trunk	Maxime Dénès	2017-04-03
\|\ \ \ \ \ \ \ \
\| * \ \ \ \ \ \ \	Merge PR#533: Instances should obey universe binders even when defined by tac...	Maxime Dénès	2017-04-03
\| \|\ \ \ \ \ \ \ \
* \| \| \| \| \| \| \| \| \|	Fix loading of ocamldebug printers.	Pierre-Marie Pédrot	2017-04-03
\| \| * \| \| \| \| \| \| \|	Instances should obey universe binders even when defined by tactics.	Gaetan Gilbert	2017-04-03
\| \|/ / / / / / / /
* \| \| \| \| \| \| \| \|	Merge PR#417: No cast surgery in let in	Maxime Dénès	2017-04-03
\|\ \ \ \ \ \ \ \ \
\| \| * \| \| \| \| \| \| \|	Add test file for #4957.	Maxime Dénès	2017-04-03
* \| \| \| \| \| \| \| \| \|	Fix higher-order pattern variables not being printed as "@?" (bug #5431).	Guillaume Melquiond	2017-04-02
* \| \| \| \| \| \| \| \| \|	Fix documentation typo (bug #5433).	Guillaume Melquiond	2017-04-02
* \| \| \| \| \| \| \| \| \|	Simplify some proofs.	Guillaume Melquiond	2017-04-02
* \| \| \| \| \| \| \| \| \|	Declaring ltac plugin, so that static linking works.	Hugo Herbelin	2017-04-01
* \| \| \| \| \| \| \| \| \|	Merge branch 'v8.6' into trunk	Maxime Dénès	2017-03-30
\|\ \ \ \ \ \ \ \ \ \ \| \| \|/ / / / / / / / \| \|/\| \| \| \| \| \| \| \|
\| * \| \| \| \| \| \| \| \|	Merge PR#463: Run non-tactic comands without resilient_command	Maxime Dénès	2017-03-30
\| \|\ \ \ \ \ \ \ \ \
* \| \| \| \| \| \| \| \| \| \|	Fix ring_simplify sometimes producing R0 and R1 instead of 0%R and 1%R.	Guillaume Melquiond	2017-03-30
* \| \| \| \| \| \| \| \| \| \|	Merge PR#469: Added take to VectorDef	Maxime Dénès	2017-03-30
\|\ \ \ \ \ \ \ \ \ \ \
\| * \| \| \| \| \| \| \| \| \| \|	Added take to VectorDef.	George Stelle	2017-03-30
* \| \| \| \| \| \| \| \| \| \| \|	Merge PR#511: [stm] Remove some obsolete vernacs/classification.	Maxime Dénès	2017-03-30
\|\ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \	Merge PR#522: [coqide] Protect against size_allocate race in proofview.	Maxime Dénès	2017-03-29
\|\ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \	Merge branch 'v8.6' into trunk	Maxime Dénès	2017-03-29
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \| \| \|_\|_\|/ / / / / / / / / / \| \|/\| \| \| \| \| \| \| \| \| \| \| \|
\| * \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR#514: [travis] Backport from trunk: VST	Maxime Dénès	2017-03-29
\| \|\ \ \ \ \ \ \ \ \ \ \ \ \
* \| \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR#506: [nit] Fix a couple incorrect uses of msg_error.	Maxime Dénès	2017-03-29
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR#521: Do so that "About" tells if a reference is a coercion.	Maxime Dénès	2017-03-29
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR#525: [ide] Fix typo in pp serialization.	Maxime Dénès	2017-03-29
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| * \| \| \| \| \| \| \|	Run non-tactic comands without resilient_command	Tej Chajed	2017-03-29
\| \| \| \| \| \|_\|_\|_\|/ / / / / / / / \| \| \| \| \|/\| \| \| \| \| \| \| \| \| \| \|
\| * \| \| \| \| \| \| \| \| \| \| \| \| \| \|	[ide] Fix typo in pp serialization.	Emilio Jesus Gallego Arias	2017-03-29
* \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Fixing missing PropFacts.v in Logic/vo.itarget.	Hugo Herbelin	2017-03-28
\|/ / / / / / / / / / / / / / /
\| \| \| \| \| * / / / / / / / / /	[coqide] Protect against size_allocate race in proofview.	Emilio Jesus Gallego Arias	2017-03-28
\| \|_\|_\|_\|/ / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \|
\| * \| \| \| \| \| \| \| \| \| \| \| \|	Do so that "About" tells if a reference is a coercion.	Hugo Herbelin	2017-03-27
\|/ / / / / / / / / / / / /
\| \| \| \| \| \| \| \| \| \| \| * \|	More efficient check in validity of side-effects.	Pierre-Marie Pédrot	2017-03-27