coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Moving code for "simple induction"/"simple destruct" to coretactics.ml4.	Hugo Herbelin	2018-03-01
*	Merge PR #6852: [stdlib] move “Require” out of sections	Maxime Dénès	2018-02-28
\|\
* \	Merge PR #6853: Add a comment on EConstr.to_constr regarding evar-freeness.	Maxime Dénès	2018-02-28
\|\ \
* \ \	Merge PR #1026: changed statements of Rpower_lt and Rle_power and added lemmas	Maxime Dénès	2018-02-28
\|\ \ \
* \ \ \	Merge PR #6756: Fix issue with spurious timing test failures	Maxime Dénès	2018-02-28
\|\ \ \ \
* \ \ \ \	Merge PR #6788: Fixes #6787 (minus sign interpreted by coqdoc as a bullet in ...	Maxime Dénès	2018-02-28
\|\ \ \ \ \
* \ \ \ \ \	Merge PR #6789: Check whitespace errors per-commit.	Maxime Dénès	2018-02-28
\|\ \ \ \ \ \
* \ \ \ \ \ \	Merge PR #6734: dest_{prod,lam}: no Cast case (it's removed by whd)	Maxime Dénès	2018-02-28
\|\ \ \ \ \ \ \
* \ \ \ \ \ \ \	Merge PR #6823: Fixes #6821 (bug in protecting notation printing from infinit...	Maxime Dénès	2018-02-28
\|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \	Merge PR #6812: Rename release_lexer_state to the more descriptive get_lexer_...	Maxime Dénès	2018-02-28
\|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \	Merge PR #6752: Remove from CircleCI builds that are already taken care of by...	Maxime Dénès	2018-02-28
\|\ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| \| \| * \|	Add a comment on EConstr.to_constr regarding evar-freeness.	Pierre-Marie Pédrot	2018-02-27
\| \|_\|_\|_\|_\|_\|_\|_\|/ / \|/\| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| *	[stdlib] move “Require” out of sections	Vincent Laporte	2018-02-27
\| \|_\|_\|_\|_\|_\|_\|_\|/ \|/\| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| * \|	[test-suite] Move sed scripts into bash arrays	Jason Gross	2018-02-24
* \| \| \| \| \| \| \| \|	Merge PR #6543: Update headers and credits	Maxime Dénès	2018-02-24
\|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \	Merge PR #6784: New IR in VM: Clambda	Maxime Dénès	2018-02-24
\|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \	Merge PR #6819: Document Arguments extra scopes flag	Maxime Dénès	2018-02-24
\|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \	Merge PR #6776: Fixes bug #6774 (anomaly with ill-typed template polymorphism).	Maxime Dénès	2018-02-24
\|\ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6803: coqdev.el: add space at the end of compile-command	Maxime Dénès	2018-02-24
\|\ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6599: Decimals in prelude	Maxime Dénès	2018-02-24
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6745: [ast] Improve precision of Ast location recognition in serial...	Maxime Dénès	2018-02-24
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| \| \| \| \| \| * \| \| \|	Check whitespace errors per-commit.	Gaëtan Gilbert	2018-02-23
\| \| \| \| \| \| * \| \| \| \| \| \| \| \| \|	New IR in VM: Clambda.	Maxime Dénès	2018-02-23
\| \| \| \| \| \| * \| \| \| \| \| \| \| \| \|	Fix map iterator on nativelambda.	Maxime Dénès	2018-02-23
\| \| \| \| \| \| \| \|_\|_\|_\|_\|/ / / / \| \| \| \| \| \| \|/\| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| * \| \| \| \|	Fixes #6821 (bug in protecting notation printing from infinite eta-expansion).	Hugo Herbelin	2018-02-23
\| \|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| * \| \| \| \| \| \| \| \|	Document Arguments extra scopes flag	Jasper Hugunin	2018-02-22
\| \|_\|_\|_\|/ / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| * \| \| \| \|	Tweak developer documentation.	Jim Fehrle	2018-02-22
\| \| \| \| \| \| \| \| * \| \| \| \|	Rename release_lexer_state to the more descriptive get_lexer_state.	Jim Fehrle	2018-02-22
\| \| \| \| \| \| \|_\|/ / / / / \| \| \| \| \| \|/\| \| \| \| \| \|
\| * \| \| \| / \| \| \| \| \| \|	[ast] Improve precision of Ast location recognition in serialization.	Emilio Jesus Gallego Arias	2018-02-22
\|/ / / / / / / / / / /
\| \| \| \| \| \| * / / / /	Remove from CircleCI builds that are already taken care of by Travis.	Théo Zimmermann	2018-02-21
\| \|_\|_\|_\|_\|/ / / / / \|/\| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \|	Merge PR #6604: Extend `zify_N` with knowledge about `N.pred`	Maxime Dénès	2018-02-21
\|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \	Merge PR #6282: proposed fix for issue #3213: extra variable m in Lt.S_pred	Maxime Dénès	2018-02-21
\|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \	Merge PR #6767: [ci] add elpi	Maxime Dénès	2018-02-21
\|\ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #982: Miscellaneous extensions of notations (including granting BZ5585)	Maxime Dénès	2018-02-21
\|\ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6283: A pre-commit hook to magically fix whitespace issues.	Maxime Dénès	2018-02-21
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6748: Fix bug #6529: nf_evar_info to nf the evars' env not just the...	Maxime Dénès	2018-02-21
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6740: Adding a sanity check on inductive variance subtyping.	Maxime Dénès	2018-02-21
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| * \| \| \| \|	Update CREDITS.	Théo Zimmermann	2018-02-21
\| \| \| \| \| \| \| \| \| \| \| * \| \| \| \|	More accurate and complete headers.	Théo Zimmermann	2018-02-21
\| \| \| \| \| \| \| \| \| \| \| * \| \| \| \|	Mention the CREDITS file in CONTRIBUTING.	Théo Zimmermann	2018-02-21
\| \| \| \| \| \| \| \| \| \| \| * \| \| \| \|	Remove redundant COPYRIGHT file.	Théo Zimmermann	2018-02-21
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| * \| \| \| \| \|	coqdev.el: add space at the end of compile-command	Gaëtan Gilbert	2018-02-21
\| \|_\|_\|_\|_\|_\|_\|_\|/ / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| * \| \| \| \| \|	Add CHANGES entry for decimals in prelude	Jason Gross	2018-02-20
\| \| \| \| \| \| \| \| * \| \| \| \| \|	Update SearchPattern.out for numeral notations	Jason Gross	2018-02-20
\| \| \| \| \| \| \| \| * \| \| \| \| \|	Doc: add Decimal-related files to index-list.html.template	Jason Gross	2018-02-20
\| \| \| \| \| \| \| \| * \| \| \| \| \|	Decimal goodies : conversion to/from Coq strings	Pierre Letouzey	2018-02-20
\| \| \| \| \| \| \| \| * \| \| \| \| \|	Decimal: proofs that conversions from/to nat,N,Z are bijections	Pierre Letouzey	2018-02-20
\| \| \| \| \| \| \| \| * \| \| \| \| \|	Decimal: simple representation of base-10 numbers	Pierre Letouzey	2018-02-20
\| \|_\|_\|_\|_\|_\|_\|/ / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| * \| \| \| \|	Fixes bug #6774 (anomaly with ill-typed template polymorphism).	Hugo Herbelin	2018-02-20
\| \|_\|_\|_\|_\|_\|_\|/ / / / / \|/\| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| * \| \|	Fixes #6787 (minus sign interpreted by coqdoc as a bullet in Ring_theory.v).	Hugo Herbelin	2018-02-20
\| \|_\|_\|_\|_\|_\|_\|_\|/ / / \|/\| \| \| \| \| \| \| \| \| \|