aboutsummaryrefslogtreecommitdiff
path: root/mathcomp/_CoqProject
AgeCommit message (Collapse)Author
2019-02-05we silence warnings that just pollute our logs (#275)Enrico
Namely: -projection-no-head-constant -redundant-canonical-projection -notation-overridden
2015-04-02Broken global MakefileCyril Cohen