coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Merge branch 'v8.6'	Pierre-Marie Pédrot	2017-06-08
\|\
* \|	Remove overlay.	Maxime Dénès	2017-06-08
\| \|
* \|	add overlays	Matej Košík	2017-06-07
\| \|
* \|	Overlay.	Maxime Dénès	2017-06-06
\| \|
* \|	Remove some overlays.	Maxime Dénès	2017-06-06
\| \|
* \|	Overlays.	Maxime Dénès	2017-06-06
\| \|
* \|	Merge PR#723: [travis] [fiat] Test also fiat-core.	Maxime Dénès	2017-06-06
\|\ \
\| * \|	[travis] [fiat] Test also fiat-core.	Emilio Jesus Gallego Arias	2017-06-02
\| \| \| \| \| \| \| \| \| \| \| \|	I didn't rename the test file to `fiat` as IMHO it is not worth the noise.
* \| \|	Adding overlay for math-comp.	Hugo Herbelin	2017-05-31
\|/ /
* \|	Merge PR#687: Gitlab CI	Maxime Dénès	2017-05-29
\|\ \
\| * \|	Gitlab CI	Gaëtan Gilbert	2017-05-28
\| \| \|
* \| \|	[coqlib] Move `Coqlib` to `library/`.	Emilio Jesus Gallego Arias	2017-05-27
\|/ / \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	We move Coqlib to library in preparation for the late binding of Gallina-level references. Placing `Coqlib` in `library/` is convenient as some components such as pretyping need to depend on it. By moving we lose the ability to locate references by syntactic abbreviations, but IMHO it makes to require ML code to refer to a true constant instead of an abbreviation/notation. Unfortunately this change means that we break the `Coqlib` API (providing a compatibility function is not possible), however we do so for a good reason. The main changes are: - move `Coqlib` to `library/`. - remove reference -> term from `Coqlib`. In particular, clients will have different needs with regards to universes/evar_maps, so we force them to call the (not very safe) `Universes.constr_of_global` explicitly so the users are marked. - move late binding of impossible case from `Termops` to `pretying/Evarconv`. Remove hook. - `Coqlib.find_reference` doesn't support syntactic abbreviations anymore. - remove duplication of `Coqlib` code in `Program`. - remove duplication of `Coqlib` code in `Ltac.Rewrite`. - A special note about bug 5066 and commit 6e87877 . This case illustrates the danger of duplication in the code base; the solution chosen there was to transform the not-found anomaly into an error message, however the general policy was far from clear. The long term solution is indeed make `find_reference` emit `Not_found` and let the client handle the error maybe non-fatally. (so they can test for constants.
* \|	[travis] temporary UniMath overlay	Maxime Dénès	2017-05-27
\| \| \| \| \| \| \| \|	We are waiting for an upstream merge of a fix related to coq_makefile2.
* \|	Merge PR#481: [option] Remove support for non-synchronous options.	Maxime Dénès	2017-05-25
\|\ \
* \ \	Merge PR#406: coq makefile2	Maxime Dénès	2017-05-25
\|\ \ \
* \| \| \|	[location] [travis] Add overlays for located_switch	Emilio Jesus Gallego Arias	2017-05-25
\| \| \| \|
* \| \| \|	Merge branch 'trunk' into located_switch	Emilio Jesus Gallego Arias	2017-05-24
\|\ \ \ \
\| \| \| * \|	[option] Remove support for non-synchronous options.	Emilio Jesus Gallego Arias	2017-05-24
\| \| \|/ / \| \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Inspired by https://coq.inria.fr/bugs/show_bug.cgi?id=5229 , which this PR solves, I propose to remove support for non-synchronous options. It seems the few uses of `optsync = false` we legacy and shouldn't have any impact. Moreover, non synchronous options may create particularly tricky situations as for instance, they won't be propagated to workers.
\| \| \| *	Add parsers-examples target to fiat-parsers ci	Jason Gross	2017-05-23
\| \| \| \| \| \| \| \| \| \| \| \|	This tests a bit more of fiat-parsers, adding an extra ~3 minutes to the build.
\| \| * \|	overlay for UniMath	Enrico Tassi	2017-05-23
\| \|/ /
\| * \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2017-05-17
\| \|\\|
\| \| *	Switch bedrock to mit-plv base	Jason Gross	2017-05-10
\| \| \|
\| \| *	Add bmsherman/topology to the ci	Jason Gross	2017-05-01
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This development of @bmsherman tests universe polymorphism and setoid rewriting in type, and should build with v8.6 and trunk.
\| * \|	Merge PR#568: Remove tactic compatibility layer	Maxime Dénès	2017-04-27
\| \|\ \
\| * \ \	Merge branch 'v8.6'	Pierre-Marie Pédrot	2017-04-27
\| \|\ \ \ \| \| \| \|/ \| \| \|/\|
* \| / \|	[travis] mathcomp and fiat overlay for #402	Emilio Jesus Gallego Arias	2017-04-25
\|/ / /
\| \| *	Adding a dedicated travis overlay for fiat-parsers.	Pierre-Marie Pédrot	2017-04-24
\| \|/ \|/\|
\| *	Add bedrock targets src and facade	Jason Gross	2017-04-20
\| \|
* \|	Merge branch 'v8.6' into trunk	Maxime Dénès	2017-04-15
\|\\|
\| *	[travis] Use the lite target for fiat-crypto.	Maxime Dénès	2017-04-14
\| \|
* \|	[travis] Overlay for PR#461: Camlp4 removal.	Emilio Jesus Gallego Arias	2017-04-07
\| \|
\| *	[travis] Backport from trunk: VST	Emilio Jesus Gallego Arias	2017-03-24
\| \|
* \|	[travis] Add VST	Emilio Jesus Gallego Arias	2017-03-24
\| \|
* \|	[travis] Fix iris-coq build.	Emilio Jesus Gallego Arias	2017-03-22
\| \| \| \| \| \| \| \| \| \| \| \| \| \|	We need to do a bit of hacking, but it should be fine for the short term. c.f. https://gitlab.mpi-sws.org/FP/iris-coq/issues/83
\| *	[travis] [8.6.only] Backport latest changes from trunk.	Emilio Jesus Gallego Arias	2017-03-22
\| \|
* \|	trivial: fix comment	Matej Kosik	2017-03-21
\| \|
* \|	[travis] Basic support for overlays.	Emilio Jesus Gallego Arias	2017-03-13
\| \| \| \| \| \| \| \| \| \| \| \| \| \|	We now allow the user to overlay contribution repositories and branches by adding their own rules to `ci-basic-overlay.sh`. This just provides very basic support.
* \|	[travis] Make the git_checkout function more reliable.	Théo Zimmermann	2017-03-10
\| \| \| \| \| \| \| \| \| \| \| \|	This commit also documents the behavior of said function; and fix the location of the ssreflect clone to an absolute path (this is now necessary).
* \|	[travis] Adding a template file and using it for all targets.	Théo Zimmermann	2017-03-10
\| \|
* \|	[travis] Change headband for wider compatibility.	Théo Zimmermann	2017-03-10
\| \|
* \|	Improve build of travis target on local machine.	Théo Zimmermann	2017-03-10
\| \| \| \| \| \| \| \| \| \|	- Move the git clones to a specific subfolder to avoid pollution. - Do not fail when git clone already exist (but make sure it is up-to-date).
\| *	[travis] Move GeoCoq to allow fail.	Emilio Jesus Gallego Arias	2017-03-10
\| \| \| \| \| \| \| \|	We need to agree a bit more with upstream.
* \|	[travis] Move GeoCoq to allow fail.	Emilio Jesus Gallego Arias	2017-03-09
\| \| \| \| \| \| \| \|	We need to agree a bit more with upstream.
\| *	[travis] Backport trunk's travis support.	Emilio Jesus Gallego Arias	2017-03-02
\|
*	[travis] [External CI] fiat-parsers	Emilio Jesus Gallego Arias	2017-02-24
\|
*	[travis] track an 8.7 specific branch of HoTT.	Maxime Dénès	2017-02-21
\| \| \| \|	This is required since we merged PR#309: Ltac as a plugin.
*	[travis] [External CI] CompCert official 8.6 support + UniMath	Emilio Jesus Gallego Arias	2017-02-15
\|
*	[travis] [External CI] Factor out math-comp installs.	Emilio Jesus Gallego Arias	2017-02-15
\| \| \| \| \|	We make math-comp overlays easier, we also start structuring the scripts a bit more.
*	Merge PR#425: [travis] [External CI] [geocoq] don't build slow file	Maxime Dénès	2017-02-07
\|\
\| *	[travis] [External CI] [geocoq] don't build slow file	Emilio Jesus Gallego Arias	2017-02-07
\| \| \| \| \| \| \| \| \| \|	Unfortunately `Ch16_coordinates_with_functions.v` takes alone ~15 minutes which is too much for Travis. Pity, because it was a nice use case.