aboutsummaryrefslogtreecommitdiff
path: root/src/tac2entries.mli
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-08-31Fix coq/ltac2#10: Antiquotation syntax breaks when backtracking across `Requi...Pierre-Marie Pédrot
2017-08-27Introducing rebindable toplevel definitions.Pierre-Marie Pédrot
2017-08-25Introducing a distinct bindings scope.Pierre-Marie Pédrot
2017-08-25Renaming the bindings scope into with_bindings.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-18More precise type for quotation entries.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-05Exporting the rewrite tactic.Pierre-Marie Pédrot
2017-08-04Introducing quotations for the rewrite tactic.Pierre-Marie Pédrot
2017-08-04Introducing notations for destruct and induction arguments.Pierre-Marie Pédrot
2017-08-02Tentatively implementing apply.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
2017-07-24Turning the ltac2 subfolder into a standalone plugin.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 03:28:51 +0000