aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2017-08-24Adding notation for the remaining reduction functions.Pierre-Marie Pédrot
2017-08-24Fix typing of reference quotations.Pierre-Marie Pédrot
2017-08-24Adding a scope for reduction flags.Pierre-Marie Pédrot
2017-08-24Introducing a quotation for global references.Pierre-Marie Pédrot
2017-08-24Use references in reduction tactics.Pierre-Marie Pédrot
2017-08-18More precise type for quotation entries.Pierre-Marie Pédrot
2017-08-18Removing dead code.Pierre-Marie Pédrot
2017-08-18Laxer dependencies between file and link reordering.Pierre-Marie Pédrot
2017-08-18Notations for a few reduction functions.Pierre-Marie Pédrot
2017-08-18Exporting scopes for occurrences.Pierre-Marie Pédrot
2017-08-18Trying to enhance the printing of tactic expressions.Pierre-Marie Pédrot
2017-08-11Introducing a syntax for goal dispatch.Pierre-Marie Pédrot
2017-08-08Another batch of primitive operations.Pierre-Marie Pédrot
2017-08-08Code simplification in quotations.Pierre-Marie Pédrot
2017-08-07Defining several aliases for built-in tactics.Pierre-Marie Pédrot
2017-08-07Defining abbreviations for tactics that can parse as atoms.Pierre-Marie Pédrot
2017-08-07Fix location of not-unit warning.Pierre-Marie Pédrot
2017-08-07Fix parsing of parenthesized expressions.Pierre-Marie Pédrot
2017-08-07Defining a few base tacticals.Pierre-Marie Pédrot
2017-08-07Introducing grammar-free tactic notations.Pierre-Marie Pédrot
2017-08-05Exporting more reduction functions.Pierre-Marie Pédrot
2017-08-05More notations for basic tactics.Pierre-Marie Pédrot
2017-08-05Exporting the rewrite tactic.Pierre-Marie Pédrot
2017-08-04Introducing quotations for the rewrite tactic.Pierre-Marie Pédrot
2017-08-04Adding locations to quotation types.Pierre-Marie Pédrot
2017-08-04More precise type for quoted structures.Pierre-Marie Pédrot
2017-08-04Adding the induction and destruct tactics.Pierre-Marie Pédrot
2017-08-04Introducing notations for destruct and induction arguments.Pierre-Marie Pédrot
2017-08-02Inserting enter functions in Ltac1 bindings.Pierre-Marie Pédrot
2017-08-02Tentatively implementing apply.Pierre-Marie Pédrot
2017-08-02Typo in documentation.Pierre-Marie Pédrot
2017-08-02Expanding documentation.Pierre-Marie Pédrot
2017-08-02Fix compilation of horrible Ltac2 example.Pierre-Marie Pédrot
2017-08-02Properly implementing the notation to easily access hypotheses.Pierre-Marie Pédrot
2017-08-02Code factorization in elim notation.Pierre-Marie Pédrot
2017-08-02Merging the e/- variants of primitive tactics.Pierre-Marie Pédrot
2017-08-02Adding new notations.Pierre-Marie Pédrot
2017-08-02Extending the set of tactic scopes.Pierre-Marie Pédrot
2017-08-02More examplesPierre-Marie Pédrot
2017-08-02Properly classifying Ltac2 notations.Pierre-Marie Pédrot
2017-08-02Fixing parsing of match branches.Pierre-Marie Pédrot
2017-08-02Removing deprecated stuff.Pierre-Marie Pédrot
2017-08-02Adding a few standard notations for Ltac1 tactics.Pierre-Marie Pédrot
2017-08-02Bindings use open constr quotations.Pierre-Marie Pédrot
2017-08-02Adding the open_constr scopePierre-Marie Pédrot
2017-08-02Better test Makefile.Pierre-Marie Pédrot
2017-08-02Tentatively fixing a few parsing issues.Pierre-Marie Pédrot
2017-08-02Fixup reification of egeneralize.Pierre-Marie Pédrot
2017-08-01More primitive tactics.Pierre-Marie Pédrot
2017-08-01Expanding unification variables in typechecking error messages.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-31 12:46:12 +0000