coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Post-merge API fix.	Maxime Dénès	2017-08-29
\|
*	Merge PR #946: Functional pretyping interface	Maxime Dénès	2017-08-29
\|\
* \	Merge PR #937: [general] Remove spurious dependency of highparsing on toplevel.	Maxime Dénès	2017-08-29
\|\ \
* \ \	Merge PR #916: Fixing notation bug 5608 involving { } and a slight ↵	Maxime Dénès	2017-08-29
\|\ \ \ \| \| \| \| \| \| \| \| \| \| \| \|	restructuration
* \ \ \	Merge PR #838: Have coq-dpdgraph ci test print the differences	Maxime Dénès	2017-08-29
\|\ \ \ \
* \ \ \ \	Merge PR #830: Moving assert (the "Cut" rule) to new proof engine	Maxime Dénès	2017-08-29
\|\ \ \ \ \
* \ \ \ \ \	Merge PR #819: Cleanup old things	Maxime Dénès	2017-08-29
\|\ \ \ \ \ \
* \ \ \ \ \ \	Merge PR #805: Functional tactics	Maxime Dénès	2017-08-29
\|\ \ \ \ \ \ \
* \ \ \ \ \ \ \	Merge PR #773: [flags] Remove XML output flag.	Maxime Dénès	2017-08-29
\|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \	Merge PR #966: Makefile : ignore user-contrib in various file searches	Maxime Dénès	2017-08-29
\|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \	Merge PR #985: Fix coqdoc test-suite target on Windows.	Maxime Dénès	2017-08-29
\|\ \ \ \ \ \ \ \ \ \
* \| \| \| \| \| \| \| \| \| \|	Trying to fix deployment of master on bintray, and deploy tags to github.	Maxime Dénès	2017-08-29
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Deployment doesn't work on PRs, so I have to push it directly, sorry for the noise.
* \| \| \| \| \| \| \| \| \| \|	Master now deploys 8.8+alpha.	Maxime Dénès	2017-08-29
\| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| * \| \|	Quoting notations in incompatible-level error message.	Hugo Herbelin	2017-08-29
\| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| * \| \|	A new step of restructuration of notations.	Hugo Herbelin	2017-08-29
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This allows to issue a more appropriate message when a notation with a { } cannot be defined because of an incompatible level. E.g.: Notation "{ A } + B" := (sumbool A B) (at level 20).
\| \| \| \| \| \| \| \| * \| \|	Adding a test for #5569 (warning about skipping spaces).	Hugo Herbelin	2017-08-29
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	The two previous commits make the warning irrelevant and useless.
\| \| \| \| \| \| \| \| * \| \|	Dropping former fix to bug #5469 (notation format not recognizing curly braces).	Hugo Herbelin	2017-08-29
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This reverts commit 53a50875 and a bit more: it also makes the check for possibly ignoring formatting spaces irrelevant, since the previous commit makes that curly brackets are not any more dropped for printing.
\| \| \| \| \| \| \| \| * \| \|	A little reorganization of notations + a fix to #5608.	Hugo Herbelin	2017-08-29
\| \|_\|_\|_\|_\|_\|_\|/ / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	- Formerly, notations such as "{ A } + { B }" were typically split into "{ _ }" and "_ + _". We keep the split only for parsing, which is where it is really needed, but not anymore for interpretation, nor printing. - As a consequence, one notation string can give rise to several grammar entries, but still only one printing entry. - As another consequence, "{ A } + { B }" and "A + { B }" must be reserved to be used, which is after all the natural expectation, even if the sublevels are constrained. - We also now keep the information "is ident", "is binder" in the "key" characterizing the level of a notation.
* \| \| \| \| \| \| \| \| \|	Update .mailmap file.	Guillaume Melquiond	2017-08-24
\| \| \| \| \| \| \| \| \| \|
\| * \| \| \| \| \| \| \| \|	Fix coqdoc URLs under Windows.	Théo Zimmermann	2017-08-21
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	URLs on Windows are the same as on Unix, they use / not \.
\| * \| \| \| \| \| \| \| \|	Extend .gitignore for coqdoc test-suite.	Théo Zimmermann	2017-08-21
\| \| \| \| \| \| \| \| \| \|
\| * \| \| \| \| \| \| \| \|	Fix coqdoc test-suite target on Windows.	Théo Zimmermann	2017-08-21
\|/ / / / / / / / / \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Commit 8f12597 introduced new output tests but these were broken on Windows. We fix them by using --strip-trailing-cr option of diff, like in other output tests in the test-suite.
* \| \| \| \| \| \| \| \|	Merge PR #965: Moving file primitive.ml to cPrimitive.ml to avoid conflict ↵	Maxime Dénès	2017-08-18
\|\ \ \ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	with OCaml.
* \ \ \ \ \ \ \ \ \	Merge PR #983: Correct the option for cumulativity in CHANGES	Maxime Dénès	2017-08-18
\|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \	Merge PR #973: Adding documentation for Printing Focused option.	Maxime Dénès	2017-08-18
\|\ \ \ \ \ \ \ \ \ \ \
\| \| * \| \| \| \| \| \| \| \| \|	Correct the option for cumulativity in CHANGES	Amin Timany	2017-08-18
\| \| \| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \| \|	Merge PR #801: Make Travis generate OSX packages.	Maxime Dénès	2017-08-18
\|\ \ \ \ \ \ \ \ \ \ \ \ \| \|_\|/ / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \|
\| * \| \| \| \| \| \| \| \| \| \|	Separate jobs for test-suite and package building under OSX.	Maxime Dénès	2017-08-18
\| \| \| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \| \|	Merge PR #972: 8.7 change entries	Maxime Dénès	2017-08-17
\|\ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #490: A possible fix for #5391 (command line tools do not accept ↵	Maxime Dénès	2017-08-17
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	trailing / and \ on windows)
* \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #974: Change section caption, improve some wording	Maxime Dénès	2017-08-17
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #976: Document anonymous universes (PR #544).	Maxime Dénès	2017-08-17
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| * \| \| \| \| \| \| \| \| \| \| \|	Use the wording suggested by Gaetan.	Théo Zimmermann	2017-08-17
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| * \| \| \| \| \| \| \| \| \| \| \|	Addition suggested by Pierre-Marie.	Théo Zimmermann	2017-08-17
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| * \| \| \| \| \| \| \| \| \| \|	Change 8.7~alpha to 8.7+alpha.	Maxime Dénès	2017-08-17
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Only the latter is a valid git tag, and we will soon be using those to generate our version numbers.
\| \| \| \| \| * \| \| \| \| \| \| \| \| \| \|	Make Travis generate OSX packages.	Maxime Dénès	2017-08-17
\| \|_\|_\|_\|/ / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	The packages will be built only for main branches (not pull requests), and are accessible via bintray: https://bintray.com/coq/coq
\| * \| \| \| \| \| \| \| \| \| \| \| \| \|	Document anonymous universes (PR #544).	Gaëtan Gilbert	2017-08-17
\|/ / / / / / / / / / / / / /
\| \| \| \| * / / / / / / / / /	Adding documentation for Printing Focused option.	Pierre Courtieu	2017-08-17
\| \|_\|_\|/ / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| * \| \| \| \| \| \| \| \| \|	Additions following Hugo's suggestions.	Théo Zimmermann	2017-08-16
\| \| \| \| \| \| \| \| \| \| \| \| \|
\| * \| \| \| \| \| \| \| \| \| \| \|	mention that tactic is the identity or gives error	Paul Steckler	2017-08-16
\| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| * \| \| \| \| \| \| \| \| \|	Improve wording.	Théo Zimmermann	2017-08-16
\| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| * \| \| \| \| \| \| \| \| \|	Mention tclINDEPENDENTL (#349) in dev/doc/changes.	Théo Zimmermann	2017-08-16
\| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| * \| \| \| \| \| \| \| \| \|	8.7 CHANGES	Théo Zimmermann	2017-08-16
\| \| \| \| \| \| \| \| \| \| \| \| \|
\| * \| \| \| \| \| \| \| \| \| \| \|	change section caption, improve some wording	Paul Steckler	2017-08-16
\|/ / / / / / / / / / / /
\| \| * / / / / / / / / /	Porting #856 (8.6.1 CHANGES entries) to master	Théo Zimmermann	2017-08-16
\| \|/ / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \|	Merge PR #957: Set detachable windows type hint to dialog.	Maxime Dénès	2017-08-16
\|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \	Merge PR #831: Port ssreflect user manual to Coq's latex/hevea style	Maxime Dénès	2017-08-16
\|\ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #912: Detyping functions are now operating on EConstr.t.	Maxime Dénès	2017-08-16
\|\ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #942: solving b1859	Maxime Dénès	2017-08-16
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #954: Print names of all open blocks	Maxime Dénès	2017-08-16
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \