max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore(frontends/lean/elaborator): rename attribute [elab_default] ==> [elab_simple]

Browse source
This commit is contained in:
Leonardo de Moura 2016-09-14 09:42:30 -07:00
parent 83cc67ba67
commit b426119e83
1 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/frontends/lean/elaborator.cpp
View file

@ -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");
}