From 22f6a95cc4966254624372ed0f8ae517389ddf82 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 21 Apr 2015 19:55:59 -0700 Subject: [PATCH] feat(frontends/lean): local notation override global one --- hott/algebra/precategory/basic.hlean | 2 +- src/frontends/lean/notation_cmd.cpp | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) 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);