coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
* \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	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
\| \|/ / / / / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| * \| \| \|	Merge PR#452: [ltac] Move dummy plugin to plugins folder.	Maxime Dénès	2017-03-07
\| \| \| \| \| \| \| \| \| \| \| \|\ \ \ \
* \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Fixing Bug 5383 (Hyps Limit) + small refactoring.	Pierre Courtieu	2017-03-07
\| \| \| \| \| \| \| \| \| \| \| * \| \| \| \|	Merge PR#453: [travis] Backport trunk's travis support.	Maxime Dénès	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
\| \|_\|_\|_\|/ / / / / / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| * \| \|	[ltac] Move dummy plugin to plugins folder.	Emilio Jesus Gallego Arias	2017-03-03
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|/ / / \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|/\| \| \|
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| * \| \|	[travis] Backport trunk's travis support.	Emilio Jesus Gallego Arias	2017-03-02
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|/ / /
\| \| \| \| \| \| \| \| \| \| * \| \| \| \| \| \|	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
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| * \| \| \| \| \| \| \| \| \| \| \| \|	[travis] [External CI] fiat-parsers	Emilio Jesus Gallego Arias	2017-02-24
\| \| \| \| \|/ / / / / / / / / / / / /
\| \| \| \| \| \| \| \| \| \| \| \| * / / / /	TACTIC EXTEND now takes an optional level as argument.	Maxime Dénès	2017-02-24
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Revert "Add empty ltac_plugin file for forward compatibility."	Maxime Dénès	2017-02-24
\| \|_\|_\|/ / / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| * \| \| \| \| \| \|	Simplifying the proof of NoRetractToModalProposition.paradox in	Hugo Herbelin	2017-02-24
\| \|_\|_\|_\|_\|_\|_\|/ / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \| \| \| \|	Fixing #use"include" after vernac is added and ltac is moved to a plugin.	Hugo Herbelin	2017-02-23
* \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2017-02-22
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \| \| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / / \| \|/\| \| \| \| \| \| \| \| \| \| \| \|
\| * \| \| \| \| \| \| \| \| \| \| \| \|	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot	2017-02-22
\| \|\ \ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| \| \| \| \| * \| \| \|	Allow interactive editing of Coq.Init.Logic	Jason Gross	2017-02-21
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \| \| \| \|	[travis] track an 8.7 specific branch of HoTT.	Maxime Dénès	2017-02-21
* \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR#309: Ltac as a plugin	Maxime Dénès	2017-02-21
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \
\| \| * \| \| \| \| \| \| \| \| \| \| \| \|	Add empty ltac_plugin file for forward compatibility.	Maxime Dénès	2017-02-21
\| \| \| \| \| \| \| \| \| \| * \| \| \| \|	Fix V7 syntax in refman.	Théo Zimmermann	2017-02-20
\| \| \| \| \| * \| \| \| \| \| \| \| \| \|	Deprecate -debug flag.	Maxime Dénès	2017-02-20
* \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR#189: Remove tabulation support from pretty-printing.	Maxime Dénès	2017-02-20
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| * \| \| \| \| \| \|	Merge pull request #4 from Zimmi48/patch-1	Emilio Jesús Gallego Arias	2017-02-20
\| \| \| \| \| \| \| \| \|\ \ \ \ \ \ \
\| \| \| \| \| \| \| \| \| * \| \| \| \| \| \|	[ocamlbuild] fix small mistakes in descriptions	Théo Zimmermann	2017-02-20
\| \| \| \| \| \| \| \| \|/ / / / / / /
\| \| \| \| \| \| \| \| * \| \| \| \| \| \|	[ocamlbuild] Update meta for the vernac split.	Emilio Jesus Gallego Arias	2017-02-20
* \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Fixing debugger after the split of toplevel into vernac.	Pierre-Marie Pédrot	2017-02-19
\| \|_\|_\|_\|_\|_\|_\|/ / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \|