coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Merge PR #7798: Remove hack skipping comparison of algebraic universes in ↵	Matthieu Sozeau	2018-06-25
\|\ \| \| \| \| \| \|	subtyping.
* \	Merge PR #7559: Existing Class noop when already a class + warning.	Matthieu Sozeau	2018-06-25
\|\ \
* \ \	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
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| \| \| \| \| \| \| \| *	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.
* \| \| \| \| \| \| \| \| \| \| \|	Merge PR #7774: [build] Fix checks and notes noting 4.02.1 instead of 4.02.3	Maxime Dénès	2018-06-21
\|\ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #7873: Make Clément the secondary codeowner of doc/tools/coqrst.	Maxime Dénès	2018-06-21
\|\ \ \ \ \ \ \ \ \ \ \ \ \
\| \| \| * \| \| \| \| \| \| \| \| \| \|	Update dpdgraph branch name	Gaëtan Gilbert	2018-06-21
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	See https://github.com/Karmaki/coq-dpdgraph/issues/50 for context
* \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #7770: Move indices on top on the TOC. Closes #7764.	Maxime Dénès	2018-06-21
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \| \|_\|_\|/ / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #7815: On cygwin, pass the filename in a format that coqdoc ↵	Maxime Dénès	2018-06-21
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	understands.
* \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #7865: Fix #7432: Grammar token @term points to the SSR chapter.	Maxime Dénès	2018-06-21
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| *	Remove enforce_leq from checker	Gaëtan Gilbert	2018-06-21
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #7842: Fix #7836: tools/inferior-coq.el uses next-line instead of ↵	Pierre Courtieu	2018-06-21
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	forward-line.
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #7880: Clean up Dyn	Pierre-Marie Pédrot	2018-06-21
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\| * \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Add documentation for Dyn.	whitequark	2018-06-21
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| * \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Rename Dyn.TParam→ValueS, Dyn.MapS.obj→value to clarify their purpose.	whitequark	2018-06-21
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| * \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Reformat Dyn.{ml,mli}.	whitequark	2018-06-21
\|/ / / / / / / / / / / / / / / / /
\| \| \| * \| \| \| \| \| \| \| \| \| \| \| \| \|	On cygwin, pass the filename in a format that coqdoc understands.	Jim Fehrle	2018-06-20
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #7868: [coqtop] Give priority to stdlib load path over current ↵	Emilio Jesus Gallego Arias	2018-06-20
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	directory
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| * \| \|	[ssr] test case for rewrite (setoid) making the goal illtyped	Enrico Tassi	2018-06-20
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| * \| \|	[ssr] rewrite: turn anomaly into regular error	Enrico Tassi	2018-06-20
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	I think the bug was introduces when apply_type was made safe. In the test joint to #7255 rewrite (setoid case) generates an ill-typed goal and apply_type raises a Pretype_error. It is unclear to me why the tactic monad does not turn the pretype_error into a UserError
\| \| \| \| \| \| * \| \| \| \| \| \| \| \| \| \|	Make Clément the secondary codeowner of doc/tools/coqrst.	Théo Zimmermann	2018-06-20
\| \|_\|_\|_\|_\|/ / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| *	Fix Univ.enforce_leq dropped constraints when algebraic on the right	Gaëtan Gilbert	2018-06-19
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	There's probably a proof of false using subtyping if someone wants to look. NB: the checker doesn't handle algebraics on the right.
\| * \| \| \| \| \| \| \| \| \| \| \| \| \|	[coqtop] Give priority to stdlib load path over current directory	Maxime Dénès	2018-06-19
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	When initilazing the load path, coqtop adds implicit bindings for stdlib and for the current directory (-R stdlib Coq -R . ""). In case of a clash, the binding of the current directory had priority, which makes it impossible to edit stdlib files (when they Require files from the same directory) using PG, or from CoqIDE when launched from the directory containing the file. Example to reproduce the problem: ``` cd plugins/omega coqide Omega.v ``` some of the Requires will fail.
* \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #7797: Remove reference name type.	Enrico Tassi	2018-06-19
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6754: Better elaboration of pattern-matchings on primitive projections	Pierre-Marie Pédrot	2018-06-19
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #7491: Fix #7421: constr_eq ignores universe constraints.	Pierre-Marie Pédrot	2018-06-19
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \