aboutsummaryrefslogtreecommitdiff
path: root/plugins/xml/doubleTypeInference.ml
AgeCommit message (Expand)Author
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2013-10-14Remove some uses of local modules (some were unused, some were costly).xclerc
2013-04-29Splitting Term into five unrelated interfaces:ppedrot
2013-02-19Dir_path --> DirPathletouzey
2013-02-18Minor code cleanups, especially take advantage of Dir_path.is_emptyletouzey
2012-12-18Modulification of Labelppedrot
2012-12-14Modulification of dir_pathppedrot
2012-10-02Remove some more "open" and dead code thanks to OCaml4 warningsletouzey
2012-06-01Cleaning Pp.ppnl useppedrot
2012-05-29Glob_term now mli-only, operations now in Glob_opsletouzey
2012-03-02Noise for nothingpboutill
2010-12-23Rename rawterm.ml into glob_term.mlglondu
2010-07-24Updated all headers for 8.3 and trunkherbelin
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2009-03-20Directory 'contrib' renamed into 'plugins', to end confusion with archive of ...letouzey