coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge PR #6576: generate both binary and text annotations	Maxime Dénès	2018-01-22
\|\
* \	Merge PR #6550: Remove outdated note about rlwrap in setup.txt	Maxime Dénès	2018-01-22
\|\ \
* \ \	Merge PR #6618: Fix Ltac subterm matching in (co-)fixpoints.	Maxime Dénès	2018-01-22
\|\ \ \
* \ \ \	Merge PR #6575: Add flash infos for find and replace	Maxime Dénès	2018-01-22
\|\ \ \ \
* \ \ \ \	Merge PR #6506: Fast rel lookup	Maxime Dénès	2018-01-22
\|\ \ \ \ \
\| \| \| \| \| *	-annotate deprecated. New options: -annot, -bin-annot	Vadim Zaliva	2018-01-19
\| \| \| * \| \|	Add test-suite file for issue #6617.	Cyprien Mangin	2018-01-19
\| \| \| * \| \|	Fix context handling of fix and cofix in Ltac subterm matching.	Cyprien Mangin	2018-01-19
\| \| \| * \| \|	Define EConstr version of [push_rec_types].	Cyprien Mangin	2018-01-19
\| \| * \| \| \|	add flash infos about wrap, not found, no. of replacements, no. of finds, iss...	Paul Steckler	2018-01-18
\| \|/ / / / \|/\| \| \| \|
* \| \| \| \|	Merge PR #6555: Use let-in aware prod_applist_assum in dtauto and firstorder.	Maxime Dénès	2018-01-18
\|\ \ \ \ \
* \ \ \ \ \	Merge PR #6448: Cleanup and add debug printers a bit	Maxime Dénès	2018-01-18
\|\ \ \ \ \ \ \| \|_\|_\|/ / / \|/\| \| \| \| \|
* \| \| \| \| \|	Merge PR #6600: Update configure.ml to only warn on lablgtk >= 2.16.0 and < 2...	Maxime Dénès	2018-01-17
\|\ \ \ \ \ \
* \ \ \ \ \ \	Merge PR #6593: Add plugins to META.coq	Maxime Dénès	2018-01-17
\|\ \ \ \ \ \ \
* \ \ \ \ \ \ \	Merge PR #6298: Fix #6297: handle constraints like (u+1 <= Set/Prop)	Maxime Dénès	2018-01-17
\|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \	Merge PR #6584: Implement the strategy mechanism in the checker	Maxime Dénès	2018-01-17
\|\ \ \ \ \ \ \ \ \
\| \| \| \| \| \| * \| \| \|	Add CHANGES entry	Jasper Hugunin	2018-01-17
\| \| \| \| \| \| * \| \| \|	Add a test that `prod_applist_assum` reduces the right number of let-ins	Jasper Hugunin	2018-01-17
\| \| \| \| \| \| * \| \| \|	Use let-in aware prod_applist_assum in dtauto and firstorder.	Jasper Hugunin	2018-01-17
\| \| \| \| * \| \| \| \| \|	Update lablgtk check to be more general	Jason Gross	2018-01-16
\| \| \| * \| \| \| \| \| \|	Rename coq.ltac to coq.plugins.ltac in META.coq	Cyprien Mangin	2018-01-16
\| \| \| \| * \| \| \| \| \|	Update configure.ml to only warn on lablgtk 2.16.0	Jason Gross	2018-01-16
\| \| \| \| \| \|/ / / / \| \| \| \| \|/\| \| \| \|
* \| \| \| \| \| \| \| \|	Merge PR #6590: Fix the wrapper around ocamldebug.	Maxime Dénès	2018-01-16
\|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \	Merge PR #6499: [vernac] Move the flags/attributes out of vernac_expr	Maxime Dénès	2018-01-16
\|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \	Merge PR #6466: Replace md5sum/md5 calls by an OCaml program	Maxime Dénès	2018-01-16
\|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \	Merge PR #6551: Bracket with goal selector	Maxime Dénès	2018-01-16
\|\ \ \ \ \ \ \ \ \ \ \ \ \| \|_\|_\|_\|_\|_\|_\|/ / / / / \|/\| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| * \| \| \| \|	Add plugins to META.coq	Cyprien Mangin	2018-01-16
\| \|_\|_\|_\|_\|_\|/ / / / / \|/\| \| \| \| \| \| \| \| \| \|
\| \| \| \| * \| \| \| \| \| \|	Fix the wrapper around ocamldebug.	Pierre-Marie Pédrot	2018-01-15
\| \|_\|_\|/ / / / / / / \|/\| \| \| \| \| \| \| \| \|
\| \| * \| \| \| \| \| \| \|	Avoid shell backticks and improve md5sum.ml error messages	Jacques-Pascal Deplaix	2018-01-15
\| * \| \| \| \| \| \| \| \|	More tests on brackets with goal selectors (including failures).	Théo Zimmermann	2018-01-15
\| * \| \| \| \| \| \| \| \|	Add test-suite file for bracket with goal selector.	Théo Zimmermann	2018-01-15
\| \| \| \| * \| \| \| \| \|	Actually use the strategy information in the checker.	Pierre-Marie Pédrot	2018-01-14
\| \| \| \| * \| \| \| \| \|	Store the conversion oracle in constant and inductive definitions.	Pierre-Marie Pédrot	2018-01-14
\| \|_\|_\|/ / / / / / \|/\| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \|	Merge PR #6578: Remove references to deleted Unicode.Unsupported exception	Maxime Dénès	2018-01-13
\|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \	Merge PR #6581: Added newline at the end of usage of coqdep.	Maxime Dénès	2018-01-13
\|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \	Merge PR #6564: Fix undefined variables in test-suite/Makefile + add PRINT_LOGS	Maxime Dénès	2018-01-13
\|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \	Merge PR #6483: Strong invariants in polymorphic definitions	Maxime Dénès	2018-01-12
\|\ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6288: Interfaces for checker and IDE.	Maxime Dénès	2018-01-12
\|\ \ \ \ \ \ \ \ \ \ \ \ \
\| \| * \| \| \| \| \| \| \| \| \| \| \|	Adding a custom Travis overlay for HoTT.	Pierre-Marie Pédrot	2018-01-11
\| \| * \| \| \| \| \| \| \| \| \| \| \|	Enforce that polymorphic definitions do not generate internal constraints.	Pierre-Marie Pédrot	2018-01-11
\| \| \| * \| \| \| \| \| \| \| \| \| \|	Document test-suite PRINT_LOGS.	Gaëtan Gilbert	2018-01-11
\| \| \| * \| \| \| \| \| \| \| \| \| \|	Fix undefined variables in test-suite/Makefile + add PRINT_LOGS	Gaëtan Gilbert	2018-01-11
\| \|_\|/ / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #6557: First stab at documenting the test suite.	Maxime Dénès	2018-01-11
\|\ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6552: [PR template] Remove the relative link to CHANGES.	Maxime Dénès	2018-01-11
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ \|/\| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| * \| \| \| \| \| \| \| \|	Added newline at the end of usage of coqdep.	Bernhard Schommer	2018-01-11
\| \|_\|_\|_\|/ / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| * \| \| \| \| \| \| \| \|	Force polymorphic definitions to have no internal constraints.	Pierre-Marie Pédrot	2018-01-11
\| \| \| \| \| * \| \| \| \| \| \| \|	Remove references to removed Unicode.Unsupported	Jasper Hugunin	2018-01-11
\| \|_\|_\|_\|/ / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \|
\| \| * \| \| \| \| \| \| \| \| \|	Lint and remove redundant line	Jasper Hugunin	2018-01-11
\| \| \| * \| \| \| \| \| \| \| \|	Add interfaces for IDE and remove dead code.	Maxime Dénès	2018-01-10
\| \| \| * \| \| \| \| \| \| \| \|	Add interfaces for checker and remove dead code.	Maxime Dénès	2018-01-10
\| \|_\|/ / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \|