aboutsummaryrefslogtreecommitdiff
path: root/src/tac2env.ml
AgeCommit message (Expand)Author
2017-09-04Closures now wear the constant they originated from.Pierre-Marie Pédrot
2017-09-03Moving generic arguments to Tac2quote.Pierre-Marie Pédrot
2017-09-03Allowing ML objects to return mere tactic expressions.Pierre-Marie Pédrot
2017-09-03Allowing complex types in ML objects.Pierre-Marie Pédrot
2017-08-29Fixing printing of tactic expressions.Pierre-Marie Pédrot
2017-08-29Rolling our own generic arguments.Pierre-Marie Pédrot
2017-08-29Removing dead code for handling of array litterals.Pierre-Marie Pédrot
2017-08-27Introducing rebindable toplevel definitions.Pierre-Marie Pédrot
2017-08-24Introducing a quotation for global references.Pierre-Marie Pédrot
2017-08-07Introducing grammar-free tactic notations.Pierre-Marie Pédrot
2017-07-30Exporting more internals from Coq implementation.Pierre-Marie Pédrot
2017-07-27Adding necessary primitives to do pattern-matching over constr.Pierre-Marie Pédrot
2017-07-26Ensuring that inductive constructors are always capitalized.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-04-21 21:11:05 +0000