aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2018-08-31Numeral Notation + test-suite : fix 3 tests using Datatypes.v but not Prelude.vPierre Letouzey
2018-08-31Numeral Notation: use the modern warning infrastructurePierre Letouzey
2018-08-31Numeral Notation: minor text improvements suggested by J. GrossPierre Letouzey
2018-08-31Error on polymorphic conversions for numeral notationsJason Gross
2018-08-31Fix grammarJason Gross
2018-08-31Numeral Notation: some documentation in the refmanPierre Letouzey
2018-08-31remove legacy syntax plugins subsumed by Numeral NotationPierre Letouzey
2018-08-31Numeral Notation for natPierre Letouzey
2018-08-31Numeral Notation: allow parsing from/to Decimal.int or Decimal.uintPierre Letouzey
2018-08-31remove test file NatSyntaxViaZ.vPierre Letouzey
2018-08-31Numeral Notation: misc code improvements (records, subfunctions, exceptions ...)Pierre Letouzey
2018-08-31Numeral Notation (for inductive types)Pierre Letouzey
2018-08-31prim notations backtrackable, their declarations now in two parts (API change)Pierre Letouzey
2018-08-31Prelude : update the comment about ML plugins loaded by InitPierre Letouzey
2018-08-31Extraargs: avoid two token declarations to appear in all .voPierre Letouzey
2018-08-31Tacenv: minor code cleanupPierre Letouzey
2018-08-31Notation: remove support for prim tokens denoting inductive types in "return"Pierre Letouzey
2018-08-31Notation: avoid one intermediate (unit -> ...)Pierre Letouzey
2018-08-31Notation: no more chains of prim_token_interpreterPierre Letouzey
2018-09-01Merge PR #8348: Download tarball instead of cloning external projects.Emilio Jesus Gallego Arias
2018-08-31Trying to make the code of conduct shorter and more to the point.Théo Zimmermann
2018-08-31Move paragraph on Coq-related subjects up.Théo Zimmermann
2018-08-31Add paragraph contributed by Cyril Cohen.Théo Zimmermann
2018-08-31Expand the section on enforcement:Théo Zimmermann
2018-08-31Add code owners for the Code of Conduct.Théo Zimmermann
2018-08-31Make goal that everyone feel safe more explicit.Théo Zimmermann
2018-08-31Suggestions by Hugo.Théo Zimmermann
2018-08-31Permalink to Django code of conduct using Archive.org.Théo Zimmermann
2018-08-31Propose a Code of Conduct for Coq.Théo Zimmermann
2018-08-31Merge PR #8346: Clean-up Travis folds.Gaëtan Gilbert
2018-08-31Merge PR #8351: [ci] [docker] Update base Dune version.Gaëtan Gilbert
2018-08-31Merge PR #8170: Don't index names starting with `_` in docsThéo Zimmermann
2018-08-31Merge PR #8219: Refman consistency checkThéo Zimmermann
2018-08-31Download tarball instead of cloning external projects (when $CI is set).Théo Zimmermann
2018-08-31Merge PR #8368: [ci] Fix QuickChick by adding new simple-io dependency.Gaëtan Gilbert
2018-08-31[ci] Fix QuickChick by adding new simple-io dependency.Théo Zimmermann
2018-08-31Fixed the seealso directive in a few places.Zeimer
2018-08-31Uniformized many spelling variants. Added .. warning:: and .. seealso:: direc...Zeimer
2018-08-30Replace use of xargs in "make clean", which tends to fail on Windows/Cygwin.Jim Fehrle
2018-08-30Fix #8361: dependency states: camldevfilesGaëtan Gilbert
2018-08-30[ci] [docker] Update Dune and Elpi versions.Emilio Jesus Gallego Arias
2018-08-30[ssr] move ssr_*v tests to test-suite/ssr/Enrico Tassi
2018-08-30Merge PR #8354: Move CHANGES entry for #8167 to 8.8.2 sectionThéo Zimmermann
2018-08-30Merge PR #8349: Mention dev/doc/critical-bugs in CONTRIBUTINGThéo Zimmermann
2018-08-30Merge PR #8292: Create SPHINXWARNERROR variable to control Sphinx "warn as er...Théo Zimmermann
2018-08-29Merge PR #8353: [sphinx] Fix timeout issue by splitting imports.Clément Pit-Claudel
2018-08-29Merge PR #8345: Add index for focusing braces.Clément Pit-Claudel
2018-08-29Create SPHINXWARNERROR variable that controls whether the SphinxJim Fehrle
2018-08-29Move CHANGES entry for #8167 to 8.8.2 sectionJason Gross
2018-08-29Move mention of dev/doc/critical-bugs to CONTRIBUTINGJason Gross