coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
\| \| \| \| * \| \|	Pretyping cleanup: remove constr_of_global calls	Matthieu Sozeau	2017-05-29
\| \| \| \| * \| \|	tactics cleanup: remove constr_of_global calls	Matthieu Sozeau	2017-05-29
* \| \| \| \| \| \|	Merge PR#690: [stm] Uniformize `Sideff / Sideff.	Maxime Dénès	2017-05-29
\|\ \ \ \ \ \ \
\| \| \| \| \| * \| \|	Ltac cleanup: no more constr_of_global calls	Matthieu Sozeau	2017-05-29
\| \| \| \| \| * \| \|	Equality cleanup: remove constr_of_global	Matthieu Sozeau	2017-05-29
\| \| \| \| \| * \| \|	Command.ml cleanup: remove constr_of_global calls	Matthieu Sozeau	2017-05-29
* \| \| \| \| \| \| \|	Merge PR#555: Missing optimization when Kernel Term Sharing is disabled.	Maxime Dénès	2017-05-29
\|\ \ \ \ \ \ \ \
\| \| \| \| \| * \| \| \|	Configuration with -local definitively seen as an installation layout like ot...	Hugo Herbelin	2017-05-29
\| \| \| \| \| * \| \| \|	Using the same strategy in coqdoc than in coqtop to guess the coqlib.	Hugo Herbelin	2017-05-29
\| \| \| \| \| * \| \| \|	Relying on computation done in Envars to discover the installation directories.	Hugo Herbelin	2017-05-29
\| \| \| \| \| * \| \| \|	Generalizing to docdir and datadir the test for a relocated installation.	Hugo Herbelin	2017-05-29
\| \| \| \| \| * \| \| \|	Exporting the suffixes needed to build coqlib, docdir, etc.	Hugo Herbelin	2017-05-29
\| \| \| \| \| * \| \| \|	Using Coq_config.local rather than None to tell that Coq_config.coqlib is local.	Hugo Herbelin	2017-05-29
\| \| \| \| \| \| * \| \|	Cleanup: removal of constr_of_global.	Matthieu Sozeau	2017-05-29
\| \|_\|_\|_\|_\|/ / / \|/\| \| \| \| \| \| \|
\| \| \| \| \| * \| \|	Configure: viewing compilation in -local itself as an installation layout.	Hugo Herbelin	2017-05-29
\| \| \| \| \| * \| \|	Configuration: always giving a value to configdir and datadir.	Hugo Herbelin	2017-05-29
\| \| \| \| \| * \| \|	More structure and more code factorization in building default	Hugo Herbelin	2017-05-29
\| \| \| \| \| * \| \|	Unifying the layout of installation directories.	Hugo Herbelin	2017-05-29
\| \| \| \| \| * \| \|	Unified terminology in configure.ml/coq_config.ml: arch_win32 -> arch_is_win32.	Hugo Herbelin	2017-05-29
\| \| \| \| \| * \| \|	Mini-renaming in configure.ml to avoid switching back and forth from	Hugo Herbelin	2017-05-29
\| \| \| \| \| * \| \|	Dead code (xdg_config_dirs).	Hugo Herbelin	2017-05-29
* \| \| \| \| \| \| \|	Merge PR#512: [cleanup] Unify all calls to the error function.	Maxime Dénès	2017-05-29
\|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \	Merge PR#678: [coqlib] Move `Coqlib` to `library/`.	Maxime Dénès	2017-05-28
\|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \	Merge PR#689: Changes to make coq-makefile not failing on MacOS X.	Maxime Dénès	2017-05-28
\|\ \ \ \ \ \ \ \ \ \ \| \|_\|_\|_\|_\|_\|_\|/ / / \|/\| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| * \| \|	Fail on deprecated warning even for Ocaml > 4.02.3	Gaëtan Gilbert	2017-05-28
* \| \| \| \| \| \| \| \| \|	Merge PR#675: [coqlib] Deprecate redundant Coqlib functions.	Maxime Dénès	2017-05-28
\|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \	Merge PR#683: coq_makefile: build .cma for each .mlpack	Maxime Dénès	2017-05-28
\|\ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| \| \| * \| \|	Don't disable deprecation warning for configure.ml	Gaëtan Gilbert	2017-05-28
* \| \| \| \| \| \| \| \| \| \| \|	Merge PR#684: Trunk+fix coq makefile test suite on nixos	Maxime Dénès	2017-05-28
\|\ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \	Merge PR#681: Fix votour for safe strings & warnings	Maxime Dénès	2017-05-28
\|\ \ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| \| \| \| * \| \| \|	Gitlab CI	Gaëtan Gilbert	2017-05-28
\| \| \| \| \| \| \| \| \| \| \|/ / /
* \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR#680: add Show test with -emacs flag for trunk	Maxime Dénès	2017-05-28
\|\ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR#676: Primitive Ltac definitions for first and solve	Maxime Dénès	2017-05-28
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR#658: [coqdoc] Add keywords in bug 2884.	Maxime Dénès	2017-05-28
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| \| * \| \|	[stm] Rename Side-Effect type.	Emilio Jesus Gallego Arias	2017-05-27
\| \| \| \| \| \| \| \| \| \| * \| \| \| \|	[cleanup] Unify all calls to the error function.	Emilio Jesus Gallego Arias	2017-05-27
\| \|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| * \| \|	[stm] Uniformize `Sideff / Sideff.	Emilio Jesus Gallego Arias	2017-05-27
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / / \|/\| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| * \| \| \|	[coqlib] Move `Coqlib` to `library/`.	Emilio Jesus Gallego Arias	2017-05-27
\| \| \| \| \| \| \| \| \|/ / / / \| \| \| \| \| \| \| \|/\| \| \| \|
\| \| \| \| \| \| \| * \| \| \| \|	[coqlib] Deprecate redundant Coqlib functions.	Emilio Jesus Gallego Arias	2017-05-27
\| \|_\|_\|_\|_\|_\|/ / / / / \|/\| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| * \| \| \| \|	coq_makefile: build .cma for each .mlpack	Enrico Tassi	2017-05-27
\| \| * \| \| \| \| \| \| \| \|	Documenting the existence of first and solve as Ltac definitions.	Pierre-Marie Pédrot	2017-05-27
\| \| * \| \| \| \| \| \| \| \|	Exporting a few primitive tacticals as named Ltac definitions.	Pierre-Marie Pédrot	2017-05-27
\| \|/ / / / / / / / / \|/\| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \|	Merge PR#686: [travis] temporary UniMath overlay	Maxime Dénès	2017-05-27
\|\ \ \ \ \ \ \ \ \ \
\| * \| \| \| \| \| \| \| \| \|	[travis] temporary UniMath overlay	Maxime Dénès	2017-05-27
\|/ / / / / / / / / /
\| \| \| \| * \| \| \| \| \|	Add execution permission to test-suite file.	Théo Zimmermann	2017-05-27
\| \| \| \| * \| \| \| \| \|	Use specific shell for more robustness.	Théo Zimmermann	2017-05-27
\| \| \| \| * \| \| \| \| \|	Fix test-suite/coq-makefile on NixOS.	Théo Zimmermann	2017-05-27
\| \|_\|_\|/ / / / / / \|/\| \| \| \| \| \| \| \|
\| \| \| \| \| * \| \| \|	Changes to make coq-makefile not failing on MacOS X.	Hugo Herbelin	2017-05-26
\| \|_\|_\|_\|/ / / / \|/\| \| \| \| \| \| \|
\| \| \| * \| \| \| \|	Merge pull request #7 from SkySkimmer/checker+fix_votour	Emilio Jesús Gallego Arias	2017-05-26
\| \| \| \|\ \ \ \ \
\| \| \| \| * \| \| \| \|	[checker] [votour] resolve warning 52 fragile constant pattern	Gaëtan Gilbert	2017-05-26
\| \| \| \|/ / / / /