aboutsummaryrefslogtreecommitdiff
path: root/vernac/comPrimitive.ml
AgeCommit message (Collapse)Author
2020-03-18Update headers in the whole code base.Théo Zimmermann
Add headers to a few files which were missing them.
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
Primitives don't have anything to do with assumptions.