coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	pre-commit hook: fix whitespace error detection	Gaëtan Gilbert	2018-02-08
\| \| \| \|	--quiet implies --exit-code
*	Mention linter and pre-commit hook in CONTRIBUTING.md.	Gaëtan Gilbert	2018-02-08
\|
*	A pre-commit hook to magically fix whitespace issues.	Gaëtan Gilbert	2018-02-08
\|
*	Merge PR #6627: Fix #6619: coqchk does not reduce compatibility constants ↵	Maxime Dénès	2018-01-23
\|\ \| \| \| \| \| \|	for primitive projections
* \	Merge PR #6628: [printing] Remove duplicate definitions of pr_lident and ↵	Maxime Dénès	2018-01-23
\|\ \ \| \| \| \| \| \| \| \| \|	pr_lname
* \ \	Merge PR #6629: Archive COMPATIBILITY	Maxime Dénès	2018-01-23
\|\ \ \
* \ \ \	Merge PR #6568: Cleanup scripts	Maxime Dénès	2018-01-23
\|\ \ \ \
\| \| * \| \|	Archive COMPATIBILITY.	Théo Zimmermann	2018-01-22
\| \| \| \| \|
\| \| * \| \|	Move the mention of the removal of Qed exporting at the right place.	Théo Zimmermann	2018-01-22
\| \| \| \| \|
* \| \| \| \|	Merge PR #6461: Let dtauto recognize '@sigT A (fun _ => B)' as a conjunction.	Maxime Dénès	2018-01-22
\|\ \ \ \ \
* \ \ \ \ \	Merge PR #6625: Update location on tab switch, issue 6624	Maxime Dénès	2018-01-22
\|\ \ \ \ \ \
* \ \ \ \ \ \	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
\|\ \ \ \ \ \ \ \ \ \ \ \| \|_\|_\|_\|_\|_\|_\|_\|/ / / \|/\| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| * \|	[printing] Remove duplicate definitions of pr_lident and pr_lname	Vincent Laporte	2018-01-22
\| \|_\|_\|_\|_\|_\|_\|_\|/ / \|/\| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| *	Adding a test for coqchk bug #6619.	Pierre-Marie Pédrot	2018-01-20
\| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| *	Fix #6618: coqchk fails with "ill-typed term".	Pierre-Marie Pédrot	2018-01-20
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Primitive projections were not correctly unfolded, leading to failure of conversion checks in some cases. The kernel was strangely not affected by this bug, and it was probably a remnant of some vestigial code.
\| \| \| \| \| \| \| \| \| *	Remove dead code in Environ.	Pierre-Marie Pédrot	2018-01-20
\| \|_\|_\|_\|_\|_\|_\|_\|/ \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	The constant_value function was actually not behaving the same as constant_value_in w.r.t. projections. The former was not used, and the only place that used the latter was in Tacred and was statically insensitive to the use of projections.
\| \| \| \| \| * \| \| \|	-annotate deprecated. New options: -annot, -bin-annot	Vadim Zaliva	2018-01-19
\| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| * \| \|	update location on tab switch, issue 6624	Paul Steckler	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, ↵	Paul Steckler	2018-01-18
\| \|/ / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	issue #6452
* \| \| \| \| \| \|	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 < ↵	Maxime Dénès	2018-01-17
\|\ \ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	2.18.3
* \ \ \ \ \ \ \ \	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
\| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| * \|	Let dtauto recognize '@sigT A (fun _ => B)' as a conjunction	Jasper Hugunin	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
\| \| \| \| \| \| \| \|_\|_\|/ / \| \| \| \| \| \| \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Fixes #6490. `prod_applist_assum` is copied from `kernel/term.ml` to `engine/termops.ml`, and adjusted to work with econstr. This change uncovered a bug in `Hipattern.match_with_nodep_ind`, where `has_nodep_prod_after` counts both products and let-ins, but was only being passed `mib.mind_nparams`, which does not count let-ins. Replaced with (Context.Rel.length mib.mind_params_ctxt).
\| \| \| \| * \| \| \| \| \| \|	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
\| \| \| \| \| \|/ / / / / \| \| \| \| \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	The Launchpad packages for lablgtk2 are misconfigured to report 2.16.0 even for much newer versions. This makes building Coq on Ubuntu impossible without modifying configure. This commit fixes that problem. See https://bugs.launchpad.net/ubuntu/+source/lablgtk2/+bug/1577236 for the upstream bug. This closes #6585
\| \| \| \| \| \| \| \| \| *	merge-pr.sh: use git diff --quiet	Gaëtan Gilbert	2018-01-16
\| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| *	Source basic overlay before user overlays.	Gaëtan Gilbert	2018-01-16
\| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| *	Cleanup shell expansions and quoting.	Gaëtan Gilbert	2018-01-16
\| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| *	Simplify logic and streamline lint-repository.sh	Gaëtan Gilbert	2018-01-16
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	We inline should-check-whitespace.sh in check-eof-newline.sh simplifying the find invocation.
* \| \| \| \| \| \| \| \| \|	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
\| \|_\|_\|/ / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Since 5ffa147, there is a new clib folder that needed to be added to the set of includes of ocamldebug