pow notation breaks after importing Limit and defining \infty notation

wtf.v

Require Import 
  additional_operations.

Check (1^3).
(* 1 ^ 3
     : nat *)

Require Import Streams.

Notation "∅ x" := (Stream x) (at level 38).

Check (1^3).
(* 1 ^ 3 : nat *)

Require Import Limit.
(*
<W> Grammar extension: in [constr:pattern], some rule has been masked
<W> Grammar extension: in [constr:operconstr], some rule has been masked
<W> Grammar extension: in [constr:pattern], some rule has been masked
Ambiguous paths:
[Qpossec.integral_Qpos; Qpossec.QposAsQ] : BinPos.positive >-> QArith_base.Q
Ambiguous paths:
[QnonNeg.from_Qpos; QnonNeg.to_Q] : Qpossec.Qpos >-> QArith_base.Q
[QnonNeg.from_nat; QnonNeg.to_Q] : nat >-> QArith_base.Q
[Qpossec.integral_Qpos; QnonNeg.from_Qpos; QnonNeg.to_Q] : BinPos.positive >-> QArith_base.Q
Ambiguous paths:
[QnonNeg.from_Qpos; QnnInf.Finite] : Qpossec.Qpos >-> QnnInf.T
[Qpossec.integral_Qpos; QnonNeg.from_Qpos; QnnInf.Finite] : BinPos.positive >-> QnnInf.T
Ambiguous paths:
[universal_algebra.et_laws] : universal_algebra.EquationalTheory >-> Funclass
*)

Check (1^3). (* 1^3 : Q *)

(** shorthand (Agda) notation for streams. *)
Notation "∞ x" := (Stream x) (at level 37).

Check (1^3).
(* pow 1 3 : Q *)