aboutsummaryrefslogtreecommitdiff
path: root/vernac/comInductive.ml
AgeCommit message (Expand)Author
2018-02-22[ast] Improve precision of Ast location recognition in serialization.Emilio Jesus Gallego Arias
2018-02-11Use specialized function for inductive subtyping inference.Gaëtan Gilbert
2018-02-10Inference of inductive subtyping does not need an evar map.Gaëtan Gilbert
2018-02-10Simplification: cumulativity information is variance information.Gaëtan Gilbert
2017-12-23[api] Also deprecate constructors of Decl_kinds.Emilio Jesus Gallego Arias
2017-12-17[vernac] Split `command.ml` into separate files.Emilio Jesus Gallego Arias