coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
* \| \| \| \| \| \| \| \| \|	Merge PR#532: Clean Nsatz implementation.	Maxime Dénès	2017-04-11
\|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \	Merge PR#537: Efficient side-effect abstraction	Maxime Dénès	2017-04-11
\|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \	Merge PR#379: Introducing evar-insensitive constrs	Maxime Dénès	2017-04-11
\|\ \ \ \ \ \ \ \ \ \ \ \
\| * \| \| \| \| \| \| \| \| \| \| \|	Adding a test for 'rewrite in *' when an evar is solved by side-effect.	Pierre-Marie Pédrot	2017-04-10
\| * \| \| \| \| \| \| \| \| \| \| \|	Adding a test for the correctness of normalization in legacy typeclasses.	Pierre-Marie Pédrot	2017-04-10
\| * \| \| \| \| \| \| \| \| \| \| \|	Documenting the changes introduced by the EConstr branch.	Pierre-Marie Pédrot	2017-04-10
* \| \| \| \| \| \| \| \| \| \| \| \|	Revert "refactoring: Reductionops.contextual_reduction_function type"	Matej Košík	2017-04-10
* \| \| \| \| \| \| \| \| \| \| \| \|	Revert "comment: typo"	Matej Košík	2017-04-10
* \| \| \| \| \| \| \| \| \| \| \| \|	Revert "refactoring: Names.DirPath.equal"	Matej Košík	2017-04-10
* \| \| \| \| \| \| \| \| \| \| \| \|	Revert "refactoring: Names.DirPath.compare"	Matej Košík	2017-04-10
* \| \| \| \| \| \| \| \| \| \| \| \|	Revert "refactoring: Names.DirPath.is_empty"	Matej Košík	2017-04-10
* \| \| \| \| \| \| \| \| \| \| \| \|	Revert "simplify: Environ.push_named"	Matej Košík	2017-04-10
* \| \| \| \| \| \| \| \| \| \| \| \|	Revert "trivial"	Matej Košík	2017-04-10
* \| \| \| \| \| \| \| \| \| \| \| \|	Revert "trivial"	Matej Košík	2017-04-10
* \| \| \| \| \| \| \| \| \| \| \| \|	Revert "comments: corrected in the Context module"	Matej Košík	2017-04-10
* \| \| \| \| \| \| \| \| \| \| \| \|	comments: corrected in the Context module	Matej Kosik	2017-04-10
* \| \| \| \| \| \| \| \| \| \| \| \|	trivial	Matej Kosik	2017-04-10
* \| \| \| \| \| \| \| \| \| \| \| \|	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
\| \| \| \| \| \| \| \| \| \| * \|	Add some hints to the "real" database to automatically discharge literal comp...	Guillaume Melquiond	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
\|\ \ \ \ \ \ \ \ \ \