coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Make theorems about ex equality Qed	Jason Gross	2017-05-28
\| \| \| \| \|	As requested in https://github.com/coq/coq/pull/384#issuecomment-303809461
*	Make new proofs of equality Qed	Jason Gross	2017-05-28
\| \| \| \| \|	As requested in https://github.com/coq/coq/pull/384#issuecomment-303809461
*	Add some more comments about sigma equalities	Jason Gross	2017-05-28
\| \| \| \| \|	Forwards/backwards reasoning thoughts come from https://github.com/coq/coq/pull/385#discussion_r111008347
*	Remove motive argument from [rew dependent]	Jason Gross	2017-05-28
\|
*	Use a local [rew dependent] notation	Jason Gross	2017-05-28
\|
*	Add forward-chaining versions: [eq_sig*_uncurried]	Jason Gross	2017-05-28
\|
*	Use notation for sigT	Jason Gross	2017-05-28
\|
*	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
\| \| \| \| \| \| \| \| \|	The ' was originally denoting that we were taking in the projections and applying the constructor in the conclusion, rather than taking in the bundled versions and projecting them out (because the projections don't exist for [ex] and [ex2]). But we don't have versions like this for [sig] and [sigT] and [sigT2] and [sig2], so we might as well not add the ' to the [ex] and [ex2] versions.
*	Use [rew_] instead of [eq_rect_] prefix	Jason Gross	2017-05-28
\| \| \| \|	As per Hugo's request.
*	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
\| \| \| \| \|	As per Hugo's suggestion in https://github.com/coq/coq/pull/384#issuecomment-264891011
*	Add an [inversion_sigma] tactic	Jason Gross	2017-05-28
\| \| \| \|	This tactic does better than [inversion] at sigma types.
*	Add lemmas about equality of sigma types	Jason Gross	2017-05-28
\|
*	Use [rew_] instead of [eq_rect_] prefix	Jason Gross	2017-05-28
\| \| \| \|	As per Hugo's request.
*	Use [rew] notations rather than [eq_rect]	Jason Gross	2017-05-28
\| \| \| \| \|	As per Hugo's request in https://github.com/coq/coq/pull/384#issuecomment-264891011
*	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
\|/ / / / / \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	We are waiting for an upstream merge of a fix related to coq_makefile2.
\| \| \| \| *	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
\| \| \| \| *	[checker] [votour] resolve warning 52 fragile constant pattern	Gaëtan Gilbert	2017-05-26
\| \| \| \|/ \| \| \| \| \| \| \| \| \| \| \| \|	Also stop using failwith for flow control in tuple_of_string.
* \| \| \|	Merge PR#666: romega revisited : no more normalization trace, cleaned-up ↵	Maxime Dénès	2017-05-26
\|\ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	resolution trace
* \ \ \ \	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
\| \|\ \ \ \ \ \ \ \ \ \| \|/ / / / / / / / / \|/\| \| \| \| \| \| \| \| \|