aboutsummaryrefslogtreecommitdiff
path: root/src/tac2intern.ml
AgeCommit message (Expand)Author
2017-08-24Removing dead code about arrays in the AST.Pierre-Marie Pédrot
2017-08-24Rely on quoting for lists instead of hardwiring it in the AST.Pierre-Marie Pédrot
2017-08-18Removing dead code.Pierre-Marie Pédrot
2017-08-07Fix location of not-unit warning.Pierre-Marie Pédrot
2017-08-07Introducing grammar-free tactic notations.Pierre-Marie Pédrot
2017-08-01Expanding unification variables in typechecking error messages.Pierre-Marie Pédrot
2017-07-28Allowing generic patterns in let-bindings.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-26Do not expand trivial patterns in functions.Pierre-Marie Pédrot
2017-07-26Ensuring that inductive constructors are always capitalized.Pierre-Marie Pédrot
2017-07-26Fix typo in error messagePierre-Marie Pédrot
2017-07-26Better typing errors for function types.Pierre-Marie Pédrot
2017-07-26Bugfix: wrong access to non-constant constructor compilation.Pierre-Marie Pédrot
2017-07-25Generalizing patterns in fun bindings.Pierre-Marie Pédrot
2017-07-24Correctly pushing variables for tuple patterns.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-27 05:05:09 +0000