aboutsummaryrefslogtreecommitdiff
path: root/vernac/comPrimitive.ml
AgeCommit message (Expand)Author
2020-03-18Update headers in the whole code base.Théo Zimmermann
2019-10-14Use kernel info from Global for Lib.sections_{depth,are_opened}Gaëtan Gilbert
2019-10-05Move do_primitive from comassumption to its own module.Gaëtan Gilbert