coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Merge PR #1053: [deps] Move `Discharge` to `interp`	Maxime Dénès	2017-10-10
\|\
* \	Merge PR #1067: Iris CI: use opam to install dependencies	Maxime Dénès	2017-10-10
\|\ \
* \ \	Merge PR #1087: [stm] Switch to a functional API	Maxime Dénès	2017-10-09
\|\ \ \
* \ \ \	Merge PR #1126: [ltac] Warning for deprecated `Add Setoid` and `Add ↵	Maxime Dénès	2017-10-09
\|\ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Morphism` forms.
* \ \ \ \	Merge PR #1134: Revert "Switch Travis to OSX 10.12 and Xcode 8.3.3."	Maxime Dénès	2017-10-09
\|\ \ \ \ \
* \ \ \ \ \	Merge PR #1133: Fix hardcoded boot dependencies after #1041.	Maxime Dénès	2017-10-09
\|\ \ \ \ \ \
* \ \ \ \ \ \	Merge PR #1132: TimeFileMaker.py: Allow trailing spaces	Maxime Dénès	2017-10-09
\|\ \ \ \ \ \ \
* \ \ \ \ \ \ \	Merge PR #1115: Autolink to Github PRs from Bugzilla	Maxime Dénès	2017-10-09
\|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \	Merge PR #1114: Generic handling of nameable objects for plugins	Maxime Dénès	2017-10-09
\|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \	Merge PR #1109: Handle some misc todos	Maxime Dénès	2017-10-09
\|\ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| \| \| \| *	[deps] Move `Discharge` to `interp`	Emilio Jesus Gallego Arias	2017-10-09
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	More dependencies / linking fixes.
* \| \| \| \| \| \| \| \| \| \|	Merge PR #1086: [stm] [flags] Move document mode flags to the STM.	Maxime Dénès	2017-10-09
\|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \	Merge PR #1062: BZ#5739, Allow level for leftmost nonterminal for ↵	Maxime Dénès	2017-10-09
\|\ \ \ \ \ \ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	printing-ony Notations
* \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #1117: [ci] Remove temporary bignums overlay.	Maxime Dénès	2017-10-09
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ \|/\| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| * \| \| \|	Revert "Switch Travis to OSX 10.12 and Xcode 8.3.3."	Théo Zimmermann	2017-10-07
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This reverts commit 587e556a909fcd2e1507a9230d9cdaffa3f9394e from PR #1024. This commit did not solve any issue at the time it was merged but made the macOS package we produce compatible only with macOS 10.12 and later.
\| \| \| \| \| \| \| \| * \| \| \| \|	Fix hardcoded boot dependencies after #1041.	Gaëtan Gilbert	2017-10-07
\| \|_\|_\|_\|_\|_\|_\|/ / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Specifically since e88dfedd99a84e9e375f3583be6fd1de3de36c72. There seem to have been no actual errors due to this, only ocaml complaining about missing .cmi files.
\| \| \| \| \| \| \| \| \| \| * \|	[stm] Switch to a functional API	Emilio Jesus Gallego Arias	2017-10-06
\| \| \| \| \|_\|_\|_\|_\|_\|/ / \| \| \| \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	We make the Stm API functional over an opaque `doc` type. This allows to have a much better picture of what the toplevel is doing; now almost all users of STM private data are marked by typing. For now only, the API is functional; a PR switching the internals should come soon thou; however we must first fix some initialization bugs. Due to some users, we modify `feedback` internally to include a "document id" field; we don't expose this change in the IDE protocol yet.
\| \| \| * \| \| \| \| \| \| \|	[stm] [flags] Move document mode flags to the STM.	Emilio Jesus Gallego Arias	2017-10-06
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	We move toplevel/STM flags from `Flags` to their proper components; this ensures that low-level code doesn't depend on them, which was incorrect and source of many problems wrt the interfaces. Lower-level components should not be aware whether they are running in batch or interactive mode, but instead provide a functional interface. In particular: == Added flags == - `Safe_typing.allow_delayed_constants` Allow delayed constants in the kernel. - `Flags.record_aux_file` Output `Proof using` information from the kernel. - `System.trust_file_cache` Assume that the file system won't change during our run. == Deleted flags == - `Flags.compilation_mode` - `Flags.batch_mode` Additionally, we modify the STM entry point and `coqtop` to account for the needed state. Note that testing may be necessary and the number of combinations possible exceeds what the test-suite / regular use does. The next step is to fix the initialization problems [c.f. Bugzilla], which will require a larger rework of the STM interface.
\| \| \| * \| \| \| \| \| \| \|	[coqtop] Don't reset coqinit internal variables after initialization.	Emilio Jesus Gallego Arias	2017-10-06
\| \|_\|/ / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	We remove `init_library_roots` as there is no point in resetting this internal variable. Its only user is `init_load_path` and this function is not meant (and is not) idempotent now.
* \| \| \| \| \| \| \| \| \|	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
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| * \| \|	TimeFileMaker.py: Allow trailing spaces	Jason Gross	2017-10-06
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This allows the timing aggregation scripts to handle logs from Travis, which, for some reason, seems to insert trailing spaces.
\| \| \| * \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	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
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| * \|	[ltac] Warning for deprecated `Add Setoid` and `Add Morphism` forms.	Emilio Jesus Gallego Arias	2017-10-05
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	The manual has long stated that these forms are deprecated. We add a warning for them, as indeed `Add Morphism` is an "proof evil" [] command, and we may want to remove it in the future. We've also fixed the stdlib not to emit the warning. [] https://ncatlab.org/nlab/show/principle+of+equivalence
* \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	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.