Merge pull request #168 from Seasawher/auto-update-branch

Author: Seasawher

docs/attributes.md

@@ -1,6 +1,6 @@
 # Attributes
 
-Mathlib version: `6d297a4172e6c37d3bf82e68924c45d72621ac5d`
+Mathlib version: `955e8f97a6372ceeeb97f4acc87f71ae1fea7d85`
 
 ## aesop
  Register a declaration as an Aesop rule.

docs/commands.md

@@ -1,6 +1,6 @@
 # Commands
 
-Mathlib version: `6d297a4172e6c37d3bf82e68924c45d72621ac5d`
+Mathlib version: `955e8f97a6372ceeeb97f4acc87f71ae1fea7d85`
 
 ## \#adaptation_note
 Defined in: `adaptationNoteCmd`
@@ -1269,7 +1269,7 @@ Defined in: `commandDeclare_uint_theorems_`
 
 
 ## deprecate to
-Defined in: `Mathlib.Tactic.DeprecateMe.commandDeprecate_to______`
+Defined in: `Mathlib.Tactic.DeprecateTo.commandDeprecate_to______`
 
 Writing
 ```lean
@@ -1367,7 +1367,7 @@ end Evening.Sky
 #check Evening.Sky.star
 ```
 
-## export private
+## export
 Defined in: `Lean.Elab.Command.exportPrivate`
 
 The command `export private a b c in foo bar` is similar to `open private`, but instead of opening
@@ -1712,6 +1712,19 @@ can also refer to typeclass instance variables by type using the syntax `omit [T
 which case all instance variables that unify with the given type are omitted. `omit` should usually
 only be used in conjunction with `in` in order to keep the section structure simple.
 
+## open
+Defined in: `Lean.Elab.Command.openPrivate`
+
+The command `open private a b c in foo bar` will look for private definitions named `a`, `b`, `c`
+in declarations `foo` and `bar` and open them in the current scope. This does not make the
+definitions public, but rather makes them accessible in the current section by the short name `a`
+instead of the (unnameable) internal name for the private declaration, something like
+`_private.Other.Module.0.Other.Namespace.foo.a`, which cannot be typed directly because of the `0`
+name component.
+
+It is also possible to specify the module instead with
+`open private a b c from Other.Module`.
+
 ## open
 Defined in: `Lean.Parser.Command.open`
 
@@ -1827,19 +1840,6 @@ section
 end
 ```
 
-## open private
-Defined in: `Lean.Elab.Command.openPrivate`
-
-The command `open private a b c in foo bar` will look for private definitions named `a`, `b`, `c`
-in declarations `foo` and `bar` and open them in the current scope. This does not make the
-definitions public, but rather makes them accessible in the current section by the short name `a`
-instead of the (unnameable) internal name for the private declaration, something like
-`_private.Other.Module.0.Other.Namespace.foo.a`, which cannot be typed directly because of the `0`
-name component.
-
-It is also possible to specify the module instead with
-`open private a b c from Other.Module`.
-
 ## proof_wanted
 Defined in: `«proof_wanted»`
 

docs/options.md

@@ -1,6 +1,6 @@
 # Options
 
-Mathlib version: `6d297a4172e6c37d3bf82e68924c45d72621ac5d`
+Mathlib version: `955e8f97a6372ceeeb97f4acc87f71ae1fea7d85`
 
 ## Mathlib.Tactic.TFAE.useDeprecated
 type: `Bool`
@@ -758,6 +758,13 @@ default: `true`
 
 enable the 'unused variables' linter to mark unused pattern variables
 
+## linter.upstreamableDecl
+type: `Bool`
+
+default: `false`
+
+enable the upstreamableDecl linter
+
 ## loogle.queries
 type: `Nat`
 

docs/tactics.md

@@ -1,6 +1,6 @@
 # Tactics
 
-Mathlib version: `6d297a4172e6c37d3bf82e68924c45d72621ac5d`
+Mathlib version: `955e8f97a6372ceeeb97f4acc87f71ae1fea7d85`
 
 ## \#adaptation_note
 Defined in: `«tactic#adaptation_note_»`

lake-manifest.json

@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "b100ff2565805e9f30a482788b3fc66937a7f38a",
+   "rev": "01f4969b6e861db6a99261ea5eadd5a9bb63011b",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -55,7 +55,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "b0b73e5bc33f1bc4d3c0f254630dd0e262cecc08",
+   "rev": "119b022b3ea88ec810a677888528e50f8144a26e",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -85,7 +85,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "6d297a4172e6c37d3bf82e68924c45d72621ac5d",
+   "rev": "955e8f97a6372ceeeb97f4acc87f71ae1fea7d85",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",