aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2017-08-01Don't reuse Coq AST for binding quotations.Pierre-Marie Pédrot
2017-08-01Fix parsing of fresh ident antiquotations.Pierre-Marie Pédrot
2017-08-01Introducing the all-mighty intro-patterns.Pierre-Marie Pédrot
2017-08-01Fix documentation.Pierre-Marie Pédrot
2017-08-01Binding more primitive tactics.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
2017-08-01Do not thunk notations preemptively.Pierre-Marie Pédrot
2017-08-01Adding new scopes for standard Ltac structures.Pierre-Marie Pédrot
2017-07-30Exporting more internals from Coq implementation.Pierre-Marie Pédrot
2017-07-28Parameterizing FFI functions for parameterized types.Pierre-Marie Pédrot
2017-07-28Moving the Ltac2 FFI to a separate file.Pierre-Marie Pédrot
2017-07-28Allowing generic patterns in let-bindings.Pierre-Marie Pédrot
2017-07-27Factorizing code for constructors and tuples.Pierre-Marie Pédrot
2017-07-27Cleaning up code in internalization.Pierre-Marie Pédrot
2017-07-27Using thunks in the horrible Ltac2 example.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-28 15:43:11 +0000