aboutsummaryrefslogtreecommitdiff
path: root/vernac/comPrimitive.ml
AgeCommit message (Expand)Author
2019-10-05Move do_primitive from comassumption to its own module.Gaƫtan Gilbert