aboutsummaryrefslogtreecommitdiff
path: root/ltac/pptactic.ml
AgeCommit message (Expand)Author
2017-02-17Ltac as a plugin.Pierre-Marie Pédrot
2017-02-14[misc] Remove unused binding.Emilio Jesus Gallego Arias
2016-12-07Merge branch 'v8.6'Pierre-Marie Pédrot
2016-11-30Merge branch 'v8.6'Pierre-Marie Pédrot
2016-10-08Merge branch 'v8.6'Pierre-Marie Pédrot
2016-09-23Merge branch 'v8.6'Pierre-Marie Pédrot
2016-09-21Merging Stdarg and Constrarg.Pierre-Marie Pédrot
2016-09-16Make the Coq codebase independent from Ltac-related code.Pierre-Marie Pédrot
2016-09-15Made Ppanotation Ltac-agnostic.Pierre-Marie Pédrot
2016-09-15Moving Ltac-specific generic arguments to their own file in the ltac/ folder.Pierre-Marie Pédrot
2016-09-15Moving Ltac printers to ltac/ folder.Pierre-Marie Pédrot