aboutsummaryrefslogtreecommitdiff
path: root/printing/ppvernac.ml
AgeCommit message (Expand)Author
2012-09-14This patch removes unused "open" (automatically generated fromregisgia
2012-08-11Added support for option Local (at module level) in Tactic Notation.herbelin
2012-08-08Updating headers.herbelin
2012-07-09Avoid a warning about unprintable new command Print Namespaceletouzey
2012-07-05Notation: a new annotation "compat 8.x" extending "only parsing"letouzey
2012-07-04Fixes a bug in Ppvernac which had braces and bullets printed with an endingaspiwack
2012-06-22Added an indirection with respect to Loc in Compat. As many [open Compat]ppedrot
2012-06-19Fixing some inconsistencies of constr printer wrt constr parserherbelin
2012-05-29place all pretty-printing files in new dir printing/letouzey