fixes #1308

math-comp · Sep 6, 2024 · f34ace8 · f34ace8
1 parent 3d15d3e
commit f34ace8
Showing 1 changed file with 0 additions and 4 deletions.
diff --git a/theories/numfun.v b/theories/numfun.v
@@ -469,8 +469,6 @@ HB.end.
 Section Tietze.
 Context {X : topologicalType} {R : realType}.
 
-Local Notation "3" := 3%:R : ring_scope.
-
 Hypothesis normalX : normal_space X.
 
 Lemma urysohn_ext_itv A B x y :
@@ -495,8 +493,6 @@ Qed.
 Context (A : set X).
 Hypothesis clA : closed A.
 
-Local Notation "3" := 3%:R.
-
 Local Lemma tietze_step' (f : X -> R) (M : R) :
   0 < M -> {within A, continuous f} ->
   (forall x, A x -> `|f x| <= M) ->