coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
...
* \| \| \| \| \| \| \|	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
\|\ \ \ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	choice
\| \| \| \| \| \| \| * \| \|	Farewell decl_mode	Enrico Tassi	2017-03-07
\| \|_\|_\|_\|_\|_\|/ / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This commit removes from the source tree plugins/decl_mode, its chapter in the reference manual and related tests.
* \| \| \| \| \| \| \| \|	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
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Further highlighting when the correspondence between variants of choice is independent of the domain and codomain of the function, as was done already done in the beginning of the file (suggestion from Jason). Adding some corollaries.
\| \| * \| \| \| \| \| \| \|	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
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Also integrating suggestions from Théo.
\| \| * \| \| \| \| \| \| \|	Adding various properties and characterization of the extensional	Hugo Herbelin	2017-03-03
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	axiom of choice (i.e. choice on setoids) and of the axiom selecting representatives in classes of equivalence. Also integrating suggestions from Théo.
\| \| * \| \| \| \| \| \| \|	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
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	choice of a representative in a partition of bool. Also move a result about propositional extensionality from ClassicalFacts.v to PropExtensionalityFacts.v, generalizing it by symmetry. Also spotting typos (thanks to Théo).
* \| \| \| \| \| \| \| \| \|	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
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Don't know if compare_cont is very useful to use, but, at least, these extensions make sense.
\| \| * \| \| \| \| \| \| \| \|	Compatibility of iff wrt not and imp.	Hugo Herbelin	2017-03-03
\| \|/ / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This completes the series and cannot hurt.
\| \| * \| \| \| \| \| \| \|	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
\| \|/ / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Hurkens.v by dropping the artificial need for monad laws. Tactic eauto decided to be dependent on the laws but there is a shorter proof without them. [Interestingly, eauto is not able to find the short proof. This is a situation of the form subgoal 1: H : ?A \|- P x subgoal 2: H : M ?A \|- M (forall x, P x) where addressing the second subgoal would find the right instance of ?A, but this instance is too hard to find by addressing first the first subgoal.]
\| \| \| \| \| * \|	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
\| \|/ / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Without this change, coqtop complains that I need to require Coq.Init.Logic to use [replace ... with ... by ...].
* \| \| \| \| \|	Ltac as a plugin.	Pierre-Marie Pédrot	2017-02-17
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This commit is essentially moving files around. In particular, the corresponding plugin still relies on a mllib file rather than a mlpack one. Otherwise, this causes link-time issues for third-party plugins depending on modules defined in the Ltac plugin.
\| \| \| \| \| *	Added some theory on powerRZ.	Thomas Sibut-Pinote	2017-02-15
\| \|_\|_\|_\|/ \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \|	For this, I used a new inductive type Z_spec to reason on Z.
\| * \| \| \|	Proof clean-up.	Théo Zimmermann	2017-01-30
\|/ / / / \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	- Do not use induction/elim when not necessary: use destruct or destructive intro-pattern instead. - Do not use heavy automation when lightweight automation is enough. - Prefer shorter proofs when it does not hinder readability. - Do not rely on automatically generated names. - Use bullets.
\| \| \| *	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
\| \|/ / \|/\| \| \| \| \| \| \| \|	because P:U->Prop implies P:U->Type, the new statement is strictly more useful. No change was needed to the proof.
* \| \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-11-30
\|\\| \|
\| * \|	Fix some documentation typos.	Guillaume Melquiond	2016-11-24
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Note: "dependant" does exist, but it is a noun and it means a person that is somehow financially dependent on someone else.
\| * \|	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
\| \|\ \ \| \| \| \| \| \| \| \| \| \| \| \|	Was PR#331: Solve_constraints and Set Use Unification Heuristics
\| \| * \|	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
\| \|\ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Was PR#336: Remove v62
\| * \| \| \|	Silence option deprecation warnings in the compat file	Jason Gross	2016-11-04
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Some options are expected to be deprecated
\| \| * \| \|	Remove v62 from stdlib.	Théo Zimmermann	2016-10-24
\| \|/ / / \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This old compatibility hint database can be safely removed now that coq-contribs do not depend on it anymore.
\| \| * /	Add Unset Use Unif Heuristics in Compat/Coq85	Matthieu Sozeau	2016-10-22
\| \|/ /
* \| \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-10-17
\|\\| \|
\| * \|	Fix previous commit.	Pierre-Marie Pédrot	2016-10-17
\| \| \| \| \| \| \| \| \| \| \| \|	I've messed up with parts of the compatibility files I had to commit.
\| * \|	Merge PR #300 into v8.6	Pierre-Marie Pédrot	2016-10-17
\| \|\ \
* \| \| \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-10-12
\|\\| \| \|
\| * \| \|	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot	2016-10-12
\| \|\ \ \ \| \| \| \|/ \| \| \|/\|
\| * \| \|	Little addition to 6eede071 for consistency of style in OrdersFacts.v.	Hugo Herbelin	2016-10-12
\| \| \| \|
* \| \| \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-10-08
\|\\| \| \|
\| * \| \|	Fixing unexpected "noise" introduced in commit 24d5448c.	Hugo Herbelin	2016-10-06
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	A file was introduced by mistake in theories/Logic.
* \| \| \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-10-05
\|\\| \| \|
\| * \| \|	Clean up type classes flags and update compat file.	Maxime Dénès	2016-10-05
\| \| \| \|