aboutsummaryrefslogtreecommitdiff
path: root/ide/tags.ml
AgeCommit message (Expand)Author
2010-02-25Changes in lexing and tagging.vgross
2009-11-23Ergonomy and robustness fixvgross
2009-11-13new handling for lexical structures.vgross
2009-10-16note for later : when the tag table is shared, never, ever create twovgross
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2009-09-14tags refactoringvgross