coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
\| \| \| \| \| \| \| \| *	[safe_string] lib/cThread	Emilio Jesus Gallego Arias	2017-03-14
* \| \| \| \| \| \| \| \|	Merge PR#438: Fix V7 syntax in refman.	Maxime Dénès	2017-03-14
\|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \	Merge PR#412: Remove outdated comment from 2002.	Maxime Dénès	2017-03-14
\|\ \ \ \ \ \ \ \ \ \ \| \|_\|_\|_\|_\|_\|_\|_\|_\|/ \|/\| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \|	Merge PR#432: [cleanup] Change Id.t option to Name.t in TacFun	Maxime Dénès	2017-03-14
\|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \	Merge PR#477: [travis] Basic support for overlays.	Maxime Dénès	2017-03-14
\|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \	Merge PR#473: [ci] Document that sudo: false is slower	Maxime Dénès	2017-03-14
\|\ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \	Merge PR#464: [META] More fixes	Maxime Dénès	2017-03-14
\|\ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR#446: Remove a dead exception catching code.	Maxime Dénès	2017-03-14
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| \| \| \| \| \| \| \| *	[future] Remove unused parameter greedy.	Emilio Jesus Gallego Arias	2017-03-14
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ \|/\| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| * \| \| \| \| \| \| \| \| \|	[travis] Basic support for overlays.	Emilio Jesus Gallego Arias	2017-03-13
\| \|_\|_\|/ / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \|
\| * \| \| \| \| \| \| \| \| \| \| \|	Remove a dead exception catching code.	Théo Zimmermann	2017-03-13
\|/ / / / / / / / / / / /
* \| \| \| \| \| \| \| \| \| \| \|	Merge PR#456: Proposing improvement to the CI targets for local use	Maxime Dénès	2017-03-13
\|\ \ \ \ \ \ \ \ \ \ \ \
* \| \| \| \| \| \| \| \| \| \| \| \|	Updating core.dbg after ltac moved to plugins directory.	Hugo Herbelin	2017-03-12
\| * \| \| \| \| \| \| \| \| \| \| \|	[travis] Make the git_checkout function more reliable.	Théo Zimmermann	2017-03-10
\| * \| \| \| \| \| \| \| \| \| \| \|	[travis] Adding a template file and using it for all targets.	Théo Zimmermann	2017-03-10
\| * \| \| \| \| \| \| \| \| \| \| \|	[travis] Change headband for wider compatibility.	Théo Zimmermann	2017-03-10
\| * \| \| \| \| \| \| \| \| \| \| \|	Improve build of travis target on local machine.	Théo Zimmermann	2017-03-10
\|/ / / / / / / / / / / /
\| \| * / / / / / / / / /	[ci] Document that sudo: false is slower	Tej Chajed	2017-03-10
\| \|/ / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \|
\| * \| \| \| \| \| \| \| \| \|	[META] [build] Install dlls to kernel/byterun	Emilio Jesus Gallego Arias	2017-03-10
\| * \| \| \| \| \| \| \| \| \|	[META] Ltac now a plugin.	Emilio Jesus Gallego Arias	2017-03-10
\| * \| \| \| \| \| \| \| \| \|	[META] Update version number.	Emilio Jesus Gallego Arias	2017-03-10
* \| \| \| \| \| \| \| \| \| \|	Merge PR#468: [travis] Fix GeoCoq and move it to allow fail.	Maxime Dénès	2017-03-10
\|\ \ \ \ \ \ \ \ \ \ \
* \| \| \| \| \| \| \| \| \| \| \|	Typo doc notations.	Hugo Herbelin	2017-03-09
* \| \| \| \| \| \| \| \| \| \| \|	Clarifying doc about interpretation of scopes in notations (#5386).	Hugo Herbelin	2017-03-09
\| * \| \| \| \| \| \| \| \| \| \|	[travis] Move GeoCoq to allow fail.	Emilio Jesus Gallego Arias	2017-03-09
\| \|/ / / / / / / / / /
* \| \| \| \| \| \| \| \| \| \|	Merge PR#318: Providing a file in the Logic library to work with extensional ...	Maxime Dénès	2017-03-09
\|\ \ \ \ \ \ \ \ \ \ \
* \| \| \| \| \| \| \| \| \| \| \|	Micromega: removing a constant preventing micromega to be loaded before Logic.v.	Hugo Herbelin	2017-03-09
* \| \| \| \| \| \| \| \| \| \| \|	Fixing dependency order of plugins.	Hugo Herbelin	2017-03-09
\| \|/ / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \|	Fixing Bug 5383 (Hyps Limit) + small refactoring.	Pierre Courtieu	2017-03-07
* \| \| \| \| \| \| \| \| \| \|	Merge PR#436: [ocamlbuild] Update META for the vernac split.	Maxime Dénès	2017-03-07
\|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \	Merge PR#447: [travis] [External CI] fiat-parsers	Maxime Dénès	2017-03-06
\|\ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \	Merge PR#279: A few lemmas about iff and about orders on positive and Z	Maxime Dénès	2017-03-06
\|\ \ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| * \| \| \| \| \| \| \| \| \|	CHANGES: choice over setoids and prop. ext.	Hugo Herbelin	2017-03-03
\| \| \| \| * \| \| \| \| \| \| \| \| \|	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
\| \|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / \|/\| \| \| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR#399: Debug by default	Maxime Dénès	2017-02-27
\|\ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR#395: Allow hintdb to be parameters in a Ltac definition or	Maxime Dénès	2017-02-27
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \