coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
\| \| \| \| \| \| \| \| \| \| \| \| \| * \|	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
\| \| \| \| \| \| \| \| \| \| \| \| \| * \|	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 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
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| *	Fix #7704: get_toplevel_path needs normalised argv.(0)	Gaëtan Gilbert	2018-06-22
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| * \| \|	Fix handling of universe context for expanded program obligations.	Matthieu Sozeau	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
\| \|_\|_\|_\|_\|_\|_\|_\|/ / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| \| \| \| * \| \|	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 INSTA...	Théo Zimmermann	2018-06-22
\| \| \| \| \| \| \| \| \| \| \| \| \| * \| \|	Clarify further doc/README.md following Jim's comments.	Théo Zimmermann	2018-06-22
\| \| \| \| \| \| \| \| \| \| \| \| \| * \| \|	Fix copyright dates in doc/LICENSE.	Théo Zimmermann	2018-06-22
\| \| \| \| \| \| \| \| \| \| \| \| \| * \| \|	Improve doc/README.md.	Théo Zimmermann	2018-06-22
\| \| \| \| \| \| \| \| \| \| \| \| \| * \| \|	Move INSTALL.doc into doc/README.md.	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
\|/ / / / / / / / / / / / / / / / / / / /
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| * \| \|	Mention Company-Coq as well.	Théo Zimmermann	2018-06-20
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| * \| \|	Add a good reference for Proof-General as suggested by Clément.	Théo Zimmermann	2018-06-20