coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Stop using auto with * in two proofs.	Théo Zimmermann	2017-05-16
*	Merge PR#201: Transparent abstract	Maxime Dénès	2017-05-11
\|\
* \	Merge PR#605: Report a useful error for dependent induction	Maxime Dénès	2017-05-05
\|\ \
* \ \	Merge PR#593: Functional choice <-> [inhabited] and [forall] commute	Maxime Dénès	2017-05-05
\|\ \ \
* \ \ \	Merge PR#588: Allow interactive editing of {C,}Morphisms in PG	Maxime Dénès	2017-05-03
\|\ \ \ \
* \ \ \ \	Merge PR#386: Better editing of the standard library in coqtop/PG	Maxime Dénès	2017-05-03
\|\ \ \ \ \
\| \| \| \| * \|	Report a useful error for dependent induction	Tej Chajed	2017-05-03
\| \|_\|_\|/ / \|/\| \| \| \|
\| \| \| * \|	Reorganize comment documentation of ChoiceFacts.v	Gaetan Gilbert	2017-05-03
\| \| \| * \|	Functional choice <-> [inhabited] and [forall] commute	Gaetan Gilbert	2017-04-30
\| \|_\|/ / \|/\| \| \|
* \| \| \|	Suppress warning message in stdlib.	Guillaume Melquiond	2017-04-29
\| \| * \|	Allow interactive editing of {C,}Morphisms in PG	Jason Gross	2017-04-28
\| \|/ / \|/\| \|
\| * \|	Add .dir-locals.el and _CoqProject files for emacs stdlib editing	Jason Gross	2017-04-28
\|/ /
* \|	Merge PR#414: Some more theory on powerRZ.	Maxime Dénès	2017-04-27
\|\ \
* \ \	Merge PR#584: Give andb_prop a simpler proof	Maxime Dénès	2017-04-27
\|\ \ \
* \| \| \|	Small typo in comment	Vadim Zaliva	2017-04-26
\| \| \| *	Add transparent_abstract tactic	Jason Gross	2017-04-25
\| \|_\|/ \|/\| \|
\| * \|	Give andb_prop a simpler proof	Jason Gross	2017-04-25
\|/ /
* \|	Merge PR#545: Add some hints to the "real" database to automatically discharg...	Maxime Dénès	2017-04-19
\|\ \
* \ \	Merge branch 'v8.6' into trunk	Maxime Dénès	2017-04-15
\|\ \ \
\| \| * \|	Add some hints to the "real" database to automatically discharge literal comp...	Guillaume Melquiond	2017-04-07
\| \|/ / \|/\| \|
* \| \|	Merge PR#455: Farewell decl_mode	Maxime Dénès	2017-04-06
\|\ \ \
\| \| * \	Merge branch 'origin/v8.5' into v8.6.	Hugo Herbelin	2017-04-06
\| \| \|\ \
* \| \| \| \|	Fix documentation typo (bug #5433).	Guillaume Melquiond	2017-04-02
* \| \| \| \|	Simplify some proofs.	Guillaume Melquiond	2017-04-02
* \| \| \| \|	Fix ring_simplify sometimes producing R0 and R1 instead of 0%R and 1%R.	Guillaume Melquiond	2017-03-30
* \| \| \| \|	Merge PR#469: Added take to VectorDef	Maxime Dénès	2017-03-30
\|\ \ \ \ \
\| * \| \| \| \|	Added take to VectorDef.	George Stelle	2017-03-30
* \| \| \| \| \|	Fixing missing PropFacts.v in Logic/vo.itarget.	Hugo Herbelin	2017-03-28
* \| \| \| \| \|	Merge PR#392: strengthened the statement of JMeq_eq_dep	Maxime Dénès	2017-03-24
\|\ \ \ \ \ \
* \ \ \ \ \ \	Merge branch 'v8.6' into trunk	Maxime Dénès	2017-03-23
\|\ \ \ \ \ \ \ \| \| \|_\|_\|/ / / \| \|/\| \| \| \| \|
* \| \| \| \| \| \|	Make IZR a morphism for field.	Guillaume Melquiond	2017-03-22
* \| \| \| \| \| \|	Change the parser and printer so that they use IZR for real constants.	Guillaume Melquiond	2017-03-22
* \| \| \| \| \| \|	Make IZR use a compact representation of integers.	Guillaume Melquiond	2017-03-22
* \| \| \| \| \| \|	Simplify some proofs using ring and field.	Guillaume Melquiond	2017-03-22
* \| \| \| \| \| \|	Add a forgotten (?) line to "theories/Logic/vo.itarget".	Matej Kosik	2017-03-19
* \| \| \| \| \| \|	Merge PR#442: Allow interactive editing of Coq.Init.Logic	Maxime Dénès	2017-03-17
\|\ \ \ \ \ \ \
* \ \ \ \ \ \ \	Merge PR#451: Add η principles for sigma types	Maxime Dénès	2017-03-17
\|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \	Merge PR#444: Simplifying a statement in Hurkens.v + a case study for eauto	Maxime Dénès	2017-03-14
\|\ \ \ \ \ \ \ \ \ \| \|_\|_\|_\|_\|/ / / / \|/\| \| \| \| \| \| \| \|
\| \| \| \| * \| \| \| \|	Fix 3 unused-intro-pattern warnings in stdlib.	Théo Zimmermann	2017-03-14
* \| \| \| \| \| \| \| \|	Merge PR#318: Providing a file in the Logic library to work with extensional ...	Maxime Dénès	2017-03-09
\|\ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| * \| \|	Farewell decl_mode	Enrico Tassi	2017-03-07
\| \|_\|_\|_\|_\|_\|/ / / \|/\| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \|	Merge PR#279: A few lemmas about iff and about orders on positive and Z	Maxime Dénès	2017-03-06
\|\ \ \ \ \ \ \ \ \
\| \| * \| \| \| \| \| \| \|	Strengthening some of the results in ChoiceFacts.v.	Hugo Herbelin	2017-03-03
\| \| * \| \| \| \| \| \| \|	Adding explicitly a file to work in the context of propositional extensionality.	Hugo Herbelin	2017-03-03
\| \| * \| \| \| \| \| \| \|	Adding a file providing extensional choice (i.e. choice over setoids).	Hugo Herbelin	2017-03-03
\| \| * \| \| \| \| \| \| \|	Adding various properties and characterization of the extensional	Hugo Herbelin	2017-03-03
\| \| * \| \| \| \| \| \| \|	Slightly unifying renaming in ChoiceFacts.v.	Hugo Herbelin	2017-03-03
\| \| * \| \| \| \| \| \| \|	Logic library: Adding a characterization of excluded-middle in term of	Hugo Herbelin	2017-03-03
* \| \| \| \| \| \| \| \| \|	Merge PR#273: Tidy stdlib	Maxime Dénès	2017-03-03
\|\ \ \ \ \ \ \ \ \ \
\| \| * \| \| \| \| \| \| \| \|	Completing basic lemmas about <= and < in BinInt.Z.Pos2Z.	Hugo Herbelin	2017-03-03