aboutsummaryrefslogtreecommitdiff
path: root/pretyping/coercionops.ml
AgeCommit message (Expand)Author
2020-10-21Introduce an Ind module in the Names API.Pierre-Marie Pédrot
2020-05-10No more local reduction functions in Reductionops.Pierre-Marie Pédrot
2020-03-30Merge PR #11817: [cleanup] Remove unnecessary Map/Set module creationGaëtan Gilbert
2020-03-18Update headers in the whole code base.Théo Zimmermann
2020-03-13[cleanup] Remove unnecessary Map/Set module creationEmilio Jesus Gallego Arias
2019-12-22Rename files with Class in their name to make their role clearer.Pierre-Marie Pédrot