coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Merge branch 'v8.6'	Pierre-Marie Pédrot	2017-05-17
\|\
* \	Merge PR#620: Reorganization of the layout for miscellaneous tests	Maxime Dénès	2017-05-17
\|\ \
* \ \	Merge PR#614: Improve Travis	Maxime Dénès	2017-05-17
\|\ \ \
\| * \| \|	Travis: add -warn-error targets (standard and 4.04.1 ocaml)	Gaetan Gilbert	2017-05-17
\| \| \| \|
* \| \| \|	Merge PR#630: [interp] [ast] Make raw_cases_pattern_expr private + small cleanup	Maxime Dénès	2017-05-17
\|\ \ \ \
\| \| * \| \|	Travis: deduplicate package list for coqide+documentation targets	Gaetan Gilbert	2017-05-17
\| \| \| \| \|
\| \| * \| \|	Travis: do not run the tests if building Coq fails	Gaetan Gilbert	2017-05-17
\| \|/ / / \|/\| \| \|
\| \| \| *	Merge PR#635: Fixing #5522 (anomaly with free vars of pat)	Maxime Dénès	2017-05-17
\| \| \| \|\
* \| \| \| \	Merge PR#636: Miscellaneous typos, dead code, etc.	Maxime Dénès	2017-05-17
\|\ \ \ \ \
* \ \ \ \ \	Merge PR#639: Stop using auto with * in two proofs.	Maxime Dénès	2017-05-17
\|\ \ \ \ \ \
\| * \| \| \| \| \|	Stop using auto with * in two proofs.	Théo Zimmermann	2017-05-16
\|/ / / / / / \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	auto with * is an overkill for people who do not care to understand what they really need. In these two cases, one lemma which was available in the typeclass_instances hint db.
\| \| \| \| \| *	Fixing bug #5222 (anomaly with "`pat" in the presence of scope delimiters).	Hugo Herbelin	2017-05-16
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	We seized this opportunity to factorize the code for interning `pat with more general pre-existing code. More precisely: There was already a function to compute the free variables of a pattern. Commit c6d9d4fb rewrote an approximation of it and #5222 hits cases non-treated by this function. We remove the partially-defined redundant code and use instead the existing code since intern_cases_pattern, already called, was already doing this computation. (In doing so, we discover a bug in merging names in the presence of nested "as" clauses, which we fix in previous commit. Additionally, intern_local_pattern was misleadingly overkill to simply mean a folding on Id.Set.add and we avoid the detour.
\| \| \| \| \| *	Fixing a bug with nested "as" clauses in "match".	Hugo Herbelin	2017-05-16
\| \| \| \| \| \|
\| \| \| \| * \|	Merge PR#624: Switch bedrock to mit-plv base	Maxime Dénès	2017-05-16
\| \| \| \| \|\ \ \| \| \| \| \| \|/ \| \| \| \| \|/\|
* \| \| \| \| \|	Merge PR#626: Add documentation for Set Ltac Batch Debug	Maxime Dénès	2017-05-16
\|\ \ \ \ \ \
* \ \ \ \ \ \	Merge PR#629: A couple of simple updates for Travis	Maxime Dénès	2017-05-16
\|\ \ \ \ \ \ \
\| \| \| * \| \| \| \|	Dead code in coqdep.	Hugo Herbelin	2017-05-15
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Was introduced in 5268efdef, reverted then readded in 1be9c4d.
\| \| \| \| * \| \| \|	[interp] Rework check for casts inside patterns.	Emilio Jesus Gallego Arias	2017-05-15
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	1969e10f25df0c913600099b7b98ea273a064017 introduced a check so a cast in a pattern is not a fatal error. We move this check to the internalization function, which is the logical place to raise it, removing a bit boilerplate code.
\| \| \| \| * \| \| \|	[interp] [ast] Make raw_cases_pattern_expr private.	Emilio Jesus Gallego Arias	2017-05-15
\| \|_\|_\|/ / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	The type `raw_cases_pattern_expr` is used only in the interpretation of notation patterns. Indeed, this should be a private type thus we make it local to `Constrintern`; it makes no sense to expose it in the public AST. The patch is routine, except for the case used to interpret primitives in patterns. We now return a `glob_constr` representing the raw pattern, instead of the private raw pattern type. This could be further refactored but have opted to be conservative here. This patch is a refinement of b2953849b999d1c3b42c0f494b234f2a93ac7754 , see the commentaries there for more information about `raw_cases_pattern_expr`.
\| \| \| * \| \| \|	Typo in comments of constrintern.	Hugo Herbelin	2017-05-15
\| \| \| \| \| \| \|
\| \| \| \| \| * \|	Removing a line warned unused.	Hugo Herbelin	2017-05-14
\| \| \| \| \| \| \|
\| \| \| \| \| * \|	Removing a variable warned unused.	Hugo Herbelin	2017-05-14
\| \| \| \| \| \| \|
\| * \| \| \| \| \|	[travis] Update OCaml to 4.04.1	Emilio Jesus Gallego Arias	2017-05-13
\| \| \| \| \| \| \|
\| * \| \| \| \| \|	[travis] Move VST to required suite.	Emilio Jesus Gallego Arias	2017-05-13
\|/ / / / / /
\| \| * \| \| \|	Uniformity of style for selecting plural or not; spacing for comma.	Hugo Herbelin	2017-05-13
\| \| \| \| \| \|
\| \| * \| \| \|	Typo in a comment of plugin Quote.	Hugo Herbelin	2017-05-13
\| \| \| \| \| \|
\| \| * \| \| \|	Aligning on standard layout of CHANGES.	Hugo Herbelin	2017-05-13
\| \|/ / / / \|/\| \| \| \|
\| * \| \| \|	Add documentation for Set Ltac Batch Debug	Jason Gross	2017-05-11
\|/ / / /
* \| \| \|	Merge PR#594: An example showing the benefit of Econstr	Maxime Dénès	2017-05-11
\|\ \ \ \
* \ \ \ \	Merge PR#373: A refined solution to the beta-iota discrepancies between 8.4 ↵	Maxime Dénès	2017-05-11
\|\ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	and 8.5/8.6 "refine"
* \ \ \ \ \	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
\|\ \ \ \ \ \ \
\| \| \| \| \| \| \| *	Switch bedrock to mit-plv base	Jason Gross	2017-05-10
\| \| \| \| \| \| \|/
\| \| \| \| \| \| *	Merge PR#604: FIx bug #5300: Anomaly: Uncaught exception Not_found" in ↵	Maxime Dénès	2017-05-10
\| \| \| \| \| \| \|\ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	"Print Assumptions".
\| \| \| \| \| * \| \|	Moving code for miscellaneous tests to specific files.	Hugo Herbelin	2017-05-10
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	The rule is that any file misc/*.sh will now be automatically executed from the test-file directory with appropriate environment variables set. The test can use any auxiliary material which is put in a directory of the same name as the test. This avoids making the main Makefile more or more complex. We loose some customization though (no more custom messages such as printing of the number of universes in the test about the number of necessary universes). We could preserve such customization if needed but I did not consider it was worth the effort. Warning: specific targets universes, deps-order, deps-checksum are removed by consistency. Do instead "make misc/universes.log", etc., or even "make misc" for all.
\| \| \| \| \| * \| \|	A more regular naming of variables in test-suite Makefile.	Hugo Herbelin	2017-05-10
\| \| \| \| \| \| \| \|
\| \| \| \| \| * \| \|	Adding tests for testing exit status and #use"include".	Hugo Herbelin	2017-05-10
\| \| \| \| \| \| \| \|
\| \| \| \| \| * \| \|	Cleaning old untested not any more interesting testing files.	Hugo Herbelin	2017-05-10
\| \|_\|_\|_\|/ / / \|/\| \| \| \| \| \|
\| \| \| \| \| * \|	Merge PR#591: Add bmsherman/topology to the ci	Maxime Dénès	2017-05-09
\| \| \| \| \| \|\ \
\| \| \| \| \| \| * \|	Put .travis.yml in alphabetical order	Jason Gross	2017-05-09
\| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \|	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#609: Fix bug #3659: -time should understand multibyte encodings.	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
\| \|_\|_\|_\|/ / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Note that [@@@ocaml.warning "-32"] caused an error with Drop. It was put there because I didn't realise the warning was about a real issue.