Stream: math-comp users

Topic: Exporting of notations in ssrfun.v


view this post on Zulip Karl Palmskog (Dec 07 2020 at 13:09):

I recently fixed an issue where ssreflect notations were clashing with custom ones (https://github.com/coq-community/autosubst/pull/20). While doing this, I noticed that ssreflect/ssrfun.v pretty much only does two things: (1) export the ssrfun from Coq, and (2) export ssrnotations. (1) completely makes sense, but what's the rationale for (2)? Shouldn't people have the choice to use ssrfun while avoiding notations? None of the other files in ssreflect exports notations, so why does ssrfun.v?

https://github.com/math-comp/math-comp/blob/master/mathcomp/ssreflect/ssrfun.v#L3

view this post on Zulip Karl Palmskog (Dec 07 2020 at 13:26):

to avoid the notations, I get this awkward incantation:

From mathcomp Require Import ssreflect ssrbool.
From Coq Require Import ssrfun.

instead of

From mathcomp Require Import ssreflect ssrbool ssrfun.

view this post on Zulip Karl Palmskog (Dec 07 2020 at 14:57):

@Dan Frumin this is the issue we discussed in the Autosubst PR


Last updated: Feb 02 2023 at 15:04 UTC