aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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-04-05 03:03:08 +0000