aboutsummaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Expand)Author
2017-08-01Binding more primitive tactics.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-27Fix expansion of toplevel let-rec after the constructor / constant split.Pierre-Marie Pédrot
2017-07-27Adding necessary primitives to do pattern-matching over constr.Pierre-Marie Pédrot
2017-07-26Tentative fix of parsing of product types.Pierre-Marie Pédrot
2017-07-26Dedicated module for ident type.Pierre-Marie Pédrot
2017-07-26Do not expand trivial patterns in functions.Pierre-Marie Pédrot
2017-07-26Ensuring that inductive constructors are always capitalized.Pierre-Marie Pédrot
2017-07-26Fix typo in error messagePierre-Marie Pédrot
2017-07-26Better typing errors for function types.Pierre-Marie Pédrot
2017-07-26Lightweight quotation syntax for terms and idents.Pierre-Marie Pédrot
2017-07-26Properly handling toplevel recursive definitions.Pierre-Marie Pédrot
2017-07-26Exporting some basic tactics from Ltac1.Pierre-Marie Pédrot
2017-07-26Bugfix: wrong access to non-constant constructor compilation.Pierre-Marie Pédrot
2017-07-25Generalizing patterns in fun bindings.Pierre-Marie Pédrot
2017-07-24Adding a few primitive functions.Pierre-Marie Pédrot
2017-07-24Correctly pushing variables for tuple patterns.Pierre-Marie Pédrot
2017-07-24Properly handle parsing of list patterns.Pierre-Marie Pédrot
2017-07-24Fix library hardwired prefix.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-02-16 16:17:13 +0000