aboutsummaryrefslogtreecommitdiff
path: root/printing/ppvernac.ml
AgeCommit message (Expand)Author
2012-10-29Fixed #2926:ppedrot
2012-10-26Change Hint Resolve, Immediate to take a global reference as argumentmsozeau
2012-10-16Split Tacinterp in 3 files : Tacsubst, Tacintern and Tacinterpletouzey
2012-10-06still some more dead code removalletouzey
2012-10-04Moved Compat to parsing. This permits to break the dependency of theppedrot
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