diff --git a/hott/algebra/precategory/basic.hlean b/hott/algebra/precategory/basic.hlean
index e67072fa2..1e67ebad0 100644
--- a/hott/algebra/precategory/basic.hlean
+++ b/hott/algebra/precategory/basic.hlean
@@ -66,7 +66,7 @@ namespace category
     !is_trunc_eq
 
   end basic_lemmas
-  context squares
+  section squares
     parameters {ob : Type} [C : precategory ob]
     local infixl `⟶`:25 := @precategory.hom ob C
     local infixr `∘`    := @precategory.comp ob C _ _ _
diff --git a/src/frontends/lean/notation_cmd.cpp b/src/frontends/lean/notation_cmd.cpp
index 576207f45..7eca1a303 100644
--- a/src/frontends/lean/notation_cmd.cpp
+++ b/src/frontends/lean/notation_cmd.cpp
@@ -711,7 +711,7 @@ static environment dispatch_notation_cmd(parser & p, bool overload, bool reserve
 }
 
 environment local_notation_cmd(parser & p) {
-    bool overload   = !in_context(p.env());
+    bool overload   = false; // REMARK: local notation override global one
     bool reserve    = false;
     bool persistent = false;
     return dispatch_notation_cmd(p, overload, reserve, persistent);