aboutsummaryrefslogtreecommitdiff
path: root/ide/utils/uoptions.mli
AgeCommit message (Expand)Author
2009-03-27Remove unused mli filesletouzey
2004-04-30Achèvement du passage des emprunts à cameleon de Maxence Guesdon de la vers...herbelin
2003-03-03coqide: preferences support and optimizationsmonate