aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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-07[api] Remove 8.7 ML-deprecated functions.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-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
2017-11-05Cosmetic changes in evar_map printer.Hugo Herbelin
2017-11-05Preventively protect locally against failures of evar_map printer.Hugo Herbelin
2017-11-05Fixing a cause of failure of evar_map printer in debugger.Hugo Herbelin
2017-11-04[api] Deprecate all legacy uses of Name.Id in core.Emilio Jesus Gallego Arias
2017-11-04Finish removing Show Goal uidGaëtan Gilbert
2017-11-03Merge PR #6060: Improve error message and fix #6055 (spelling mistake).Maxime Dénès
2017-11-03Merge PR #6051: Fix FIXME: use OCaml 4.02 generative functors when available.Maxime Dénès
2017-11-03Merge PR #6047: A generic printer for ltac valuesMaxime Dénès
2017-11-03Merge PR #6037: Fixing #5401 (printing of patterns with bound anonymous varia...Maxime Dénès
2017-11-03Merge PR #6036: [toplevel] Export the last document seen after `Drop`.Maxime Dénès
2017-11-03Merge PR #6031: [ci] Switch back to upstream version of Math-Classes and Corn.Maxime Dénès
2017-11-03Merge PR #6027: Mention the migration from Bugzilla to GitHub issues in dev/d...Maxime Dénès
2017-11-03Merge PR #6024: Update of Coq version historyMaxime Dénès
2017-11-03Merge PR #6021: Fixing #2881 ("change with" failing in an Ltac definition).Maxime Dénès
2017-11-03Merge PR #5999: An attempt to fix issue #5771 (error color hidden by warning ...Maxime Dénès
2017-11-03Merge PR #924: Fixing part of #5669: unification heuristics sensitive to alph...Maxime Dénès
2017-11-02Update tactics.mlFarzon Lotfi
2017-11-02Ltac Debug: exporting env and sigma when needed so that term can be printed.Hugo Herbelin
2017-11-02Binding ltac printing functions to the system of generic printing.Hugo Herbelin
2017-11-02Setting a system to register printers for Ltac values.Hugo Herbelin
2017-11-02Exporting ValTMap for use in Genintern.Hugo Herbelin
2017-11-02Using a specific function to register vernac printers.Hugo Herbelin
2017-11-02Exporting the level-parametric printer of constr and its variants.Hugo Herbelin
2017-11-02Do not identify a pre_ident as a string Ltac value.Hugo Herbelin
2017-11-02Removing a redundancy in naming types (Ppconstr.precedence = tolerability).Hugo Herbelin
2017-11-02Naming the type of Dyn.Map for future reuse.Hugo Herbelin
2017-11-02Exporting a few more printing functions.Hugo Herbelin
2017-11-02Improving checks about the list separator in tactic notations.Hugo Herbelin
2017-11-01Fix FIXME: use OCaml 4.02 generative functors when available.Gaëtan Gilbert
2017-11-01provide "loc : Loc.t" binding within "VERNAC COMMAND EXTEND" rulesMatej Košík
2017-10-30Fixing #2881 ("change with" failing in an Ltac definition).Hugo Herbelin
2017-10-30[ci] Switch VST back to upstream.Théo Zimmermann
2017-10-28Fixing #5401 (printing of patterns with bound anonymous variables).Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-19 07:24:20 +0000