-I . -R . mathcomp -arg -w -arg -projection-no-head-constant -arg -w -arg -redundant-canonical-projection -arg -w -arg -notation-overridden -arg -w -arg -duplicate-clear -arg -w -arg +non-primitive-record