coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
* \| \| \| \|	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
\| \| * \| \| \| \| \| \| \| \|	Relying on BinInt.Z.Pos2Z for proofs of a few lemmas in Zorder.	Hugo Herbelin	2017-03-03
\| \| * \| \| \| \| \| \| \| \|	Completing "few lemmas about Zneg" with lemmas also about Zpos.	Hugo Herbelin	2017-03-03
\| \| * \| \| \| \| \| \| \| \|	A couple of other useful properties about compare_cont.	Hugo Herbelin	2017-03-03
\| \| * \| \| \| \| \| \| \| \|	Compatibility of iff wrt not and imp.	Hugo Herbelin	2017-03-03
\| \|/ / / / / / / / / \|/\| \| \| \| \| \| \| \| \|
\| \| * \| \| \| \| \| \| \|	Formatting references with surrounding brackets in Diaconescu.v.	Hugo Herbelin	2017-03-03
\| \|/ / / / / / / / \|/\| \| \| \| \| \| \| \|
\| \| \| * \| \| \| \| \|	Add η principles for sigma types	Jason Gross	2017-03-01
\| \| \| * \| \| \| \| \|	Remove some trailing whitespace in Init/Specif.v	Jason Gross	2017-03-01
\| \|_\|/ / / / / / \|/\| \| \| \| \| \| \|
\| \| * \| \| \| \| \|	Simplifying the proof of NoRetractToModalProposition.paradox in	Hugo Herbelin	2017-02-24
\| \|/ / / / / / \|/\| \| \| \| \| \|
\| \| \| \| \| * \|	Fixing a little bug in printing ex2 (type was printed "_" by default).	Hugo Herbelin	2017-02-23
\| \| * \| \| \| \|	Allow interactive editing of Coq.Init.Logic	Jason Gross	2017-02-21
\| \|/ / / / / \|/\| \| \| \| \|
* \| \| \| \| \|	Ltac as a plugin.	Pierre-Marie Pédrot	2017-02-17
\| \| \| \| \| *	Added some theory on powerRZ.	Thomas Sibut-Pinote	2017-02-15
\| \|_\|_\|_\|/ \|/\| \| \| \|
\| * \| \| \|	Proof clean-up.	Théo Zimmermann	2017-01-30
\|/ / / /
\| \| \| *	Fix some documentation typos.	Guillaume Melquiond	2016-12-26
* \| \| \|	Fix a typo in Hurkens.v comment	Jason Gross	2016-12-19
\| \| * \|	strengthened the statement of JMeq_eq_dep	Abhishek Anand	2016-12-11
\| \|/ / \|/\| \|
* \| \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-11-30
\|\\| \|
\| * \|	Fix some documentation typos.	Guillaume Melquiond	2016-11-24
\| * \|	Fix some documentation typos.	Guillaume Melquiond	2016-11-24
* \| \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-11-18
\|\\| \|
\| * \|	Merge commit 'e6edb33' into v8.6	Maxime Dénès	2016-11-07
\| \|\ \
\| \| * \|	More explicit name for status of unification constraints.	Maxime Dénès	2016-11-07
\| * \| \|	Merge remote-tracking branch 'github/pr/336' into v8.6	Maxime Dénès	2016-11-04
\| \|\ \ \
\| * \| \| \|	Silence option deprecation warnings in the compat file	Jason Gross	2016-11-04
\| \| * \| \|	Remove v62 from stdlib.	Théo Zimmermann	2016-10-24
\| \|/ / /