aboutsummaryrefslogtreecommitdiff
path: root/src/tac2print.ml
AgeCommit message (Expand)Author
2018-03-27Fix printing of toplevel record values.Pierre-Marie Pédrot
2017-10-27Better printers for toplevel values.Pierre-Marie Pédrot
2017-10-07Remove unused warnings.Pierre-Marie Pédrot
2017-10-07Fix coq/ltac2#30: Compilation broken since -safe-string PR got merged.Pierre-Marie Pédrot
2017-10-01Abstracting away the implementation of value representations.Pierre-Marie Pédrot
2017-09-30Abstracting away the primitive functions on valexpr datatype.Pierre-Marie Pédrot
2017-09-14Moving valexpr definition to Tac2ffi.Pierre-Marie Pédrot
2017-09-13Better printing for list literals.Pierre-Marie Pédrot
2017-09-08Fix coq/ltac2#27: ... is not a particularly helpful printing of an error mess...Pierre-Marie Pédrot
2017-09-08Fix coq/ltac2#22: Argument to Tactic_failure should be printed.Pierre-Marie Pédrot
2017-09-02Fix coq/ltac2#12: Error should name which match cases are unhandled.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-18Trying to enhance the printing of tactic expressions.Pierre-Marie Pédrot
2017-08-07Introducing grammar-free tactic notations.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-26Ensuring that inductive constructors are always capitalized.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-25 13:11:11 +0000