coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Slightly less crazy parsing algorithm for CoqProject_file.	Pierre-Marie Pédrot	2018-06-27
\| \| \| \| \|	We use a buffer instead of O(n) appending to a string, and we also make the parser tail-call.
*	Turn CoqProject_file into a normal OCaml file.	Pierre-Marie Pédrot	2018-06-27
\|
*	Merge PR #7863: Remove Sorts.contents	Pierre-Marie Pédrot	2018-06-27
\|\
* \	Merge PR #7888: Clarify the message "this hint will only be used by eauto"	Pierre-Marie Pédrot	2018-06-27
\|\ \
* \ \	Merge PR #7826: evd: restrict_evar with candidates, can raise NoCandidatesLeft	Hugo Herbelin	2018-06-26
\|\ \ \
* \ \ \	Merge PR #7906: universes_of_constr don't include universes of monomorphic ↵	Pierre-Marie Pédrot	2018-06-26
\|\ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	constants
* \ \ \ \	Merge PR #7775: Fix handling of universe context for expanded program ↵	Maxime Dénès	2018-06-26
\|\ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	obligations.
* \ \ \ \ \	Merge PR #7831: Fix for issue #7707: include Ltac2 and Equations in Windows ↵	Maxime Dénès	2018-06-26
\|\ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	build
* \ \ \ \ \ \	Merge PR #7756: Fix #7608: missing num package in INSTALL documentation.	Maxime Dénès	2018-06-26
\|\ \ \ \ \ \ \
* \ \ \ \ \ \ \	Merge PR #7783: Move INSTALL.doc to doc/README.md and improve a few things.	Maxime Dénès	2018-06-26
\|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \	Merge PR #7919: Fix equality check on global names from native compute.	Maxime Dénès	2018-06-26
\|\ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| \| \| *	Add overlay for elpi	Gaëtan Gilbert	2018-06-26
\| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| *	Remove Sorts.contents	Gaëtan Gilbert	2018-06-26
\| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| * \| \| \|	Add overlay for Equations, Elpi	Gaëtan Gilbert	2018-06-26
\| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| * \| \| \|	universes_of_constr don't include universes of monomorphic constants	Gaëtan Gilbert	2018-06-26
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Apparently it was not useful. I don't remember what I was thinking when I added it.
* \| \| \| \| \| \| \| \| \|	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.
* \| \| \| \| \| \| \| \|	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
\|\ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \	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 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.