coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Ad hoc fix for #5696, #7903 (ltac subterms and open subterms in notations).	Hugo Herbelin	2018-06-26
*	Merge PR #7798: Remove hack skipping comparison of algebraic universes in sub...	Matthieu Sozeau	2018-06-25
\|\
* \	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 kerne...	Maxime Dénès	2018-06-23
\|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \	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
\| * \| \| \| \| \| \| \| \| \| \|	Using more general information for primitive records.	Pierre-Marie Pédrot	2018-06-23
\| * \| \| \| \| \| \| \| \| \| \|	Change the proj_ind field from MutInd.t to inductive.	Pierre-Marie Pédrot	2018-06-23
\|/ / / / / / / / / / /
* \| \| \| \| \| \| \| \| \| \|	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
\| \| \| \| \| \| \| \| \| \| \| \| \| \| *	Define and use UGraph.enforce_leq_alg for subtyping inference	Gaëtan Gilbert	2018-06-22
\| \| \| \| \| \| * \| \| \| \| \| \| \| \|	[ssr] document {}/view	Enrico Tassi	2018-06-22
\| \| \| \| \| \| * \| \| \| \| \| \| \| \|	[ssr] document rewrite {}foo	Enrico Tassi	2018-06-22
\| \| \| \| \| \| * \| \| \| \| \| \| \| \|	[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
\| \|_\|_\|_\|_\|/ / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \|
\| * \| \| \| \| \| \| \| \| \| \| \| \|	[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
\| \|_\|_\|_\|_\|_\|_\|_\|/ / / / \|/\| \| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \| \|	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
* \| \| \| \| \| \| \| \| \| \| \| \| \|	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 understa...	Maxime Dénès	2018-06-21
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \	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 fo...	Pierre Courtieu	2018-06-21
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	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 direc...	Emilio Jesus Gallego Arias	2018-06-20
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| * \| \|	[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
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| * \| \| \| \| \| \| \| \| \| \|	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
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| * \| \| \| \| \| \| \| \| \| \| \| \| \|	[coqtop] Give priority to stdlib load path over current directory	Maxime Dénès	2018-06-19
* \| \| \| \| \| \| \| \| \| \| \| \| \| \|	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
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \