coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
...
* \| \| \| \| \| \| \| \| \| \| \|	Merge PR #6827: [VM] Remove projection names from structured constants.	Pierre-Marie Pédrot	2018-06-11
\|\ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #7761: Fixing #7700: section variables bound to abbreviations were ↵	Emilio Jesus Gallego Arias	2018-06-11
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	not found
* \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #7406: Fix #7214: install knows which ml files do not get compiled ↵	Pierre-Marie Pédrot	2018-06-11
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	to cmx.
* \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #7748: Add a bit of doc to EConstr.decompose_lam*	Pierre-Marie Pédrot	2018-06-11
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #7757: [lib] Fix wrong deprecation comment.	Pierre-Marie Pédrot	2018-06-11
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| *	[build] Fix checks and notes noting 4.02.1 instead of 4.02.3	Emilio Jesus Gallego Arias	2018-06-11
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Bumping to 4.02.3 was decided some time ago in the WG, however a couple of places escaped updating.
\| \| \| \| \| \| * \| \| \| \| \| \| \| \| \|	Bump version number to 8.9+alpha1	Maxime Dénès	2018-06-11
\| \|_\|_\|_\|_\|/ / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #7736: [ci] Fix GeoCoq after https://github.com/GeoCoq/GeoCoq/issues/12	Gaëtan Gilbert	2018-06-11
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #7284: [sphinx] Start fixing SSR chapter.	Maxime Dénès	2018-06-11
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\| \| * \| \| \| \| \| \| \| \| \| \| \| \| \| \|	[ci] GeoCoq now depends on math-comp's ssralg.	Emilio Jesus Gallego Arias	2018-06-11
\| \|/ / / / / / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| * \| \| \| \| \| \| \|	Tweak printing boxes for unicode binders	Ralf Jung	2018-06-10
\| \|_\|_\|_\|_\|_\|_\|/ / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| * \| \| \| \| \| \| \| \|	[VM] Remove projection names from structured constants.	Maxime Dénès	2018-06-10
\| \|_\|_\|_\|_\|/ / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	It was actually a hack since those names are never used to represent values, only to be passed as arguments to bytecode instructions. So instead of reusing the structured_constant type, we follow the same pattern as switch annotations.
\| \| \| \| \| * \| \| \| \| \| \| \| \|	Fixing #7700 (section variables bound to abbreviations were not found).	Hugo Herbelin	2018-06-10
\| \|_\|_\|_\|/ / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Redundancy between finding section variables in both interp_var and interp_qualid could probably be cleaned.
\| \| * \| \| \| \| \| \| \| \| \| \|	[lib] Fix wrong deprecation comment.	Emilio Jesus Gallego Arias	2018-06-10
\| \|/ / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \| \|	Merge PR #7691: Fixing spelling of statment/statement in two API types	Pierre-Marie Pédrot	2018-06-09
\|\ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| \| \| \| \| * \|	[merge script] Check if the CI that was run is outdated.	Théo Zimmermann	2018-06-09
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	[ci skip]
* \| \| \| \| \| \| \| \| \| \| \|	Merge PR #7515: gitlab: build sphinx doc in separate job	Emilio Jesus Gallego Arias	2018-06-09
\|\ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #7642: Gitlab: retry failed jobs once	Emilio Jesus Gallego Arias	2018-06-09
\|\ \ \ \ \ \ \ \ \ \ \ \ \
\| \| * \| \| \| \| \| \| \| \| \| \| \|	gitlab: build sphinx doc in separate job	Gaëtan Gilbert	2018-06-08
\| \| \| \| \| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #7739: add test for #7595	Gaëtan Gilbert	2018-06-08
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #7747: dev/doc/univpoly.{txt => md}, split off primitive projection ↵	Théo Zimmermann	2018-06-08
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	info
\| \| \| \| \| \| \| * \| \| \| \| \| \| \| \|	Add a bit of doc to EConstr.decompose_lam*	Gaëtan Gilbert	2018-06-08
\| \|_\|_\|_\|_\|_\|/ / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| \| \| \| *	[doc] Disable smartquotes conversion	Clément Pit-Claudel	2018-06-08
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Closes GH-7742.
\| * \| \| \| \| \| \| \| \| \| \| \| \|	dev/doc/univpoly.{txt => md}, split off primitive projection info	Gaëtan Gilbert	2018-06-08
\| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| * \| \| \| \| \| \| \| \| \| \|	Gitlab: retry failed "build" jobs once	Gaëtan Gilbert	2018-06-08
\| \| \| \| \| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #7417: Micromega clean-up	Théo Zimmermann	2018-06-08
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \| \|/ / / / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #7687: [ci] [docker] Pin specific versions of OPAM CI dependencies.	Gaëtan Gilbert	2018-06-08
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \
\| \| * \| \| \| \| \| \| \| \| \| \| \| \|	Micromega clean-up	Maxime Dénès	2018-06-07
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	We add .mli files, removed dead code and use standard combinators instead of redefined ad-hoc ones in a few places. A lot of cleaning still has to be done on this code: documenting the interfaces, resolving the many abstraction leaks. I suspect there is still a lot of code duplication.
\| \| \| * \| \| \| \| \| \| \| \| \| \| \|	add test for #7595	Ralf Jung	2018-06-07
\| \|_\|/ / / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #7735: Remove cross-crypto from Travis. It is still tested in ↵	Emilio Jesus Gallego Arias	2018-06-07
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	GitLab CI.
\| * \| \| \| \| \| \| \| \| \| \| \| \| \|	Remove cross-crypto from Travis. It is still tested in GitLab CI.	Théo Zimmermann	2018-06-07
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This fixes #7734.
\| \| \| \| \| \| \| \| \| \| \| \| \| * \|	Fix the checker by merely adapting the data structure.	Pierre-Marie Pédrot	2018-06-07
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Unluckily, this is completely wrong as we trust the inlined term to be well-typed in some unavailable environment. To start with, the checker should not even rely on substitutions as it does not trust functors, but it does anyways. I have thus commented this code as a useful backdoor for when Coq is used to implement the next blockchain Ponzi scheme. We really need to sort this out though.
\| \| \| \| \| \| \| \| \| \| \| \| \| * \|	Fix #7615: Functor inlining drops universe substitution.	Pierre-Marie Pédrot	2018-06-07
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	We store the universe context in the inlined terms and apply it to the instance provided to the substitution function. Technically the context is not needed, but we use it to assert that the length of the instance corresponds, just in case.
* \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #7629: Fix anomaly in autoapply when an unbound hint name is provided	Matthieu Sozeau	2018-06-07
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \| \|/ / / / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #7706: Fix wrong deprecation msg	Pierre-Marie Pédrot	2018-06-07
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6874: [econstr] Some minor tweaks	Pierre-Marie Pédrot	2018-06-07
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #7721: Add a note about [ci skip] in CI README.	Emilio Jesus Gallego Arias	2018-06-06
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| * \| \| \| \| \| \| \| \| \| \| \|	[ci] [docker] Pin specific versions of OPAM CI dependencies.	Emilio Jesus Gallego Arias	2018-06-06
\| \|_\|_\|_\|/ / / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Packages such as `menhir` or `elpi` are fragile w.r.t. updates, so allowing a non-deterministic install in the Dockefile seems risky. We have found trouble with Menhir in the past. We thus specify a concrete version for all `CI_OPAM` packages. cc: https://github.com/AbsInt/CompCert/issues/234 We also add remove `hevea` from `apt` dependencies as it hasn't been needed since #7466 and add `texlive-science` which is needed to build the `source-doc` target due to the `textgreek` package being used.
\| * \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Add a note about [ci skip] in CI README.	Théo Zimmermann	2018-06-06
\|/ / / / / / / / / / / / / / /
* \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #7717: [ci] Temporal fix for CompCert	Gaëtan Gilbert	2018-06-06
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \| \|_\|_\|_\|/ / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| * \| \| \| \| \| \| \| \| \| \| \| \| \|	[ci] Temporal fix for CompCert	Emilio Jesus Gallego Arias	2018-06-06
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	https://github.com/AbsInt/CompCert/issues/234
* \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #7679: Clean native compilation of primitive projections	Maxime Dénès	2018-06-05
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #7004: Make `simple apply` obey `Opaque` directive.	Pierre-Marie Pédrot	2018-06-05
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #7077: Preserving canonical structure of return predicate in ↵	Maxime Dénès	2018-06-05
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	vm_compute and native_compute (partial fix to #7068; also fixes #7076))
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #7663: test suite: make target to regenerate failing output tests	Enrico Tassi	2018-06-05
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| \| \| \| \| \| * \| \| \| \| \| \|	Improve links to SSR tactics, and some other improvements.	Théo Zimmermann	2018-06-05
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #7464: Make whitespace linter not check for trailing space.	Maxime Dénès	2018-06-05
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| *	Define rec_declaration in terms of prec_declaration.	SimonBoulier	2018-06-05
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	And similarly for fixpoint and cofixpoint.
\| \| \| \| \| \| \| \| * \| \| \| \| \| \| \| \| \| \|	Update evarutil.mli	Matthieu Sozeau	2018-06-05
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Actually all the new_ functions are in evarutil still
\| \| \| \| \| \| \| \| * \| \| \| \| \| \| \| \| \| \|	Fix wrong deprecation msg	Matthieu Sozeau	2018-06-05
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|