aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2018-01-16Source basic overlay before user overlays.Gaëtan Gilbert
2018-01-16Cleanup shell expansions and quoting.Gaëtan Gilbert
2018-01-16Simplify logic and streamline lint-repository.shGaëtan Gilbert
2018-01-16Merge PR #6590: Fix the wrapper around ocamldebug.Maxime Dénès
2018-01-16Merge PR #6499: [vernac] Move the flags/attributes out of vernac_exprMaxime Dénès
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-10Fix ci-all targetGaëtan Gilbert
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-09[Backport script] Check .mli files are not changed.Théo Zimmermann
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