aboutsummaryrefslogtreecommitdiff
path: root/doc
AgeCommit message (Expand)Author
2017-08-28typosgallais
2017-08-27Introducing rebindable toplevel definitions.Pierre-Marie Pédrot
2017-08-26Allowing calls to Ltac2 inside Ltac1.Pierre-Marie Pédrot
2017-08-26TyposHugo Herbelin
2017-08-26Allowing to insert calls to Ltac1 references in Ltac2.Pierre-Marie Pédrot
2017-08-25Do not return STRING scopes in the tuple produced by "seq" scopes.Pierre-Marie Pédrot
2017-08-24Documentation about the transition from Ltac1.Pierre-Marie Pédrot
2017-08-24Introducing a quotation for global references.Pierre-Marie Pédrot
2017-08-07Introducing grammar-free tactic notations.Pierre-Marie Pédrot
2017-08-02Typo in documentation.Pierre-Marie Pédrot
2017-08-02Expanding documentation.Pierre-Marie Pédrot
2017-08-02Properly implementing the notation to easily access hypotheses.Pierre-Marie Pédrot
2017-08-02Extending the set of tactic scopes.Pierre-Marie Pédrot
2017-08-01Fix documentation.Pierre-Marie Pédrot
2017-08-01More in documentation.Pierre-Marie Pédrot
2017-08-01Fixup docPierre-Marie Pédrot
2017-08-01Fixup docPierre-Marie Pédrot
2017-08-01Adding documentation from the CEP.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-13 00:00:12 +0000