aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2017-11-15[dev] Remove deprecation warning from `base_include`Emilio Jesus Gallego Arias
2017-11-15Merge PR #6147: Change OCAMLRUNPARAM warning to mention OCaml 4.06Maxime Dénès
2017-11-15Merge PR #6146: coq_makefile: document COQ_SRC_SUBDIRSMaxime Dénès
2017-11-15Merge PR #6138: Clean up/less files at rootMaxime Dénès
2017-11-15Merge PR #6122: Remove dependency of test-suite on git (fix #5725).Maxime Dénès
2017-11-15Merge PR #6058: Remove redundant env argument to Reduction.ccnvMaxime Dénès
2017-11-15Merge PR #6045: [travis] [coq] Complete 4.06.0 support.Maxime Dénès
2017-11-13Move contributing files to .github/ sub-directory.Théo Zimmermann
2017-11-13Remove useless file README.doc.Théo Zimmermann
2017-11-13Change OCAMLRUNPARAM warning to mention OCaml 4.06Paul Steckler
2017-11-13[ci] [coq] Complete 4.06.0 support.Emilio Jesus Gallego Arias
2017-11-13coq_makefile: document COQ_SRC_SUBDIRSEnrico Tassi
2017-11-13Merge PR #6098: [api] Move structures deprecated in the API to the core.Maxime Dénès
2017-11-13Merge PR #6136: Update and simplify README.Maxime Dénès
2017-11-13Merge PR #6126: Fix ci-bignums.sh "missing ]" error.Maxime Dénès
2017-11-13Merge PR #6124: Adding a debugging printer for ident maps whose codomain type...Maxime Dénès
2017-11-13Merge PR #6117: Fix printing anomaly in convMaxime Dénès
2017-11-13Merge PR #6103: Hack to restore printing of glob_constr in debugger.Maxime Dénès
2017-11-13Merge PR #6088: Remove packaging scripts while waiting for a fix to #5998.Maxime Dénès
2017-11-13Merge PR #6071: [ci] Add Ltac2Maxime Dénès
2017-11-13Merge PR #6065: [api] Deprecate all legacy uses of Names in core.Maxime Dénès
2017-11-13Merge PR #6052: [general] Move Tactypes to `interp` + API reordering.Maxime Dénès
2017-11-13Merge PR #6000: Adding support for syntax "let _ := e in e'" in Ltac.Maxime Dénès
2017-11-10Update and simplify README.Théo Zimmermann
2017-11-09Fix ci-bignums.sh "missing ]" error.Gaëtan Gilbert
2017-11-08Adding a debugging printer for ident maps whose codomain type is unknown.Hugo Herbelin
2017-11-08Remove dependency of test-suite on git (fix #5725).Théo Zimmermann
2017-11-08Merge PR #6100: [api] Remove 8.7 ML-deprecated functions.Maxime Dénès
2017-11-08Merge PR #6096: Documentation: "tac1 || tac2" means "first [ progress tac1 | ...Maxime Dénès
2017-11-08Merge PR #6087: [feedback] Helper to print feedback messages in the console.Maxime Dénès
2017-11-08Merge PR #6086: [ci] Switch VST back to upstream.Maxime Dénès
2017-11-08Merge PR #922: New beta-iota compatibility refinementsMaxime Dénès
2017-11-08Fixing missing separator in an error message.Hugo Herbelin
2017-11-08Fixing an (apparently misplaced) spc in anomaly reporting message.Hugo Herbelin
2017-11-07Hack to restore printing of glob_constr in debugger.Hugo Herbelin
2017-11-07[api] Remove 8.7 ML-deprecated functions.Emilio Jesus Gallego Arias
2017-11-06[api] Move structures deprecated in the API to the core.Emilio Jesus Gallego Arias
2017-11-06[api] Deprecate all legacy uses of Names in core.Emilio Jesus Gallego Arias
2017-11-06Merge PR #6064: [api] Deprecate all legacy uses of Name.Id in core.Maxime Dénès
2017-11-06Documentation: "tac1 || tac2" means "first [ progress tac1 | tac2 ]",Samuel Gruetter
2017-11-06Remove packaging scripts while waiting for a fix to #5998.Théo Zimmermann
2017-11-06[feedback] Helper to print feedback messages in the console.Emilio Jesus Gallego Arias
2017-11-06Merge PR #6072: Protecting evar map printerMaxime Dénès
2017-11-06Merge PR #6074: Refining PR#924 (insensitivity of projection heuristics to al...Maxime Dénès
2017-11-06Merge PR #6085: Update .mailmap with a jkloos aliasMaxime Dénès
2017-11-06Merge PR #6063: Finish removing Show Goal uidMaxime Dénès
2017-11-06Merge PR #6049: provide "loc : Loc.t" binding within "VERNAC COMMAND EXTEND" ...Maxime Dénès
2017-11-06Merge PR #1139: Add a linter.Maxime Dénès
2017-11-05Update .mailmap with a jkloos aliasJason Gross
2017-11-05Refining PR#924 (insensitivity of projection heuristics to alphabet).Hugo Herbelin