GitLab

When using Export, even if imports are ordered consistently, there is sometimes no way to obtain consistent shadowing:

From stdpp Require base.
Module or.
  Export stdpp.base.
  Definition or_comm := 10.
End or.
Module and.
  Export stdpp.base.
  Definition and_comm := 11.
End and.
Module A.
  Import or and.
  Locate or_comm.
  (*
                    
  Constant stdpp.base.or_comm
  Constant Coq.Init.Logic.or_comm (shorter name to refer to it in current context is Logic.or_comm)
  Constant Top.or.or_comm (shorter name to refer to it in current context is or.or_comm)
  *)
  Locate and_comm.
  (*
                    
  Constant Top.and.and_comm
  Constant Coq.Init.Logic.and_comm (shorter name to refer to it in current context is Logic.and_comm)
  Constant stdpp.base.and_comm (shorter name to refer to it in current context is base.and_comm)
  *)
End A. 

Here, importing and overwrites or_comm because of the stdpp.base export.

I think the only way to avoid this is to avoid Exporting except when the re-exported symbols are conceptually really part of that library (such as stdpp.prelude).