aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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-01[API] Some reordering following latest separation commits.Emilio Jesus Gallego Arias
2017-11-01[general] Move Tactypes to `interp`Emilio Jesus Gallego Arias
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
2017-10-28[toplevel] Export the last document seen after `Drop`.Emilio Jesus Gallego Arias
2017-10-27[ci] Switch back to upstream version of Math-Classes and Corn.Théo Zimmermann
2017-10-27Mention the migration from Bugzilla to GitHub issues in dev/doc/changes.Théo Zimmermann
2017-10-27Merge PR #6026: [ocaml] [travis] Add preliminary 4.06 CI testing.Maxime Dénès
2017-10-27Merge PR #6015: [general] Remove Econstr dependency from `intf`Maxime Dénès
2017-10-27Merge PR #6005: Fixes to documentation, addressed #4846, #5413 and #5631Maxime Dénès
2017-10-27Merge PR #5979: Fix #5763: Strictly positive example is out of order.Maxime Dénès
2017-10-27Merge PR #1113: Adding 3 Arith/QArith lemmas that I found usefulMaxime Dénès
2017-10-27Merge PR #677: Trunk+abstracting injection flagsMaxime Dénès
2017-10-27Chaining two tactics in a proofRaphaël Monat
2017-10-27[ocaml] [travis] Add preliminary 4.06 CI testing.Emilio Jesus Gallego Arias
2017-10-26Passing around the flag for injection so that tactics calling inj atHugo Herbelin
2017-10-26Delay use of flag "Discriminate Introduction" from interp to execution time.Hugo Herbelin
2017-10-26Updating version history wrt 8.7.Hugo Herbelin
2017-10-26Updating version history wrt 8.6.Hugo Herbelin
2017-10-26Updating version history wrt 8.5.Hugo Herbelin
2017-10-25Rename \Tree to \NatTreeJohannes Kloos
2017-10-25[general] Remove Econstr dependency from `intf`Emilio Jesus Gallego Arias
2017-10-25Moving from `is_true` to `= true`Raphaël Monat
2017-10-25Put linter at the top of the tests.Théo Zimmermann
2017-10-25Linter: check that files end with newlines.Gaëtan Gilbert
2017-10-25Put newlines at the end of files.Gaëtan Gilbert
2017-10-25Add linter.Gaëtan Gilbert
2017-10-25Merge PR #6009: Master+misc typos dead code etcMaxime Dénès
2017-10-25Merge PR #6003: Point HoTT back at master, which now supports Coq masterMaxime Dénès
2017-10-25Merge PR #6002: Move bug files to match their new GitHub ID (fixes #6001).Maxime Dénès
2017-10-25Merge PR #5995: Revert "Add debug output to brew update."Maxime Dénès
2017-10-25Merge PR #5993: Switch testing branch back to CompCert upstream.Maxime Dénès
2017-10-25Merge PR #5980: Add AppVeyor badge next to Travis badge.Maxime Dénès
2017-10-25Merge PR #5971: [travis] Add flambda testing.Maxime Dénès
2017-10-24Fix #5763: Strictly positive example is out of order.jkloos
2017-10-24Removing dead code which raised questions.Hugo Herbelin
2017-10-24Typo in comment in tactic_matching.ml.Hugo Herbelin
2017-10-24An occurrence of set_id which behaves as the identity.Hugo Herbelin
2017-10-24A missing newline after a comment.Hugo Herbelin
2017-10-24Fix #4846Johannes Kloos
2017-10-24Fix #5413: [unfold ... in] not documentedJohannes Kloos
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-28 20:47:50 +0000