aboutsummaryrefslogtreecommitdiff
path: root/kernel/vars.ml
AgeCommit message (Expand)Author
2014-05-06Various fixes of universe polymorphism and projections when they're set.Matthieu Sozeau
2014-05-06- Fix comparison of universes.Matthieu Sozeau
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-03-05Remove some dead-code (thanks to ocaml warnings)Pierre Letouzey
2014-02-20Optimization in kernel/vars.ml: directly allocate a fixed-size block in thePierre-Marie Pédrot
2013-11-06Less partial applications in Vars, as well as better memory allocation.ppedrot
2013-10-23Optimizing Vars.replace_varsppedrot
2013-09-19Get rid of the uses of deprecated OCaml elements (still remaining compatible ...xclerc
2013-08-04Removing useless casts between arrays and lists.ppedrot
2013-04-29Splitting Term into five unrelated interfaces:ppedrot