aboutsummaryrefslogtreecommitdiff
path: root/contrib/xml
ModeNameSize
-rw-r--r--README5663logplain
-rw-r--r--Xml.v1511logplain
-rw-r--r--cooking.ml3378logplain
-rw-r--r--cooking.mli1403logplain
-rw-r--r--ntrefiner.ml2671logplain
-rw-r--r--ntrefiner.mli397logplain
-rw-r--r--xml.ml3122logplain
-rw-r--r--xml.mli2210logplain
-rw-r--r--xmlcommand.ml29195logplain
-rw-r--r--xmlcommand.mli2642logplain
-rw-r--r--xmlentries.ml1927logplain