aboutsummaryrefslogtreecommitdiff
path: root/engine/universes.ml
AgeCommit message (Expand)Author
2017-06-02Drop '.' from CErrors.anomaly, insert it in argsJason Gross
2017-04-27Remove unused [open] statementsGaetan Gilbert
2017-04-27Add [_] prefix to unused values which maybe should be keptGaetan Gilbert
2017-03-24Merge branch 'trunk' into pr379Maxime Dénès
2017-03-21[pp] Remove uses of expensive string_of_ppcmds.Emilio Jesus Gallego Arias
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-31Code factorization in Universes.Pierre-Marie Pédrot
2016-10-30Moving Universes to the engine/ folder.Pierre-Marie Pédrot