fix

math-comp · Jul 6, 2023 · 3448528 · 3448528
1 parent 80e97b3
commit 3448528
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/theories/exp.v b/theories/exp.v
@@ -852,7 +852,7 @@ Proof. by rewrite -!poweRrM mulrC. Qed.
 
 Definition poweRD_def x r s := ((r + s == 0)%R ==>
   ((x != 0) && ((x \isn't a fin_num) ==> (r == 0%R) && (s == 0%R)))).
-Notation "x `^?( r +? s )" := (poweRD_def x r s) : ereal_scope.
+Notation "x '`^?' ( r +? s )" := (poweRD_def x r s) : ereal_scope.
 
 Lemma poweRD_defE x r s :
   x `^?(r +? s) = ((r + s == 0)%R ==>