aboutsummaryrefslogtreecommitdiff
path: root/engine/universes.mli
AgeCommit message (Expand)Author
2017-04-11Update various comments to use "template polymorphism"Gaetan Gilbert
2017-03-31Make the Constr.kind_of_term type parametric in sorts and universes.Pierre-Marie Pédrot
2017-02-14Evarconv API using EConstr.Pierre-Marie Pédrot
2016-10-31Stronger static invariant in equality upto universes.Pierre-Marie Pédrot
2016-10-30Moving Universes to the engine/ folder.Pierre-Marie Pédrot