coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Merge branch 'origin/v8.5' into v8.6.	Hugo Herbelin	2017-04-06
\|\ \| \| \| \| \| \|	Was needed to be done for a while.
* \|	Fix 3 unused-intro-pattern warnings in stdlib.	Théo Zimmermann	2017-03-14
\| \|
\| *	Fixing a little bug in printing ex2 (type was printed "_" by default).	Hugo Herbelin	2017-02-23
\| \|
\| *	Fix some documentation typos.	Guillaume Melquiond	2016-12-26
\| \|
* \|	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 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
\|/ /
* \|	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.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
\| \| \|
* \| \|	Fixing unexpected "noise" introduced in commit 24d5448c.	Hugo Herbelin	2016-10-06
\| \| \| \| \| \| \| \| \| \| \| \|	A file was introduced by mistake in theories/Logic.
* \| \|	Clean up type classes flags and update compat file.	Maxime Dénès	2016-10-05
\| \| \|
\| * \|	Remove if_then_else. Use tryif instead.	Théo Zimmermann	2016-10-03
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	if_then_else definition does not account for multi success tactics. tryif_then_else is a primitive tactical with the expected behavior.
* \| \|	More tests for tactic "subst".	Hugo Herbelin	2016-10-02
\| \| \|
\| \| *	Move vector/list compat notations to their relevant files	Jason Gross	2016-09-29
\| \|/ \|/\| \| \| \| \| \| \| \| \| \| \|	Since edb55a94fc5c0473e57f5a61c0c723194c2ff414 landed, compat notations no longer modify the parser in non-compat-mode, so we can do this without breaking Ltac parsing. Also update the related test-suite files.
* \|	ZDivEucl: notations in different scope to avoid a warning	Pierre Letouzey	2016-09-28
\| \|
* \|	Remove spaces from around list notations	Jason Gross	2016-09-26
\| \|
* \|	Remove spaces from around vector notations	Jason Gross	2016-09-26
\| \|
* \|	Unbreak Ltac [ \| .. \| ] notation in -compat 8.5	Jason Gross	2016-09-26
\| \| \| \| \| \| \| \| \| \| \| \|	Importing VectorNotations breaks `; []`. So we make sure it's not imported by defualt. Some files might be required to `Import VectorDef.VectorNotations` rather than just `Import VectorNotations`.
* \|	Fix bug #4785 (use [ ] for vector nil)	Jason Gross	2016-09-26
\| \| \| \| \| \| \| \| \| \|	Also delimit vector_scope with vector, so that people can write %vector without having to delimit it themselves.
* \|	Further "decide equality" tests on demand of Jason.	Hugo Herbelin	2016-09-17
\| \|
* \|	Extending "contradiction" so that it recognizes statements such as "~x=x" or ↵	Hugo Herbelin	2016-09-15
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	~True. Found 1 incompatibility in tested contribs and 3 times the same pattern of incompatibility in the standard library. In all cases, it is an improvement in the form of the script. New behavior deactivated when version is <= 8.5.
* \|	Refolding: disable in 8.4 compat file, document	Matthieu Sozeau	2016-09-12
\| \|
* \|	no-refold patch	Paul Steckler	2016-09-09
\| \| \| \| \| \| \| \| \| \| \| \|	Add a boolean for refolding during reduction, and an option that is off by default in 8.6, to turn refolding on in all reduction functions, as in 8.5.
* \|	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot	2016-09-02
\|\\|
\| *	Fix bug #5043: [Admitted] lemmas pick up section variables.	Pierre-Marie Pédrot	2016-08-31
\| \| \| \| \| \| \| \| \| \| \| \|	We add a flag Keep Admitted Variables that allows to recover the legacy v8.4 behaviour of admitted lemmas. The statement of such lemmas did not depend on the current context variables.
* \|	Merge remote-tracking branch 'origin/pr/246' into v8.6	Matthieu Sozeau	2016-08-19
\|\ \
* \ \	Merge remote-tracking branch 'github/bug4978' into v8.6	Matthieu Sozeau	2016-08-18
\|\ \ \
* \| \| \|	Fix an occurrence of deprecated eqn syntax in stdlib.	Maxime Dénès	2016-08-18
\| \| \| \|
\| * \| \|	Fix #4978: priorities of Equivalence instances	Matthieu Sozeau	2016-08-17
\|/ / /
* \| \|	Replacing deprecated Implicit Arguments in prelude.	Maxime Dénès	2016-07-18
\| \| \| \| \| \| \| \| \| \| \| \|	Was triggering a deprecation warning.
* \| \|	Remove the swap tactic from the prelude.	Maxime Dénès	2016-07-18
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	It was anyway unusable due to a parsing conflict with the swap operator on goals. Was triggering a warning when compiling the prelude.
* \| \|	Fix bug #4923: Warning: appcontext is deprecated.	Pierre-Marie Pédrot	2016-07-18
\| \| \|
\| \| *	Typo.	Hugo Herbelin	2016-07-13
\| \| \|
* \| \|	Typo in a comment of stdlib.	Hugo Herbelin	2016-07-08
\| \| \|
\| * \|	Program: Move ProofIrrelevance to Subset.v	Matthieu Sozeau	2016-07-08
\| \| \|
* \| \|	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot	2016-07-07
\|\ \ \ \| \|/ / \|/\| / \| \|/
\| *	Merge remote-tracking branch 'github/pr/199' into v8.5	Maxime Dénès	2016-07-06
\| \|\ \| \| \| \| \| \| \| \| \|	Was PR#199: Unbreak singleton list-like notation (-compat 8.4)
* \| \|	Fix #4793: Coq 8.6 should accept -compat 8.6	Maxime Dénès	2016-07-06
\| \| \| \| \| \| \| \| \| \| \| \|	We also add a Coq86.v compat file.
\| * \|	Move option_map notation up	Jason Gross	2016-07-05
\| \| \| \| \| \| \| \| \|	This way, it's not eaten by a section
\| * \|	Restore option_map in FMapFacts	Jason Gross	2016-07-05
\| \| \| \| \| \| \| \| \|	This definition was removed by a4043608f704f026de7eb5167a109ca48e00c221 (This commit adds full universe polymorphism and fast projections to Coq), for reasons I do not know. This means that things like `unfold option_map` work only in 8.5, while `unfold <application of Facts>.option_map` works only in 8.4. This allows `unfold` to work correctly in both 8.4 and 8.5.
\| \| *	Compat84: Don't mess with stdlib modules	Jason Gross	2016-07-05
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	We don't actually need to, unless we want to support the (presumably uncommon) use-case of someone using [Import VectorNotations] to override their local notation for things in vector_scope. Additionally, we now maintain the behavior that [Import VectorNotations] opens vector_scope.
* \| \|	Typeclasses: use once in by clause for typeclass eauto	Matthieu Sozeau	2016-06-28
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Otherwise we may backtrack on the resolution in a by which seems strange.
* \| \|	Add Unset Shrink Abstract/Obligations in Coq85	Matthieu Sozeau	2016-06-27
\| \| \| \| \| \| \| \| \| \| \| \|	For compatibility with 8.5.