coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
* \| \| \| \| \| \| \| \| \| \|	trivial	Matej Kosik	2017-04-10
* \| \| \| \| \| \| \| \| \| \|	simplify: Environ.push_named	Matej Kosik	2017-04-10
* \| \| \| \| \| \| \| \| \| \|	refactoring: Names.DirPath.is_empty	Matej Kosik	2017-04-10
* \| \| \| \| \| \| \| \| \| \|	refactoring: Names.DirPath.compare	Matej Kosik	2017-04-10
* \| \| \| \| \| \| \| \| \| \|	refactoring: Names.DirPath.equal	Matej Kosik	2017-04-10
* \| \| \| \| \| \| \| \| \| \|	comment: typo	Matej Kosik	2017-04-10
* \| \| \| \| \| \| \| \| \| \|	refactoring: Reductionops.contextual_reduction_function type	Matej Kosik	2017-04-10
* \| \| \| \| \| \| \| \| \| \|	Merge PR#547: [toplevel] Remove the feedback printer only on exit.	Maxime Dénès	2017-04-10
\|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \	Merge PR#548: [ide] Correctly place warning tags.	Maxime Dénès	2017-04-10
\|\ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \	Merge PR#460: Turning the printing primitive projection compatibility flag of...	Maxime Dénès	2017-04-09
\|\ \ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| * \| \| \| \| \| \| \|	Fix an algorithmic issue in Nsatz.	Pierre-Marie Pédrot	2017-04-09
\| \| \| \| \| \| * \| \| \| \| \| \| \|	Academic prescriptivism strikes back: down with baroque programming in Nsatz.	Pierre-Marie Pédrot	2017-04-09
\| \|_\|_\|_\|_\|/ / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| * \| \| \| \| \|	Fast path in weak head reduction of applied atoms.	Pierre-Marie Pédrot	2017-04-08
\| \|_\|_\|_\|_\|_\|/ / / / / / \|/\| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| * \|	Fixing #5460 (limitation in computing deps in pattern-matching compilation).	Hugo Herbelin	2017-04-08
\| \| * \| \| \| \| \| \| \| \| \|	[ide] Correctly place warning tags.	Emilio Jesus Gallego Arias	2017-04-08
\| \|/ / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \|	Update the .mailmap file.	Guillaume Melquiond	2017-04-08
\| \| \| * \| \| \| \| \| \| \|	Fix a heuristic used by legacy typeclass resolution.	Pierre-Marie Pédrot	2017-04-08
\| \| \| \| \| \| \| * \| \| \|	[stm] remove process_error_hook	Emilio Jesus Gallego Arias	2017-04-07
\| \| \| \| \| \| \| * \| \| \|	[stm] remove tactic_being_run hook	Emilio Jesus Gallego Arias	2017-04-07
\| \|_\|_\|_\|_\|_\|/ / / / \|/\| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \|	Merge PR#461: [camlpX] Remove camlp4 compat layer.	Maxime Dénès	2017-04-07
\|\ \ \ \ \ \ \ \ \ \
\| \| \| * \| \| \| \| \| \| \|	[toplevel] Remove the feedback feeder printing only on exit.	Emilio Jesus Gallego Arias	2017-04-07
\| \|_\|/ / / / / / / / \|/\| \| \| \| \| \| \| \| \|
\| \| \| * \| \| \| \| \| \|	Fix an unhandled exception in Omega.	Pierre-Marie Pédrot	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
\|\ \ \ \ \ \ \ \ \ \
\| \| \| \| * \ \ \ \ \ \	Merge branch 'master' into econstr	Pierre-Marie Pédrot	2017-04-07
\| \| \| \| \|\ \ \ \ \ \ \ \| \|_\|_\|_\|/ / / / / / / \|/\| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \|	Remove a forgotten rule for decl_mode from the Makefile.	Pierre-Marie Pédrot	2017-04-07
\| \| \| * \| \| \| \| \| \| \|	Turning the printing primitive projection parameter flag off by default.	Hugo Herbelin	2017-04-07
\| \| \| * \| \| \| \| \| \| \|	Turning the printing primitive projection compatibility flag off by default.	Hugo Herbelin	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
\|\ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| * \| \| \| \| \| \|	Fix a normalization hotspot in computation of constr keys.	Pierre-Marie Pédrot	2017-04-06
\| \| \| \| \| \| \| \| * \| \| \| \|	Factor interp_instance out of Pretyping.pretype_global	Gaetan Gilbert	2017-04-06
\| \| \| \| \| \| \| \| * \| \| \| \|	Avoid strange shadowing of Pretyping.interp_universe_level_name	Gaetan Gilbert	2017-04-06
\| \| \| \| \| \| \| \| \| \| \| * \|	Fix a few programming pearls related to Time, Fail and Redirect.	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
\| \| \| \| \| \| \| \| \| \| \| * \|	Merge branch 'origin/v8.5' into v8.6.	Hugo Herbelin	2017-04-06
\| \| \| \| \| \| \| \| \| \| \| \|\ \
\| \| \| \| \| * \| \| \| \| \| \| \| \|	[toplevel] Remove exception error printer in favor of feedback printer.	Emilio Jesus Gallego Arias	2017-04-05
\| \|_\|_\|_\|/ / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| * \| \| \| \| \| \|	Removing a normalization hotspot from EConstr.	Pierre-Marie Pédrot	2017-04-05
\| \| \| \| \| \| \| \| \| \| * \| \|	Fixing #5454 (an assert false with 'pat).	Hugo Herbelin	2017-04-05
* \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR#434: Optimizing array mapping in the kernel.	Maxime Dénès	2017-04-05
\|\ \ \ \ \ \ \ \ \ \ \ \ \