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
*	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
*	Cleanup: removal of constr_of_global.	Matthieu Sozeau	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
\|\ \ \
* \ \ \	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
\|\ \ \ \ \
* \ \ \ \ \	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
\|\ \ \ \ \ \ \
* \ \ \ \ \ \ \	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
\|\ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| \| \| \| *	[cleanup] Unify all calls to the error function.	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
\| \| \| \|/ /
* \| \| \| \|	Merge PR#666: romega revisited : no more normalization trace, cleaned-up reso...	Maxime Dénès	2017-05-26
\|\ \ \ \ \
* \ \ \ \ \	Merge PR#655: Extra functions exported in EConstr	Maxime Dénès	2017-05-26
\|\ \ \ \ \ \ \| \|_\|_\|_\|_\|/ \|/\| \| \| \| \|
\| \| \| \| \| *	[checker] Add bin/votour to the coqocaml target.	Emilio Jesus Gallego Arias	2017-05-26
\| \| \| \| \| *	[votour] Fix/disable warnings.	Emilio Jesus Gallego Arias	2017-05-26
\| \| \| \| \| *	[votour] Fix build with -safe-string (bug 5553)	Emilio Jesus Gallego Arias	2017-05-26
\| \|_\|_\|_\|/ \|/\| \| \| \|
\| \| \| \| *	add Show test with -emacs flag	Paul Steckler	2017-05-25
\| \|_\|_\|/ \|/\| \| \|
* \| \| \|	Merge PR#645: [stm] Tweak debug options.	Maxime Dénès	2017-05-25
\|\ \ \ \
* \ \ \ \	Merge PR#637: Short cleaning of the interpretation path for constr_with_bindings	Maxime Dénès	2017-05-25
\|\ \ \ \ \
* \ \ \ \ \	Merge PR#608: Allow Ltac2 as a plugin	Maxime Dénès	2017-05-25
\|\ \ \ \ \ \
* \ \ \ \ \ \	Merge PR#481: [option] Remove support for non-synchronous options.	Maxime Dénès	2017-05-25
\|\ \ \ \ \ \ \
* \ \ \ \ \ \ \	Merge PR#406: coq makefile2	Maxime Dénès	2017-05-25
\|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \	Merge PR#402: Uniform attribute handling in interfaces	Maxime Dénès	2017-05-25
\|\ \ \ \ \ \ \ \ \
\| * \| \| \| \| \| \| \| \|	[location] [travis] Add overlays for located_switch	Emilio Jesus Gallego Arias	2017-05-25
\| * \| \| \| \| \| \| \| \|	[location] Fix warnings.	Emilio Jesus Gallego Arias	2017-05-24
\| * \| \| \| \| \| \| \| \|	[location] Renaming "CAst.ast" to "CAst.t"	Matej Košík	2017-05-24
\| * \| \| \| \| \| \| \| \|	Merge branch 'trunk' into located_switch	Emilio Jesus Gallego Arias	2017-05-24
\| \|\ \ \ \ \ \ \ \ \ \| \|/ / / / / / / / / \|/\| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| * \|	ROmega: division-aware ReflOmegaCore, allowing trace without terms	Pierre Letouzey	2017-05-24
\| \| \| * \| \| \| \| \| \|	[option] Remove support for non-synchronous options.	Emilio Jesus Gallego Arias	2017-05-24
\| \| * \| \| \| \| \| \| \|	coq_makefile: use -include rather than include	Enrico Tassi	2017-05-24
* \| \| \| \| \| \| \| \| \|	Merge PR#642: Small cleanup on `close_proof` type.	Maxime Dénès	2017-05-24
\|\ \ \ \ \ \ \ \ \ \