coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Include leading zeros in version info	Tej Chajed	2017-10-09
\| \| \| \|	Fixes BZ#5779
*	Merge PR #1127: Shorten the .gitattributes file.	Maxime Dénès	2017-10-06
\|\
* \	Merge PR #1118: Extraction : minor support stuff for the new Extraction ↵	Maxime Dénès	2017-10-06
\|\ \ \| \| \| \| \| \| \| \| \|	Compute plugin
* \ \	Merge PR #1119: Fixing bug BZ#5769 (generating a name "_" out of a type ↵	Maxime Dénès	2017-10-06
\|\ \ \ \| \| \| \| \| \| \| \| \| \| \| \|	"_something")
* \ \ \	Merge PR #1121: Fixing BZ#5765 (an anomaly with 'pat in the parameters of an ↵	Maxime Dénès	2017-10-06
\|\ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	inductive definition)
* \ \ \ \	Merge PR #1125: [pp] Minor optimization in `Pp.t` construction and gluing.	Maxime Dénès	2017-10-06
\|\ \ \ \ \
* \ \ \ \ \	Merge PR #1124: Extraction: reduce atomic eta-redexes (solves indirectly ↵	Maxime Dénès	2017-10-06
\|\ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	BZ#4852)
* \ \ \ \ \ \	Merge PR #1128: GitLab CI: make all_stdlib.v in build job	Maxime Dénès	2017-10-06
\|\ \ \ \ \ \ \
* \ \ \ \ \ \ \	Merge PR #1130: Fix copyright info in reference manual.	Maxime Dénès	2017-10-06
\|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \	Merge PR #1131: Clean-up xml protocol doc	Maxime Dénès	2017-10-06
\|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \	Merge PR #1129: 8.7+beta2 CHANGES	Maxime Dénès	2017-10-06
\|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \	Merge PR #1123: [ci] Remove deploy to GitHub of OS X package.	Maxime Dénès	2017-10-06
\|\ \ \ \ \ \ \ \ \ \ \
\| \| \| * \| \| \| \| \| \| \| \|	Extract changes to the XML protocol from its doc	Théo Zimmermann	2017-10-06
\| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| * \| \| \| \| \| \| \| \|	Make the XML protocol doc more version-independent	Théo Zimmermann	2017-10-06
\| \|_\|/ / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \|
\| \| \| * \| \| \| \| \| \| \|	Fix copyright info in reference manual.	Théo Zimmermann	2017-10-06
\| \|_\|/ / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Also simplifies the way it is presented (no need to be overly precise).
\| \| * \| \| \| \| \| \| \|	8.7+beta2 CHANGES	Théo Zimmermann	2017-10-06
\| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \|	Merge PR #1069: Improve support for -w options	Maxime Dénès	2017-10-05
\|\ \ \ \ \ \ \ \ \ \ \| \|_\|/ / / / / / / / \|/\| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \|	Merge PR #1081: Mini fix at improving the cannot unify error message	Maxime Dénès	2017-10-05
\|\ \ \ \ \ \ \ \ \ \
* \| \| \| \| \| \| \| \| \| \|	Fix typo in INSTALL	Maxime Dénès	2017-10-05
\| \| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \|	Merge PR #1041: Miscellaneous fixes about UTF-8 (including a fix to BZ#5715 ↵	Maxime Dénès	2017-10-05
\|\ \ \ \ \ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	to escape non-UTF-8 file names)
* \ \ \ \ \ \ \ \ \ \ \	Merge PR #1093: [doc] Update INSTALL to match reality.	Maxime Dénès	2017-10-05
\|\ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #1107: Add coqwc tests to test suite	Maxime Dénès	2017-10-05
\|\ \ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| * \| \| \| \| \| \|	GitLab CI: make all_stdlib.v in build job	Gaëtan Gilbert	2017-10-05
\| \| \| \| \| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #1106: Fix beautifier	Maxime Dénès	2017-10-05
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #1102: On the detection of evars which "advanced" (and a fix to ↵	Maxime Dénès	2017-10-05
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	BZ#5757)
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #1101: Fixing an old proof engine bug in collecting evars with ↵	Maxime Dénès	2017-10-05
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	cleared context.
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #1059: coq_makefile: make sure compile flags for Coq and ↵	Maxime Dénès	2017-10-05
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	coq_makefile are in sync (supersed #1039)…
* \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #1112: Fix GeoCoq CI and remove it from allowed failures	Maxime Dénès	2017-10-05
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| \| \| \| \| \| * \| \| \| \| \|	Extraction: reduce eta-redexes whose cores are atomic (solves indirectly ↵	Pierre Letouzey	2017-10-05
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	BZ#4852) This code simplification isn't that important, but it can trigger further simplifications elsewhere, see for instance BZ#4852. NB: normally, the extraction favors eta-expanded forms, since that's the usual way to avoid issues about '_a type variables that cannot be generalized. But the atomic eta-reductions done here shouldn't be problematic (no applications put outside of functions).
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| *	Shorten the .gitattributes file.	Théo Zimmermann	2017-10-05
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	.dir-locals.el can be useful for users of the tarballs as well, and TODO doesn't exist anymore.
\| \| \| \| \| \| \| \| \| \| \| \| * \| \| \|	[pp] Minor optimization in `Pp.t` construction and gluing.	Emilio Jesus Gallego Arias	2017-10-05
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	The typical Coq `Pp.t` document contains a lot of "gluing" which produces efficient structures but it is quite painful in serialization. We optimize a common document building case so we don't create as much glue nodes as with the "naive" strategy, and without incurring in the large performance cost full flattening would produce. This is a temporal fixup, see #505 for more context on the discussion and medium-term plans.
\| \| \| \| \| \| \| \| \| \| \| * \| \| \|	[ci] Remove deploy to GitHub of OS X package.	Théo Zimmermann	2017-10-05
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This is inconvenient because it can only be tested on tags and it didn't work for V8.7+beta1.
\| \| \| \| \| \| \| \| \| \| \| \| \| * \|	Fixing BZ#5769 (variable of type "_something" was named after invalid "_").	Hugo Herbelin	2017-10-05
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| \| \| * \|	Distinguishing pseudo-letters out of the set of unicode letters.	Hugo Herbelin	2017-10-05
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This includes _ and insecable space which can be used in idents and this allows more precise heuristics.
\| \| \| \| \| \| \| \| \| \| \| \| \| * \|	Fixing typos in comments of unicode.ml.	Hugo Herbelin	2017-10-05
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| \| * \| \|	Fixing #5765 (an anomaly with 'pat in parameters of inductive definition).	Hugo Herbelin	2017-10-05
\| \| \| \| \| \| \| \| \| \| \| \| \|/ /
* \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #1006: fix: ssrmatching and primitive projections	Maxime Dénès	2017-10-04
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #1078: Report missing arguments in error message	Maxime Dénès	2017-10-04
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| *	Extraction : minor support stuff for the new Extraction Compute plugin	Pierre Letouzey	2017-10-04
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|/ \| \| \| \| \| \| \| \| \| \| \| \| \| \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	See https://github.com/letouzey/extraction-compute for more details
* \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #1096: [stm] Warn about costly Undo operations in batch mode [BZ#5677]	Maxime Dénès	2017-10-04
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #1058: Fixing BZ#5741 (anomaly in info_trivial).	Maxime Dénès	2017-10-04
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| * \| \| \| \| \|	add coqwc tests	Paul Steckler	2017-10-03
\| \| \| \| \| \| \| \| \| \| \| \|_\|_\|_\|/ \| \| \| \| \| \| \| \| \| \| \|/\| \| \| \|
\| \| \| \| \| \| * \| \| \| \| \| \| \| \|	fix compilation on OCaml < 4.04	Enrico Tassi	2017-10-03
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #1110: Mention requiring extraction/funind in CHANGES	Maxime Dénès	2017-10-03
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #1105: [stm] Remove unused "Proof using" data in `Sync` tags.	Maxime Dénès	2017-10-03
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #1104: Browser userscript to turn BZ#XXXX occurences into links.	Maxime Dénès	2017-10-03
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #1100: Avoid looping when searching for CoqProject.	Maxime Dénès	2017-10-03
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #1099: BZ#5637, look for Obligation num or Next Obligation to start ↵	Maxime Dénès	2017-10-03
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	proof for coqwc
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #1097: Properly display the "only" prefix for selectors (bug #5760).	Maxime Dénès	2017-10-03
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #1094: Fixing a little parsing bug with level 90 introduced in ↵	Maxime Dénès	2017-10-03
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	3e70ea9c.