aboutsummaryrefslogtreecommitdiff
path: root/src/tac2env.ml
AgeCommit message (Expand)Author
2018-06-18Adapt to Coq's PR #7797 (removal of reference).Maxime Dénès
2017-11-04A possible fix after PR#6047 (a generic printer for ltac values).Hugo Herbelin
2017-10-07Remove unused warnings.Pierre-Marie Pédrot
2017-09-14Moving valexpr definition to Tac2ffi.Pierre-Marie Pédrot
2017-09-08Using a dedicated argument for tactic quotations.Pierre-Marie Pédrot
2017-09-06Using higher-order representation for closures.Pierre-Marie Pédrot
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-02-28 04:10:48 +0000