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

Author: Seasawher

docs/attributes.md

@@ -1,6 +1,6 @@
 # Attributes
 
-Mathlib version: `c1ee2821db22c395b37586d80ae2b7f9a24ee2cb`
+Mathlib version: `786ca91ad0b41b6ee048e3dcdd23cc71807fddbb`
 
 ## Std.Internal.tree_tac
  simp theorems used by internal DTreeMap lemmas

docs/commands.md

@@ -1,6 +1,6 @@
 # Commands
 
-Mathlib version: `c1ee2821db22c395b37586d80ae2b7f9a24ee2cb`
+Mathlib version: `786ca91ad0b41b6ee048e3dcdd23cc71807fddbb`
 
 ## \#adaptation_note
 Defined in: `adaptationNoteCmd`

docs/options.md

@@ -1,6 +1,6 @@
 # Options
 
-Mathlib version: `c1ee2821db22c395b37586d80ae2b7f9a24ee2cb`
+Mathlib version: `786ca91ad0b41b6ee048e3dcdd23cc71807fddbb`
 
 ## Elab.async
 type: `Bool`
@@ -1269,6 +1269,13 @@ default: `true`
 
 Linter used by translate attributes that checks if the given declaration name is equal to the automatically generated name
 
+## linter.translateReorder
+type: `Bool`
+
+default: `true`
+
+Linter used by translate attributes that checks if the given reorder is equal to the automatically generated one
+
 ## linter.unnecessarySeqFocus
 type: `Bool`
 
@@ -4002,13 +4009,6 @@ default: `false`
 
 enable/disable tracing for the given module and submodules
 
-## trace.Tactic.propose
-type: `Bool`
-
-default: `false`
-
-enable/disable tracing for the given module and submodules
-
 ## trace.Tactic.rewrites
 type: `Bool`
 

docs/tactics.md

@@ -1,6 +1,6 @@
 # Tactics
 
-Mathlib version: `c1ee2821db22c395b37586d80ae2b7f9a24ee2cb`
+Mathlib version: `786ca91ad0b41b6ee048e3dcdd23cc71807fddbb`
 
 ## \#adaptation_note
 Defined in: `«tactic#adaptation_note_»`
@@ -3306,59 +3306,11 @@ The tactic supports all the same syntax variants and options as the `have` term.
   which may be important for performance reasons.
     Consider using the equivalent `let +nondep` to indicate the intent.
 
-## have!?
-Defined in: `Mathlib.Tactic.Propose.«tacticHave!?:_Using__»`
-
-* `have? using a, b, c` tries to find a lemma
-  which makes use of each of the local hypotheses `a, b, c`,
-  and reports any results via trace messages.
-* `have? : h using a, b, c` only returns lemmas whose type matches `h` (which may contain `_`).
-* `have?! using a, b, c` will also call `have` to add results to the local goal state.
-
-Note that `have?` (unlike `apply?`) does not inspect the goal at all,
-only the types of the lemmas in the `using` clause.
-
-`have?` should not be left in proofs; it is a search tool, like `apply?`.
-
-Suggestions are printed as `have := f a b c`.
-
 ## have'
 Defined in: `Lean.Parser.Tactic.tacticHave'`
 
 Similar to `have`, but using `refine'`
 
-## have?
-Defined in: `Mathlib.Tactic.Propose.propose'`
-
-* `have? using a, b, c` tries to find a lemma
-  which makes use of each of the local hypotheses `a, b, c`,
-  and reports any results via trace messages.
-* `have? : h using a, b, c` only returns lemmas whose type matches `h` (which may contain `_`).
-* `have?! using a, b, c` will also call `have` to add results to the local goal state.
-
-Note that `have?` (unlike `apply?`) does not inspect the goal at all,
-only the types of the lemmas in the `using` clause.
-
-`have?` should not be left in proofs; it is a search tool, like `apply?`.
-
-Suggestions are printed as `have := f a b c`.
-
-## have?!
-Defined in: `Mathlib.Tactic.Propose.«tacticHave?!:_Using__»`
-
-* `have? using a, b, c` tries to find a lemma
-  which makes use of each of the local hypotheses `a, b, c`,
-  and reports any results via trace messages.
-* `have? : h using a, b, c` only returns lemmas whose type matches `h` (which may contain `_`).
-* `have?! using a, b, c` will also call `have` to add results to the local goal state.
-
-Note that `have?` (unlike `apply?`) does not inspect the goal at all,
-only the types of the lemmas in the `using` clause.
-
-`have?` should not be left in proofs; it is a search tool, like `apply?`.
-
-Suggestions are printed as `have := f a b c`.
-
 ## haveI
 Defined in: `Lean.Parser.Tactic.tacticHaveI__`
 

lake-manifest.json

@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "c1ee2821db22c395b37586d80ae2b7f9a24ee2cb",
+   "rev": "786ca91ad0b41b6ee048e3dcdd23cc71807fddbb",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "30cfb2255996f3e6217a77fd940fde1f3e12ccc2",
+   "rev": "26884086fb66f99b56ed363c5e54bfcc70238599",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",