coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
...
\| \| \| \| * \|	Take Suggest Proof Using outside the kernel.	Gaëtan Gilbert	2017-10-10
\| \| \| \|/ / \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Also add an output test for Suggest Proof Using. This changes the .aux output: instead of getting a key >context_used "$hyps;$suggest" where $hyps is a list of the used hypotheses and $suggest is the ;-separated suggestions (or the empty string if Suggest Proof Using is unset), there is a key >context_used "$hyps" and if Suggest Proof Using is set also a key >suggest_proof_using "$suggest" For instance instead of 112 116 context_used "B A;A B;All" we get 112 116 context_used "B A" 112 116 suggest_proof_using "A B;All"
* \| \| \| \|	Merge PR #1140: Fix Travis OSX deploy conditional.	Maxime Dénès	2017-10-10
\|\ \ \ \ \
\| \| * \| \| \|	Fix BZ#5780: coq_makefile broken under Cygwin	Ralf Jung	2017-10-10
\| \| \| \|/ / \| \| \|/\| \|
* \| \| \| \|	Merge PR #540: [configure] Support for flambda flags.	Maxime Dénès	2017-10-10
\|\ \ \ \ \
* \ \ \ \ \	Merge PR #1116: Updating citing Coq in FAQ.	Maxime Dénès	2017-10-10
\|\ \ \ \ \ \ \| \|_\|_\|/ / / \|/\| \| \| \| \|
\| * \| \| \| \|	Updating citing Coq in FAQ.	Hugo Herbelin	2017-10-10
\| \| \| \| \| \|
\| \| \| \| * \|	Restoring test on ident validity while browsing directory structure.	Hugo Herbelin	2017-10-10
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	The test was abandoned at the time of merging subdirectory browsing between coqdep and coqtop, and to limit at the same time the dependency of coqdep in files such as unicode.cmo. But checking ident validity speeds up browsing in arbitrary directory structure and we restore it for this reason. (One could also say that browsing arbitrary directory structures is not intended, but in practice this may happen, as e.g. reported in BZ#5734.)
\| \| \| \| * \|	Adding headers to segmenttree.{ml,mli}.	Hugo Herbelin	2017-10-10
\| \|_\|_\|/ / \|/\| \| \| \|
* \| \| \| \|	Merge PR #1137: Include leading zeros in version info	Maxime Dénès	2017-10-10
\|\ \ \ \ \
* \ \ \ \ \	Merge PR #768: Omega and romega know about context definitions (fix old bug 148)	Maxime Dénès	2017-10-10
\|\ \ \ \ \ \
* \ \ \ \ \ \	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
\|\ \ \ \ \ \ \ \
\| \| \| \| \| \| * \| \|	[flambda] [native] Pass `-Oclassic` to the native compiler.	Emilio Jesus Gallego Arias	2017-10-10
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This seems a safe choice as of today, but more advanced users would like to tweak it, or we could even refine it by a configure option if desired.
\| \| \| \| \| \| * \| \|	[configure] Support for flambda flags.	Emilio Jesus Gallego Arias	2017-10-10
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	We add a new option to configure `-flambda-opts` to allow passing custom flags to flambda. Example: ``` ./configure -flambda-opts "-O3 -unbox-closures" ```
* \| \| \| \| \| \| \| \|	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
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| * \|	Fix Travis OSX deploy conditional.	Gaëtan Gilbert	2017-10-09
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	IS is intended for testing nullity.
\| \| \| \| \| \| \| \| \| \| \| \| \| \| * \| \|	Include leading zeros in version info	Tej Chajed	2017-10-09
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Fixes BZ#5779
\| \| \| \| \| \| \| \| \| * \| \| \| \| \| \|	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.
\| \| \| \| \| \| \| \| \| \| \| \| * \| \|	travis: remove the overlay on bignums	Pierre Letouzey	2017-10-07
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This overlay is now useless (change pushed upstream in bignums) and moreover does not contain my commit making bignums resilient to PR#768.
\| \| \| \| \| \| \| \| \| \| \| \| * \| \|	Compat/Coq87.v : Unset Omega UseLocalDefs (see PR #768)	Pierre Letouzey	2017-10-07
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| * \| \| \| \|	[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).