chore: update stage0

stage0/src/Lean/Elab.lean

@@ -5,7 +5,6 @@ Authors: Leonardo de Moura
 -/
 import Lean.Elab.Import
 import Lean.Elab.Exception
-import Lean.Elab.StrategyAttrs
 import Lean.Elab.Command
 import Lean.Elab.Term
 import Lean.Elab.App

stage0/src/Lean/Elab/StrategyAttrs.lean

@@ -1,30 +0,0 @@
-/-
-Copyright (c) 2019 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-import Lean.Attributes
-
-namespace Lean
-/-
-Elaborator strategies available in the Lean3 elaborator.
-We want to support a more general approach, but we need to provide
-the strategy selection attributes while we rely on the Lean3 elaborator.
--/
-inductive ElaboratorStrategy
-  | simple | withExpectedType | asEliminator
-
-instance : Inhabited ElaboratorStrategy :=
-  ⟨ElaboratorStrategy.withExpectedType⟩
-
-builtin_initialize elaboratorStrategyAttrs : EnumAttributes ElaboratorStrategy ←
-  registerEnumAttributes `elaboratorStrategy
-    [(`elabWithExpectedType, "instructs elaborator that the arguments of the function application (f ...) should be elaborated using information about the expected type", ElaboratorStrategy.withExpectedType),
-     (`elabSimple, "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", ElaboratorStrategy.simple),
-     (`elabAsEliminator, "instructs elaborator that the arguments of the function application (f ...) should be elaborated as f were an eliminator", ElaboratorStrategy.asEliminator)]
-
-@[export lean_get_elaborator_strategy]
-def getElaboratorStrategy (env : Environment) (n : Name) : Option ElaboratorStrategy :=
-  elaboratorStrategyAttrs.getValue env n
-
-end Lean

stage0/src/kernel/abstract.cpp

@@ -12,7 +12,7 @@ Author: Leonardo de Moura
 
 namespace lean {
 expr abstract(expr const & e, unsigned n, expr const * subst) {
-    lean_assert(std::all_of(subst, subst+n, [](expr const & e) { return !has_loose_bvars(e) && is_local_or_fvar(e); }));
+    lean_assert(std::all_of(subst, subst+n, [](expr const & e) { return !has_loose_bvars(e) && is_fvar(e); }));
     if (!has_fvar(e))
         return e;
     return replace(e, [=](expr const & m, unsigned offset) -> optional<expr> {

stage0/stdlib/Lean/Elab.c

@@ -1,6 +1,6 @@
 // Lean compiler output
 // Module: Lean.Elab
-// Imports: Init Lean.Elab.Import Lean.Elab.Exception Lean.Elab.StrategyAttrs Lean.Elab.Command Lean.Elab.Term Lean.Elab.App Lean.Elab.Binders Lean.Elab.LetRec Lean.Elab.Quotation Lean.Elab.Frontend Lean.Elab.BuiltinNotation Lean.Elab.Declaration Lean.Elab.Tactic Lean.Elab.Syntax Lean.Elab.Match Lean.Elab.Do Lean.Elab.StructInst Lean.Elab.Inductive Lean.Elab.Structure Lean.Elab.Print Lean.Elab.MutualDef Lean.Elab.PreDefinition
+// Imports: Init Lean.Elab.Import Lean.Elab.Exception Lean.Elab.Command Lean.Elab.Term Lean.Elab.App Lean.Elab.Binders Lean.Elab.LetRec Lean.Elab.Quotation Lean.Elab.Frontend Lean.Elab.BuiltinNotation Lean.Elab.Declaration Lean.Elab.Tactic Lean.Elab.Syntax Lean.Elab.Match Lean.Elab.Do Lean.Elab.StructInst Lean.Elab.Inductive Lean.Elab.Structure Lean.Elab.Print Lean.Elab.MutualDef Lean.Elab.PreDefinition
 #include <lean/lean.h>
 #if defined(__clang__)
 #pragma clang diagnostic ignored "-Wunused-parameter"
@@ -16,7 +16,6 @@ extern "C" {
 lean_object* initialize_Init(lean_object*);
 lean_object* initialize_Lean_Elab_Import(lean_object*);
 lean_object* initialize_Lean_Elab_Exception(lean_object*);
-lean_object* initialize_Lean_Elab_StrategyAttrs(lean_object*);
 lean_object* initialize_Lean_Elab_Command(lean_object*);
 lean_object* initialize_Lean_Elab_Term(lean_object*);
 lean_object* initialize_Lean_Elab_App(lean_object*);
@@ -50,9 +49,6 @@ lean_dec_ref(res);
 res = initialize_Lean_Elab_Exception(lean_io_mk_world());
 if (lean_io_result_is_error(res)) return res;
 lean_dec_ref(res);
-res = initialize_Lean_Elab_StrategyAttrs(lean_io_mk_world());
-if (lean_io_result_is_error(res)) return res;
-lean_dec_ref(res);
 res = initialize_Lean_Elab_Command(lean_io_mk_world());
 if (lean_io_result_is_error(res)) return res;
 lean_dec_ref(res);