D'autant plus qu'à force, je me suis habitué aux opérateurs différents suivant les types, et que je râle au contraire quand dans un autre langage je ne sais pas différencier syntaxiquement si c'est une opération sur des floats ou des ints.

Le mieux pour améliorer ça pour moi n'est vraiment pas la surcharge, mais plutôt une syntaxe pour préciser l'espace de nommage à la coq.
Exemple Coq car je suppose que personne ne connaît :

  (2+3)%Z   (* les nombres et les opérations sont ceux de Z *)
  (2+3)%nat   (* idem pour nat *)

En caml on pourrait faire

  (2+3)%int
  (2+3)%float
  (2+3)%Byte.t

etc.