aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2018-01-16Merge PR #6466: Replace md5sum/md5 calls by an OCaml programMaxime Dénès
2018-01-16Merge PR #6551: Bracket with goal selectorMaxime Dénès
2018-01-16Add plugins to META.coqCyprien Mangin
2018-01-15Fix the wrapper around ocamldebug.Pierre-Marie Pédrot
2018-01-15Avoid shell backticks and improve md5sum.ml error messagesJacques-Pascal Deplaix
2018-01-15More tests on brackets with goal selectors (including failures).Théo Zimmermann
2018-01-15Add test-suite file for bracket with goal selector.Théo Zimmermann
2018-01-14Actually use the strategy information in the checker.Pierre-Marie Pédrot
2018-01-14Store the conversion oracle in constant and inductive definitions.Pierre-Marie Pédrot
2018-01-13Merge PR #6578: Remove references to deleted Unicode.Unsupported exceptionMaxime Dénès
2018-01-13Merge PR #6581: Added newline at the end of usage of coqdep.Maxime Dénès
2018-01-13Merge PR #6564: Fix undefined variables in test-suite/Makefile + add PRINT_LOGSMaxime Dénès
2018-01-12Merge PR #6483: Strong invariants in polymorphic definitionsMaxime Dénès
2018-01-12Merge PR #6288: Interfaces for checker and IDE.Maxime Dénès
2018-01-11Adding a custom Travis overlay for HoTT.Pierre-Marie Pédrot
2018-01-11Enforce that polymorphic definitions do not generate internal constraints.Pierre-Marie Pédrot
2018-01-11Document test-suite PRINT_LOGS.Gaëtan Gilbert
2018-01-11Fix undefined variables in test-suite/Makefile + add PRINT_LOGSGaëtan Gilbert
2018-01-11Merge PR #6557: First stab at documenting the test suite.Maxime Dénès
2018-01-11Merge PR #6552: [PR template] Remove the relative link to CHANGES.Maxime Dénès
2018-01-11Added newline at the end of usage of coqdep.Bernhard Schommer
2018-01-11Force polymorphic definitions to have no internal constraints.Pierre-Marie Pédrot
2018-01-11Remove references to removed Unicode.UnsupportedJasper Hugunin
2018-01-11Lint and remove redundant lineJasper Hugunin
2018-01-10Add interfaces for IDE and remove dead code.Maxime Dénès
2018-01-10Add interfaces for checker and remove dead code.Maxime Dénès
2018-01-10Merge PR #6519: Python script checking missing/unnecessary [needs: rebase] labelMaxime Dénès
2018-01-10Merge PR #6570: [meta] Fix typo on Coq's META file following #6444.Maxime Dénès
2018-01-10Add comments by @psteckler to test-suite/README.mdJasper Hugunin
2018-01-09[meta] Fix typo on Coq's META file following #6444.Emilio Jesus Gallego Arias
2018-01-08Cleanup conditional in lint-repository.shGaëtan Gilbert
2018-01-08Stop talking about debian in "A note about rlwrap"Gaëtan Gilbert
2018-01-08[vernac] vernac_expr no longer recursiveVincent Laporte
2018-01-08Merge PR #6532: Fix mli-doc issue #6531Maxime Dénès
2018-01-08Merge PR #6489: Update PNGs; mention async error handling; change query windo...Maxime Dénès
2018-01-08Merge PR #6497: Add optimize_heap tactic for #6488Maxime Dénès
2018-01-08Merge PR #6549: Normalize package namesMaxime Dénès
2018-01-08Merge PR #6533: Update the lower-bound of the lablgtk dependency.Maxime Dénès
2018-01-08Merge PR #6425: Cleanup universes in the kernelMaxime Dénès
2018-01-08Merge PR #6516: Add TIMING_SORT_BY and --sort-by to timing scriptsMaxime Dénès
2018-01-08Merge PR #6530: Ignore generated test-suite/output/MExtraction.outMaxime Dénès
2018-01-08Merge PR #6517: Trim more trailing whitespace in coq-makefile timing testMaxime Dénès
2018-01-08Merge PR #6527: Update backport script for more control.Maxime Dénès
2018-01-08Merge PR #6526: Fixing various typos in the Credits chapter.Maxime Dénès
2018-01-08github-check-prs.py: print PR URLs when needed.Gaëtan Gilbert
2018-01-08github-check-prs.py: Strip spaces from token from command lineGaëtan Gilbert
2018-01-08github-check-prs.py: command line option to get token from a fileGaëtan Gilbert
2018-01-08Merge PR #6510: Document between and exists_between types.Maxime Dénès
2018-01-08Document between and exists_between types.Ismail
2018-01-08Merge PR #6518: Fix build of micromega & nsatz with OCaml 4.06Maxime Dénès