aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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-26Adding a file for testing typing.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 typo.Pierre-Marie Pédrot
2017-07-24Removing a spurious file.Pierre-Marie Pédrot
2017-07-24Filling the README.Pierre-Marie Pédrot
2017-07-24Adding quick-n-dirty tests.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
2017-05-19Adding new tactic notation scopes.Pierre-Marie Pédrot
2017-05-19Extending the Coq API in Ltac2.Pierre-Marie Pédrot
2017-05-19Removing dead code in Ltac2, and cleaning up a bit.Pierre-Marie Pédrot
2017-05-19Introducing tactic notations in Ltac2.Pierre-Marie Pédrot
2017-05-19Allow raw terms to contain references to absolute definitions.Pierre-Marie Pédrot
2017-05-19Stdlib functions now return Ltac2 exceptions.Pierre-Marie Pédrot
2017-05-19Proper handling of exception definition in Ltac2.Pierre-Marie Pédrot
2017-05-19Merging GTacTuple and GTacCst nodes.Pierre-Marie Pédrot
2017-05-19Towards a proper printing of Ltac2 data structures.Pierre-Marie Pédrot
2017-05-19Allow the embedding of Ltac2 terms in constrs via the ltac2:(...) syntax.Pierre-Marie Pédrot
2017-05-19Fixing a precedence issue in type parameters.Pierre-Marie Pédrot
2017-05-19Proper handling of record types.Pierre-Marie Pédrot
2017-05-19Allowing to include Coq terms in Ltac2 using the constr:(...) syntax.Pierre-Marie Pédrot
2017-05-19Embedding generic arguments in Ltac2 AST.Pierre-Marie Pédrot
2017-05-19Introduction of the Ltac2 plugin.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-21 03:45:58 +0000