aboutsummaryrefslogtreecommitdiffhomepage
path: root/printing/pptactic.mli
Commit message (Collapse)AuthorAge
* Adding a nominal typing layer to Metasyntax in order to clarifyGravatar ppedrot2012-10-04
| | | | | | | | things up. Records are used instead of their equivalents as tuples. This is maybe syntactically heavier, but this is semantically equivalent and easier to understand. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15848 85f007b7-540e-0410-9357-904b9bb8a0f7
* Updating headers.Gravatar herbelin2012-08-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
* place all pretty-printing files in new dir printing/Gravatar letouzey2012-05-29
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15391 85f007b7-540e-0410-9357-904b9bb8a0f7