coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge PR#373: A refined solution to the beta-iota discrepancies between 8.4 a...	Maxime Dénès	2017-05-11
\|\
* \	Merge PR#572: Replacing costly merges in UGraph.	Maxime Dénès	2017-05-11
\|\ \
* \| \|	Remove an unused open introduced by the previous commit.	Maxime Dénès	2017-05-11
* \| \|	Merge PR#201: Transparent abstract	Maxime Dénès	2017-05-11
\|\ \ \
* \ \ \	Merge PR#619: Fix warnings in top_printers	Maxime Dénès	2017-05-09
\|\ \ \ \
* \ \ \ \	Merge PR#612: Set Ltac Batch Debug	Maxime Dénès	2017-05-09
\|\ \ \ \ \
* \ \ \ \ \	Merge PR#606: Added an option Set Debug Cbv	Maxime Dénès	2017-05-09
\|\ \ \ \ \ \
* \ \ \ \ \ \	Merge PR#621: Prevent user-defined ring morphisms from ever being evaluated.	Maxime Dénès	2017-05-09
\|\ \ \ \ \ \ \
* \ \ \ \ \ \ \	Merge PR#615: coqtop -help: don't die if coqlib can't be found	Maxime Dénès	2017-05-09
\|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \	Merge PR#617: [toplevel] Fix a couple of logical errors in error printing.	Maxime Dénès	2017-05-09
\|\ \ \ \ \ \ \ \ \
\| \| \| * \| \| \| \| \| \|	Prevent user-defined ring morphisms from ever being evaluated.	Guillaume Melquiond	2017-05-09
\| \|_\|/ / / / / / / \|/\| \| \| \| \| \| \| \|
\| \| \| \| \| * \| \| \|	Fix warnings in top_printers	Gaetan Gilbert	2017-05-08
\| \|_\|_\|_\|/ / / / \|/\| \| \| \| \| \| \|
\| * \| \| \| \| \| \|	[toplevel] Fix a couple of logical errors in error printing.	Emilio Jesus Gallego Arias	2017-05-05
\|/ / / / / / /
* \| \| \| \| \| \|	Remove dead code and unused open.	Maxime Dénès	2017-05-05
* \| \| \| \| \| \|	Merge PR#558: Adding a fold_glob_constr_with_binders combinator	Maxime Dénès	2017-05-05
\|\ \ \ \ \ \ \
* \| \| \| \| \| \| \|	Remove two unused opens.	Maxime Dénès	2017-05-05
* \| \| \| \| \| \| \|	Merge PR#598: Removing dead code in Autorewrite.	Maxime Dénès	2017-05-05
\|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \	Merge PR#610: Improve documentation of assert / pose proof / specialize.	Maxime Dénès	2017-05-05
\|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \	Merge PR#605: Report a useful error for dependent induction	Maxime Dénès	2017-05-05
\|\ \ \ \ \ \ \ \ \ \
\| \| \| \| \| * \| \| \| \| \|	coqtop -help: don't die if coqlib can't be found	Gaetan Gilbert	2017-05-05
\| \|_\|_\|_\|/ / / / / / \|/\| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \|	Merge PR#454: Printing unfocussed goals and toward a pg plugin.	Maxime Dénès	2017-05-05
\|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \	Merge PR#593: Functional choice <-> [inhabited] and [forall] commute	Maxime Dénès	2017-05-05
\|\ \ \ \ \ \ \ \ \ \ \
* \| \| \| \| \| \| \| \| \| \| \|	Remove unused open.	Maxime Dénès	2017-05-05
* \| \| \| \| \| \| \| \| \| \| \|	Merge PR#544: Anonymous universes	Maxime Dénès	2017-05-05
\|\ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| \| \| * \| \| \|	Adding an option "Set Ltac Batch Debug" to additionally run Ltac debug in bat...	Hugo Herbelin	2017-05-04
\| \|_\|_\|_\|_\|_\|_\|_\|/ / / / \|/\| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| * \| \| \| \| \| \|	Improve documentation of assert / pose proof / specialize.	Théo Zimmermann	2017-05-04
\| \|_\|_\|_\|/ / / / / / / \|/\| \| \| \| \| \| \| \| \| \|
\| \| \| * \| \| \| \| \| \| \|	Warning removed.	Pierre Courtieu	2017-05-04
\| \| \| * \| \| \| \| \| \| \|	labelizing arguments	Pierre Courtieu	2017-05-04
\| \| \| * \| \| \| \| \| \| \|	Adding an option "Printing Unfocused".	Pierre Courtieu	2017-05-04
\| \|_\|/ / / / / / / / \|/\| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \|	Merge PR#541: Fixing "decide equality" bug #5449	Maxime Dénès	2017-05-03
\|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \	Merge PR#588: Allow interactive editing of {C,}Morphisms in PG	Maxime Dénès	2017-05-03
\|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \	Merge PR#386: Better editing of the standard library in coqtop/PG	Maxime Dénès	2017-05-03
\|\ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \	Merge PR#602: Fix more warnings	Maxime Dénès	2017-05-03
\|\ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR#404: patch for printing types of let bindings	Maxime Dénès	2017-05-03
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| \| \| \| \| * \| \| \|	Added an option Set Debug Cbv.	Hugo Herbelin	2017-05-03
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| * \| \| \| \| \|	Report a useful error for dependent induction	Tej Chajed	2017-05-03
\| \|_\|_\|_\|_\|_\|_\|/ / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| * \| \| \| \| \|	Reorganize comment documentation of ChoiceFacts.v	Gaetan Gilbert	2017-05-03
\| \| \| \| \| \| * \| \| \| \| \| \|	Type@{_} should not produce a flexible algebraic universe.	Gaetan Gilbert	2017-05-03
\| \| \| \| \| \| * \| \| \| \| \| \|	Allow flexible anonymous universes in instances and sorts.	Gaetan Gilbert	2017-05-03
* \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR#411: Mention template polymorphism in the documentation.	Maxime Dénès	2017-05-03
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \| \|_\|_\|_\|_\|_\|/ / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \|
\| \| * \| \| \| \| \| \| \| \| \| \|	applied the patch for printing types of let bindings by @herbelin	Abhishek Anand (@brixpro-home)	2017-05-02
\| \|/ / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \|
\| \| * \| \| \| \| \| \| \| \| \|	Remove dead code in native compiler.	Maxime Dénès	2017-05-02
\| \| * \| \| \| \| \| \| \| \| \|	Fix two new unused opens.	Maxime Dénès	2017-05-02
\| \| * \| \| \| \| \| \| \| \| \|	Remove unused module definition after merging PR#592.	Maxime Dénès	2017-05-02
\| \|/ / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \|	Merge PR#592: Fix bug #5501: Universe polymorphism breaks proof involving auto.	Maxime Dénès	2017-05-02
\|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \	Merge PR#582: Fix warnings	Maxime Dénès	2017-05-02
\|\ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \	Merge PR#596: Fix for bug 5507. Mispelt de Bruijn.	Maxime Dénès	2017-05-02
\|\ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR#595: Avoiding registering files from _build_ci for computing depende...	Maxime Dénès	2017-05-02
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \
\| \| * \| \| \| \| \| \| \| \| \| \| \| \|	More consistent writing of de Bruijn.	Théo Zimmermann	2017-05-01
\| \| \| \| \| \| \| \| \| \| * \| \| \| \|	Removing dead code in Autorewrite.	Pierre-Marie Pédrot	2017-05-01
\| \|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \|