aboutsummaryrefslogtreecommitdiff
path: root/src/tac2print.ml
AgeCommit message (Expand)Author
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