From b426119e836cd1cf3efd975201112b3e99fb862e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 14 Sep 2016 09:42:30 -0700 Subject: [PATCH] chore(frontends/lean/elaborator): rename attribute `[elab_default]` ==> `[elab_simple]` --- src/frontends/lean/elaborator.cpp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index d2089c5cd9..d4dc428793 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -2349,14 +2349,14 @@ void initialize_elaborator() { register_system_attribute( elaborator_strategy_proxy_attribute( - "elab_default", + "elab_simple", "instructs elaborator that the arguments of the function application (f ...) " "should be elaborated from left to right, and without propagating information from the expected type " "to its arguments", elaborator_strategy::Default)); - register_incompatible("elab_default", "elab_with_expected_type"); - register_incompatible("elab_default", "elab_as_eliminator"); + register_incompatible("elab_simple", "elab_with_expected_type"); + register_incompatible("elab_simple", "elab_as_eliminator"); register_incompatible("elab_with_expected_type", "elab_as_eliminator"); }