coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
...
\| \| \| \| \| \| * \| \| \|	Make Environ.globals abstract.	Gaëtan Gilbert	2018-06-28
\| \|_\|_\|_\|_\|/ / / / \|/\| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \|	Merge PR #7932: CoqIDE scrolls the proof buffer down to the first goal.	Pierre-Marie Pédrot	2018-06-28
\|\ \ \ \ \ \ \ \ \
\| \| \| \| * \| \| \| \| \|	Update maintainers for native/VM files in pretyping	Maxime Dénès	2018-06-28
\| \|_\|_\|/ / / / / / \|/\| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \|	Merge PR #7866: Implementation of mutual records in the higher strata	Maxime Dénès	2018-06-28
\|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \	Merge PR #7934: Add mit-plv/bedrock2-ci to CI	Emilio Jesus Gallego Arias	2018-06-28
\|\ \ \ \ \ \ \ \ \ \
\| * \| \| \| \| \| \| \| \| \|	Add mit-plv/bedrock2-ci to CI	Andres Erbsen	2018-06-27
\|/ / / / / / / / / /
* \| \| \| \| \| \| \| \| \|	Merge PR #7768: Fix #7723 (vm_compute segfault and proof of false)	Pierre-Marie Pédrot	2018-06-27
\|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \	Merge PR #7939: Turn the CoqProject_file module into a pure ML file	Emilio Jesus Gallego Arias	2018-06-27
\|\ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| * \| \| \| \| \|	Mention Consortium in README	Maxime Dénès	2018-06-27
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	We are now actively looking for sponsors, let's make our communication more visible.
\| \| \| \| \| \| \| \| \| \| * \|	Adding overlay.	Hugo Herbelin	2018-06-27
\| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| * \|	Swapping Context and Constr: defining declarations on constr in Constr.	Hugo Herbelin	2018-06-27
\| \|_\|_\|_\|_\|_\|_\|_\|_\|/ / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This shall eventually allow to use contexts of declarations in the definition of the "Case" constructor. Basically, this means that Constr now includes Context and that the "t" types of Context which were specialized on constr are not defined in Constr (unfortunately using a heavy boilerplate).
* \| \| \| \| \| \| \| \| \| \|	Merge PR #7924: Ad hoc fix for #5696, #7903 (ltac subterms and open subterms ↵	Emilio Jesus Gallego Arias	2018-06-27
\|\ \ \ \ \ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	in notations).
\| \| * \| \| \| \| \| \| \| \| \|	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
\| \|/ / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| * \| \| \|	Fix 'unbound variable' issue on Windows packaging jobs.	Théo Zimmermann	2018-06-27
\| \| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \|	Merge PR #7863: Remove Sorts.contents	Pierre-Marie Pédrot	2018-06-27
\|\ \ \ \ \ \ \ \ \ \ \
\| \| \| * \| \| \| \| \| \| \| \|	Test file for #7723	Maxime Dénès	2018-06-27
\| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| * \| \| \| \| \| \|	CoqIDE scrolls the proof buffer down to the first goal.	Cyprien Mangin	2018-06-27
\| \| \| \| \| \| \|_\|/ / / / \| \| \| \| \| \|/\| \| \| \| \|
\| \| \| * \| \| \| \| \| \| \|	Fix #7723: vm_compute segfaults with universe polymorphism	Maxime Dénès	2018-06-27
\| \| \| \| \|_\|_\|/ / / / \| \| \| \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Was revealing a critical bug in VM universe handling introduced in 8.5.
* \| \| \| \| \| \| \| \| \|	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
\|\ \ \ \ \ \ \ \ \ \ \ \| \|_\|_\|_\|_\|_\|/ / / / / \|/\| \| \| \| \| \| \| \| \| \|
\| \| \| \| * \| \| \| \| \| \|	Ad hoc fix for #5696, #7903 (ltac subterms and open subterms in notations).	Hugo Herbelin	2018-06-26
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	We fix the issue by removing terms of the substitutions which have free variables and are thus not interpretable in the context of the "ltac:" subterm. This remains rather ad hoc, since, in an expression "Notation f x := ltac:(foo)", we interpret "x" at calling time of "foo" rather than at use time of "x" in foo, even if "x" is not necessary. We could also imagine that binders in the ltac expressions are then interpreted but that would start to be (very) complicated. Note that this will presumably "fix" ltac2 quotations at the same time.
* \| \| \| \| \| \| \| \| \| \|	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.
\| \| \| \| \| \| \| \| \| \| \| \| \| *	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.