aboutsummaryrefslogtreecommitdiff
path: root/vernac/declaremods.ml
AgeCommit message (Expand)Author
2019-10-14Remove obj_sec field of Nametab.obj_prefix record.Gaƫtan Gilbert
2019-09-18[declaremods] Remove abstraction layer over module interpretation.Emilio Jesus Gallego Arias
2019-09-18[library] Move `Declaremods` to `vernac/`Emilio Jesus Gallego Arias