aboutsummaryrefslogtreecommitdiff
path: root/doc
AgeCommit message (Expand)Author
2018-10-23Merge remote-tracking branch 'origin/pr/70'Pierre-Marie Pédrot
2018-08-07fix three small typosLangston Barrett
2018-08-07doc/ltac2.md: add table of contentsLangston Barrett
2018-03-13Fix another typo in the documentation's grammar for open variantsArmael
2018-03-13Fix a typoArmael
2017-10-27Adding documentationPierre-Marie Pédrot
2017-10-27Adding a command to evaluate Ltac2 expressions.Pierre-Marie Pédrot
2017-09-04Implementing the non-strict mode.Pierre-Marie Pédrot
2017-09-04Quick-and-dirty backtrace mechanism for the interpreter.Pierre-Marie Pédrot
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