diff --git a/theories/hanson_elem_analysis.v b/theories/hanson_elem_analysis.v
index fc15dcb..58afd12 100644
--- a/theories/hanson_elem_analysis.v
+++ b/theories/hanson_elem_analysis.v
@@ -19,7 +19,7 @@ Section RationalPower.
 
 Definition exp_quo r p q := q.-root r%:C ^+ p.
 
-Arguments exp_quo r p%nat q%nat : simpl never.
+Arguments exp_quo r p%_nat q%_nat : simpl never.
 
 Lemma exp_quo_0 p q : exp_quo 0 p q = (p == 0%N)%:R.
 Proof. by rewrite /exp_quo /ratr mul0r rootC0 expr0n. Qed.