itauto pulls in classic when reals are loaded

We recently saw the classic axiom popping up in our dependencies, even though there was no obvious classical reasoning going on. It seems like one of the culprits is itauto when it has Reals loaded somewhere (not necessarily imported):

From Cdcl Require Import Itauto.
From Coq Require Reals.

Lemma option_map_tauto : forall validator index (A:validator -> index) v,
 option_map A (Some v) = Some (A v).
Proof. intuition auto. Qed.

Lemma option_map_itauto : forall validator index (A:validator -> index) v,
 option_map A (Some v) = Some (A v).
Proof. itauto auto. Qed.

Print Assumptions option_map_tauto. (* Closed under the global context *)
Print Assumptions option_map_itauto. (* Lots of axioms, including classic *)

Just because something is loaded, that shouldn't in itself lead to axiom changes, right? My intuition is that imports should normally be required.