aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2018-06-22Fix #7608: missing num package in INSTALL documentation.Théo Zimmermann
2018-06-22Fix Windows install script following removal of INSTALL.ide and move of INSTA...Théo Zimmermann
2018-06-22Clarify further doc/README.md following Jim's comments.Théo Zimmermann
2018-06-22Fix copyright dates in doc/LICENSE.Théo Zimmermann
2018-06-22Improve doc/README.md.Théo Zimmermann
2018-06-22Move INSTALL.doc into doc/README.md.Théo Zimmermann
2018-06-21Merge PR #7774: [build] Fix checks and notes noting 4.02.1 instead of 4.02.3Maxime Dénès
2018-06-21Merge PR #7873: Make Clément the secondary codeowner of doc/tools/coqrst.Maxime Dénès
2018-06-21Update dpdgraph branch nameGaëtan Gilbert
2018-06-21Merge PR #7770: Move indices on top on the TOC. Closes #7764.Maxime Dénès
2018-06-21Further cleanup: do not export the closed_term Ltac entry.Pierre-Marie Pédrot
2018-06-21Merge PR #7815: On cygwin, pass the filename in a format that coqdoc understa...Maxime Dénès
2018-06-21Inline a function from Quote used in setoid_ring.Pierre-Marie Pédrot
2018-06-21Merge PR #7865: Fix #7432: Grammar token @term points to the SSR chapter.Maxime Dénès
2018-06-21Remove enforce_leq from checkerGaëtan Gilbert
2018-06-21Merge PR #7842: Fix #7836: tools/inferior-coq.el uses next-line instead of fo...Pierre Courtieu
2018-06-21Merge PR #7880: Clean up DynPierre-Marie Pédrot
2018-06-21Fix #5719: Uncaught exception Invalid_argument.Pierre-Marie Pédrot
2018-06-21Add documentation for Dyn.whitequark
2018-06-21Rename Dyn.TParam→ValueS, Dyn.MapS.obj→value to clarify their purpose.whitequark
2018-06-21Reformat Dyn.{ml,mli}.whitequark
2018-06-20Mention Company-Coq as well.Théo Zimmermann
2018-06-20Add a good reference for Proof-General as suggested by Clément.Théo Zimmermann
2018-06-20Modernize the introduction of the reference manual.Théo Zimmermann
2018-06-20On cygwin, pass the filename in a format that coqdoc understands.Jim Fehrle
2018-06-20Merge 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 illtypedEnrico Tassi
2018-06-20[ssr] rewrite: turn anomaly into regular errorEnrico Tassi
2018-06-20Make Clément the secondary codeowner of doc/tools/coqrst.Théo Zimmermann
2018-06-19Fix Univ.enforce_leq dropped constraints when algebraic on the rightGaëtan Gilbert
2018-06-19[coqtop] Give priority to stdlib load path over current directoryMaxime Dénès
2018-06-19Merge PR #7797: Remove reference name type.Enrico Tassi
2018-06-19Merge PR #6754: Better elaboration of pattern-matchings on primitive projectionsPierre-Marie Pédrot
2018-06-19Merge PR #7491: Fix #7421: constr_eq ignores universe constraints.Pierre-Marie Pédrot
2018-06-19Merge PR #7801: [vernac] Add option to force building really mutual induction...Enrico Tassi
2018-06-19Merge PR #7841: Remove CanaryPierre-Marie Pédrot
2018-06-19[doc] Rewrite and document the prodn directiveClément Pit-Claudel
2018-06-19[doc] Fix a typo in the ssreflect chapterClément Pit-Claudel
2018-06-19[doc] Fix uncaught duplicate-label errors in the SSReflect chapterClément Pit-Claudel
2018-06-19[doc] Use productionlist instead of prodn in ring.rstClément Pit-Claudel
2018-06-19Merge PR #7714: Remove primitive-projection related data from the kernelMaxime Dénès
2018-06-19Merge PR #7856: Fix #7829: Spurious documentation failures.Maxime Dénès
2018-06-18Overlay for reference removalMaxime Dénès
2018-06-18Merge PR #7855: Update section on adding your project to CI and link to examp...Emilio Jesus Gallego Arias
2018-06-18Fix #7421: constr_eq ignores universe constraints.Gaëtan Gilbert
2018-06-18Remove Canary.whitequark
2018-06-18Fix #7829: Spurious documentation failures.Théo Zimmermann
2018-06-18Merge PR #7840: Remove Hashcons.HobjPierre-Marie Pédrot
2018-06-18Update section on adding your project to CI and link to example PR.Théo Zimmermann
2018-06-18Remove reference name type.Maxime Dénès