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
to avoid the notations, I get this awkward incantation:
From mathcomp Require Import ssreflect ssrbool. From Coq Require Import ssrfun.
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