coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
\| \| \| * \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	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
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| \| \| \| \| * \| \| \| \| \| \|	Fix bug #3659: -time should understand multibyte encodings.	Pierre-Marie Pédrot	2017-05-05
\| \| \| \| \| \| \| \| \| \| \|/ / / / / / /
\| \| \| \| \| \| \| \| \| * \| \| \| \| \| \| \|	Documenting Option.List.find.	Hugo Herbelin	2017-05-05
\| \| \| \| \| \| \| \| \| * \| \| \| \| \| \| \|	Cosmetic: unifying style within option.ml.	Hugo Herbelin	2017-05-05
\| \| \| \| \| \| \| \| \| * \| \| \| \| \| \| \|	Upgrading some local function as a general-purpose combinator Option.List.map.	Hugo Herbelin	2017-05-05
\| \| \| \| \| \| \| \| \| * \| \| \| \| \| \| \|	Adding a test-suite pattern-unification example that Econstr fixed.	Hugo Herbelin	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
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| * \| \|	Adapted to EConstr.	Pierre Courtieu	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
\| \|_\|/ / / / / / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| \| * \| \| \| \|	FIx bug #5300: uncaught exception in "Print Assumptions".	Cyprien Mangin	2017-05-03
\| \| \| \| \| \| \| \| \| \| \| \|/ / / / / \| \| \| \| \| \| \| \| \| \| \|/\| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	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
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| * \| \| \|	Make congruence reuse discriminate instead of rolling its own.	Gaetan Gilbert	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
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| * \| \| \| \|	Merge PR#603: Fix outdated description in RefMan.	Maxime Dénès	2017-05-03
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|\ \ \ \ \
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| * \| \|	Adding an even more compact mode for goal display.	Pierre Courtieu	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
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \| \|_\|_\|_\|_\|_\|/ / / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| \| \| \| * \| \| \|	Fix outdated description in RefMan.	Théo Zimmermann	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#597: Fixing #5487 (v8.5 regression on ltac-matching expressions with...	Maxime Dénès	2017-05-02
\| \| \| \| \| \| \| \| \| \| \| \| \|\ \ \ \
* \| \| \| \| \| \| \| \| \| \| \| \| \ \ \ \	Merge PR#582: Fix warnings	Maxime Dénès	2017-05-02
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| \| \| \| \| \| \| * \ \ \ \	Merge PR#589: remove unneeded -emacs flag in coq-prog-args in test-suite files	Maxime Dénès	2017-05-02
\| \| \| \| \| \| \| \| \| \| \| \| \| \|\ \ \ \ \
\| \| \| \| \| \| \| \| \| \| \| \| \| * \ \ \ \ \	Merge PR#599: Repairing `Set Rewriting Schemes`	Maxime Dénès	2017-05-02
\| \| \| \| \| \| \| \| \| \| \| \| \| \|\ \ \ \ \ \