coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
...
* \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #7851: Modernize the introduction of the reference manual.	Maxime Dénès	2018-06-26
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \| \|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| * \| \| \| \| \| \| \| \| \|	Activate the build of Ltac2 and Equations in the Windows installer.	Théo Zimmermann	2018-06-25
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| * \| \| \| \| \| \| \| \| \|	Reuse CI info to know which version of plugins to build on Windows.	Théo Zimmermann	2018-06-25
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #7798: Remove hack skipping comparison of algebraic universes in ↵	Matthieu Sozeau	2018-06-25
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	subtyping.
\| \| \| \| \| \| \| \| \| \| * \| \| \| \| \|	Clarify the message "this hint will only be used by eauto"	Armaël Guéneau	2018-06-25
\| \|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| * \| \| \| \| \| \| \| \|	Fix for issue 7707: include Ltac2 and Equations in Windows build	Michael Soegtrop	2018-06-25
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	On the way I also fixed some minor issues with calling MakeCoq_MinGW from cygwin.
* \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #7559: Existing Class noop when already a class + warning.	Matthieu Sozeau	2018-06-25
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \| \|_\|_\|_\|_\|_\|/ / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| * \| \| \| \| \| \| \| \| \| \|	Fix equality check on global names from native compute.	Pierre-Marie Pédrot	2018-06-25
\| \|_\|_\|/ / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Not sure it could have led to a soundness bug, but this is definitely serious enough to deserve a backport. Also made the code robust by listing all the constructors.
\| \| \| \| \| \| \| \| \| \| \| \| \| *	Mini-update of version history with recent changes.	Hugo Herbelin	2018-06-25
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ \|/\| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| * \| \|	Critical bugs: added #3243 and Gonthier's bug in lazy machine.	Hugo Herbelin	2018-06-25
\| \|_\|_\|_\|_\|_\|_\|_\|_\|/ / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Both reminded by Enrico.
* \| \| \| \| \| \| \| \| \| \| \|	Merge PR #7620: [ssr] rewrite: turn anomaly into regular error	Maxime Dénès	2018-06-25
\|\ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #7895: Revert "Add a note about [ci skip] in CI README."	Emilio Jesus Gallego Arias	2018-06-24
\|\ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #7805: Towards listing the critical bugs of the history of Coq.	Théo Zimmermann	2018-06-24
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #7772: [native_compute] Delay computations with toplevel match	Pierre-Marie Pédrot	2018-06-24
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| \| \| \| \| \| \| * \| \|	Documenting the syntax of mutual keywords.	Pierre-Marie Pédrot	2018-06-24
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| \| \| * \| \|	Added mention of mutual records to CHANGES.	Pierre-Marie Pédrot	2018-06-24
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| \| \| * \| \|	Adding various tests for mutual records.	Pierre-Marie Pédrot	2018-06-24
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| \| \| * \| \|	Handle mutual record at the vernac level.	Pierre-Marie Pédrot	2018-06-24
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Highly spaghetti code, hopefully works.
\| \| \| \| \| \| \| \| \| \| \| \| \| * \| \|	Handle mutual records in upper layers.	Pierre-Marie Pédrot	2018-06-24
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #7784: Remove Tutorials from a few other places following #7466.	Maxime Dénès	2018-06-24
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #7614: Simplify the code that handles trust of side-effects in ↵	Maxime Dénès	2018-06-23
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	kernel typing.
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #7236: [ssr] simpler semantics for delayed clears	Maxime Dénès	2018-06-23
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #7827: [engine] safe [add_unification_pb] interface	Pierre-Marie Pédrot	2018-06-23
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #7750: Handle mutual records in the kernel	Maxime Dénès	2018-06-23
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\| * \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Adapt the kernel to generate proper data for mutual records.	Pierre-Marie Pédrot	2018-06-23
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Upper layers are still not able to handle mutual records though.
\| * \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Using more general information for primitive records.	Pierre-Marie Pédrot	2018-06-23
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This brings more compatibility with handling of mutual primitive records in the kernel.
\| * \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Change the proj_ind field from MutInd.t to inductive.	Pierre-Marie Pédrot	2018-06-23
\|/ / / / / / / / / / / / / / / / / / / \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This is a first step towards the acceptance of mutual record types in the kernel.
* \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #7715: Simplify the cooking of primitive projections.	Maxime Dénès	2018-06-23
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #7600: Faster and cleaner fconstr-to-constr conversion function.	Maxime Dénès	2018-06-22
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #7893: Update dpdgraph branch name	Théo Zimmermann	2018-06-22
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #7776: [ssr] Fix rewrite with universes	Maxime Dénès	2018-06-22
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| * \|	Fix #7704: get_toplevel_path needs normalised argv.(0)	Gaëtan Gilbert	2018-06-22
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	When launched through PATH argv.(0) is just the command name. eg "coqtop -compile foo.v" -> argv.(0) = "coqtop" Using executable_name also follows symlinks but this isn't tested to avoid messing with windows. Running Coq through a symlink is not as important as PATH anyways.
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| * \| \| \|	Fix handling of universe context for expanded program obligations.	Matthieu Sozeau	2018-06-22
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	The universe context was dropped even though it isn't added to the global universes yet. Keep it so that it is properly defined with the constant the expanded obligation appears in.
\| \| \| \| \| \| \| \| \| \| \| \| \| \| * \| \| \| \| \| \|	Remove hack skipping comparison of algebraic universes in subtyping.	Gaëtan Gilbert	2018-06-22
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	When inferring [u <= v+k] I replaced the exception and instead add [u <= v]. This is trivially sound and it doesn't seem possible to have the one without the other (except specially for [Set <= v+k] which was already handled). I don't know an example where this used to fail and now succeeds (the point was to remove an anomaly, but the example ~~~ Module Type SG. Definition DG := Type. End SG. Module MG : SG. Definition DG := Type : Type. Fail End MG. ~~~ now fails with universe inconsistency. Fix #7695 (soundness bug!).
\| \| \| \| \| \| \| \| \| \| \| \| \| \| * \| \| \| \| \| \|	Define and use UGraph.enforce_leq_alg for subtyping inference	Gaëtan Gilbert	2018-06-22
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Not sure if worth using in other places.
\| \| \| \| \| \| * \| \| \| \| \| \| \| \| \| \| \| \| \| \|	[ssr] document {}/view	Enrico Tassi	2018-06-22
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| * \| \| \| \| \| \| \| \| \| \| \| \| \| \|	[ssr] document rewrite {}foo	Enrico Tassi	2018-06-22
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	It was used in some examples, but never fully documented
\| \| \| \| \| \| * \| \| \| \| \| \| \| \| \| \| \| \| \| \|	[ssr] implement {}/v as a short hand for {v}/v when v is an id	Enrico Tassi	2018-06-22
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| * \| \| \| \| \| \| \| \| \| \| \| \| \| \|	[ssr] simplify delayed clears	Enrico Tassi	2018-06-22
\| \|_\|_\|_\|_\|/ / / / / / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	- we always rename - we compile {clear}/view to /view{clear}
\| * \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	[ssr] test case for rewrite and set on univ poly keys	Enrico Tassi	2018-06-22
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| * \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	[ssr] matching: use eq_constr_nounivs in approximated matching	Enrico Tassi	2018-06-22
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| * \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	[ssr] set: merge universe constraints before type checking the term	Enrico Tassi	2018-06-22
\|/ / / / / / / / / / / / / / / / / / /
\| \| \| \| \| \| \| \| \| * / / / / / / / / /	Revert "Add a note about [ci skip] in CI README."	Théo Zimmermann	2018-06-22
\| \|_\|_\|_\|_\|_\|_\|_\|/ / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This reverts commit 3a44a190a7f5d057b6a4bcb50124b42d83f3d03d.
\| \| \| \| \| \| \| \| \| \| \| \| \| \| * \| \| \|	Get rid of INSTALL.ide. List the dependency versions in INSTALL.	Théo Zimmermann	2018-06-22
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| \| \| \| * \| \| \|	Fix #7608: missing num package in INSTALL documentation.	Théo Zimmermann	2018-06-22
\| \| \| \| \| \| \| \| \| \| \| \| \| \|/ / / /
\| \| \| \| \| \| \| \| \| \| \| \| \| * \| \| \|	Fix Windows install script following removal of INSTALL.ide and move of ↵	Théo Zimmermann	2018-06-22
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	INSTALL.doc.
\| \| \| \| \| \| \| \| \| \| \| \| \| * \| \| \|	Clarify further doc/README.md following Jim's comments.	Théo Zimmermann	2018-06-22
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Relative links. Cf. #7800.
\| \| \| \| \| \| \| \| \| \| \| \| \| * \| \| \|	Fix copyright dates in doc/LICENSE.	Théo Zimmermann	2018-06-22
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	[ci skip]
\| \| \| \| \| \| \| \| \| \| \| \| \| * \| \| \|	Improve doc/README.md.	Théo Zimmermann	2018-06-22
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	- Fix the Markdown. - Add link to latest build of the refman for the master branch. - Clarify what are the dependencies of the HTML doc. [ci skip]
\| \| \| \| \| \| \| \| \| \| \| \| \| * \| \| \|	Move INSTALL.doc into doc/README.md.	Théo Zimmermann	2018-06-22
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This will avoid in particular this ambiguous file extension. [ci skip]