aboutsummaryrefslogtreecommitdiff
path: root/vernac/declaremods.mli
AgeCommit message (Expand)Author
2020-11-09Remove the native symbol registering from the safe environment.Pierre-Marie Pédrot
2020-06-30[declaremods] Remove abstraction of imperative module operationsEmilio Jesus Gallego Arias
2020-04-13pass filters aroundGaëtan Gilbert
2020-03-18Update headers in the whole code base.Théo Zimmermann
2019-10-31[prettyp] remove `mod_ops` and `indirect_accessor` parametersGaë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