coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	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).
*	Formatting references with surrounding brackets in Diaconescu.v.	Hugo Herbelin	2017-03-03
\|
*	Fix a typo in Hurkens.v comment	Jason Gross	2016-12-19
\|
*	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-11-18
\|\
\| *	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.
* \|	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
\|\\|
\| *	More tests for tactic "subst".	Hugo Herbelin	2016-10-02
\| \|
* \|	extensionality: Handle dependently-used hypotheses	Jason Gross	2016-09-19
\| \|
* \|	Adding an "extensionality in H" tactic which applies functional	Hugo Herbelin	2016-09-19
\|/ \| \| \| \| \| \| \|	extensionality in H supposed to be a quantified equality until giving a bare equality. Thanks to Jason Gross and Jonathan Leivent for suggestions and examples.
*	Typo in a comment of stdlib.	Hugo Herbelin	2016-07-08
\|
*	Moving the Tauto tactic to proper Ltac.	Pierre-Marie Pédrot	2016-02-22
\| \| \| \| \| \|	This gets rid of brittle code written in ML files through Ltac quotations, and reduces the dependance of Coq to such a feature. This also fixes the particular instance of bug #2800, although the underlying issue is still there.
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-29
\|\
\| *	Fix bug #4503: mixing universe polymorphic and monomorphic	Matthieu Sozeau	2016-01-23
\| \| \| \| \| \| \| \|	variables and definitions in sections is unsupported.
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-21
\|\\|
\| *	Update copyright headers.	Maxime Dénès	2016-01-20
\| \|
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-12-17
\|\\|
\| *	Refine tactic now shelves unifiable holes.	Pierre-Marie Pédrot	2015-12-15
\| \| \| \| \| \| \| \| \| \| \| \|	The unshelve tactical can be used to get the shelved holes. This changes the proper ordering of holes though, so expect some broken scripts. Also, the test-suite is not fixed yet.
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-12-11
\|\\|
\| *	Changing syntax of pat/constr1.../constrn into pat%constr1...%constrn.	Hugo Herbelin	2015-12-10
\| \| \| \| \| \| \| \|	Marking it as experimental.
* \|	Fix to previous commit (ClassicalFacts.v).	Hugo Herbelin	2015-12-05
\| \|
* \|	Adding proofs on the relation between excluded-middle and minimization.	Hugo Herbelin	2015-12-05
\| \| \| \| \| \| \| \| \| \| \| \| \| \|	In particular, a proof of the equivalence of excluded-middle and an unrestricted principle of minimization. Credits to Arnaud Spiwack for the ideas and formalizations of the proofs.
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-11-29
\|\\|
\| *	Univs: entirely disallow instantiation of polymorphic constants with	Matthieu Sozeau	2015-11-27
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Prop levels. As they are typed assuming all variables are >= Set now, and this was breaking an invariant in typing. Only one instance in the standard library was used in Hurkens, which can be avoided easily. This also avoids displaying unnecessary >= Set constraints everywhere.
* \|	Adding an amazing property of Prop.	Hugo Herbelin	2015-11-07
\|/
*	Minor modifications to WeakFanTheorem.	Hugo Herbelin	2015-09-08
\|
*	Remove some outdated files and fix permissions.	Guillaume Melquiond	2015-07-31
\|
*	Update headers.	Maxime Dénès	2015-01-12
\|
*	Added an arithmetical characterization of the hypothesis of WKL.	Hugo Herbelin	2014-12-01
\|
*	Improving elimination with indices, getting rid of intrusive residual	Hugo Herbelin	2014-11-02
\| \| \| \|	local definitions...
*	Make sure that Logic/ExtensionalityFacts gets compiled.	Guillaume Melquiond	2014-10-27
\|
*	Fix some typos.	Guillaume Melquiond	2014-10-27
\|
*	Fix some typos in comments.	Guillaume Melquiond	2014-10-27
\|
*	EqdepFacts: generalize statements which were wrongly restricted to Prop.	Arnaud Spiwack	2014-10-22
\|
*	ConstructiveEpsilon: simplify the before_witness type using non-uniform ↵	Arnaud Spiwack	2014-10-16
\| \| \| \|	parameters.
*	Hurkens.v: Fix a syntax error.	Arnaud Spiwack	2014-09-26
\| \| \|	Introduced in c74a70a73b3bf39394c551f1cdb224450bf77176.
*	ClassicalFacts: adds a proof that weak excluded middle implies weak proof ↵	Arnaud Spiwack	2014-09-26
\| \| \| \| \|	irrelevance. Application of previous commit in Hurkens.v.
*	Hurkens.v: new paradox: type of modal propositions is not a retract.	Arnaud Spiwack	2014-09-26
\| \| \|	In particular there is no retract of the type of negative propositions in a negative proposition.
*	Hurkens.v: fix coqdoc formatting in a comment.	Arnaud Spiwack	2014-09-26
\|
*	Hurkens.v: update comments.	Arnaud Spiwack	2014-09-25
\|
*	Return a Prop not an arbitrary Type, and correct a typo.	Matthieu Sozeau	2014-09-24
\|
*	Hurkens.v: show proofs in coqdoc.	Arnaud Spiwack	2014-09-24
\|
*	Hurkens.v: a proof of [Type@{i}<>A] for any [A:Type@{i}].	Arnaud Spiwack	2014-09-24
\|
*	Hurkens.v: coqdoc documentation.	Arnaud Spiwack	2014-09-24
\|