aboutsummaryrefslogtreecommitdiff
path: root/src/tac2quote.ml
AgeCommit message (Expand)Author
2017-09-05Introducing quotations for move locations.Pierre-Marie Pédrot
2017-09-05Quotations for auto-related tactics.Pierre-Marie Pédrot
2017-09-04More notations for primitive tactics.Pierre-Marie Pédrot
2017-09-03Introducing a macro for constr matching.Pierre-Marie Pédrot
2017-09-03Moving generic arguments to Tac2quote.Pierre-Marie Pédrot
2017-09-03Uniform handling of locations in the various AST.Pierre-Marie Pédrot
2017-08-29Rolling our own generic arguments.Pierre-Marie Pédrot
2017-08-29Implementing Ltac2 antiquotations in constr syntax.Pierre-Marie Pédrot
2017-08-25Do not return STRING scopes in the tuple produced by "seq" scopes.Pierre-Marie Pédrot
2017-08-24Adding a notation scope for global references.Pierre-Marie Pédrot
2017-08-24Adding a scope for reduction flags.Pierre-Marie Pédrot
2017-08-18Laxer dependencies between file and link reordering.Pierre-Marie Pédrot
2017-08-18Exporting scopes for occurrences.Pierre-Marie Pédrot
2017-08-11Introducing a syntax for goal dispatch.Pierre-Marie Pédrot
2017-08-08Code simplification in quotations.Pierre-Marie Pédrot
2017-08-07Introducing grammar-free tactic notations.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-04Introducing notations for destruct and induction arguments.Pierre-Marie Pédrot
2017-08-02Properly implementing the notation to easily access hypotheses.Pierre-Marie Pédrot
2017-08-02Adding the open_constr scopePierre-Marie Pédrot
2017-08-01Don't reuse Coq AST for binding quotations.Pierre-Marie Pédrot
2017-08-01Introducing the all-mighty intro-patterns.Pierre-Marie Pédrot
2017-08-01Adding new scopes for standard Ltac structures.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-23 21:04:33 +0000