index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
printing
/
ppvernac.ml
Age
Commit message (
Expand
)
Author
2012-10-29
Fixed #2926:
ppedrot
2012-10-26
Change Hint Resolve, Immediate to take a global reference as argument
msozeau
2012-10-16
Split Tacinterp in 3 files : Tacsubst, Tacintern and Tacinterp
letouzey
2012-10-06
still some more dead code removal
letouzey
2012-10-04
Moved Compat to parsing. This permits to break the dependency of the
ppedrot
2012-09-14
This patch removes unused "open" (automatically generated from
regisgia
2012-08-11
Added support for option Local (at module level) in Tactic Notation.
herbelin
2012-08-08
Updating headers.
herbelin
2012-07-09
Avoid a warning about unprintable new command Print Namespace
letouzey
2012-07-05
Notation: a new annotation "compat 8.x" extending "only parsing"
letouzey
2012-07-04
Fixes a bug in Ppvernac which had braces and bullets printed with an ending
aspiwack
2012-06-22
Added an indirection with respect to Loc in Compat. As many [open Compat]
ppedrot
2012-06-19
Fixing some inconsistencies of constr printer wrt constr parser
herbelin
2012-05-29
place all pretty-printing files in new dir printing/
letouzey
[prev]