Karl Palmskog (Dec 07 2020 at 13:09): 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
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.
@Dan Frumin this is the issue we discussed in the Autosubst PR
Last updated: Feb 02 2023 at 15:04 UTC