coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Remove reference to [IsIso]	Jason Gross	2017-05-28
*	Use notations for [sig], [sigT], [sig2], [sigT2]	Jason Gross	2017-05-28
*	Use extended notation for ex, ex2 types	Jason Gross	2017-05-28
*	Replace [ex'] with [ex]	Jason Gross	2017-05-28
*	Use [rew_] instead of [eq_rect_] prefix	Jason Gross	2017-05-28
*	Add equality lemmas for sig2 and sigT2	Jason Gross	2017-05-28
*	Add lemmas for ex2	Jason Gross	2017-05-28
*	Use [rew] notations rather than [eq_rect]	Jason Gross	2017-05-28
*	Add an [inversion_sigma] tactic	Jason Gross	2017-05-28
*	Add lemmas about equality of sigma types	Jason Gross	2017-05-28
*	Use [rew_] instead of [eq_rect_] prefix	Jason Gross	2017-05-28
*	Use [rew] notations rather than [eq_rect]	Jason Gross	2017-05-28
*	Add more groupoid-like theorems about [eq]	Jason Gross	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
\|\ \ \ \ \
\| \| * \| \| \|	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
\| \|_\|_\|/ \|/\| \| \|
\| \| \| *	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
\|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \	Merge PR#650: Fixing an extra bug with pattern_of_constr	Maxime Dénès	2017-05-24
\|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \	Merge PR#671: unification.mli: Fix a spelling typo in a comment	Maxime Dénès	2017-05-24
\|\ \ \ \ \ \ \ \ \ \ \ \ \| \|_\|_\|_\|_\|/ / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \|
\| * \| \| \| \| \| \| \| \| \| \|	unification.mli: Fix a spelling typo in a comment	Jason Gross	2017-05-23
\|/ / / / / / / / / / /