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

Author: Seasawher

docs/attributes.md

@@ -1,6 +1,6 @@
 # Attributes
 
-Mathlib version: `a8071348b19ed841a1f46dbd5a25d109bc804711`
+Mathlib version: `b30c0393ac6454d5d43ee1d1a6760c1939a2302b`
 
 ## Std.Internal.tree_tac
  simp theorems used by internal DTreeMap lemmas
@@ -254,6 +254,21 @@ This allows the documentation of core Lean features to be visible without import
 are defined in. This is only useful during bootstrapping and should not be used outside of
 the Lean source code.
 
+## builtin_doc_code_block
+ docstring code block expander
+
+## builtin_doc_code_suggestions
+ docstring code element suggestion provider
+
+## builtin_doc_command
+ builtin docstring command expander
+
+## builtin_doc_directive
+ docstring directive expander
+
+## builtin_doc_role
+ docstring role expander
+
 ## builtin_formatter
  (builtin) Register a formatter for a parser.
 Registers a formatter for a parser.
@@ -569,6 +584,21 @@ special casing. If the term is an `Expr.mdata` with a single key `k`, `mdata.k`
 ## doElem_parser
  parser
 
+## doc_code_block
+ docstring code block expander
+
+## doc_code_suggestions
+ docstring code element suggestion provider
+
+## doc_command
+ docstring command expander
+
+## doc_directive
+ docstring directive expander
+
+## doc_role
+ docstring role expander
+
 ## elab_as_elim
  instructs elaborator that the arguments of the function application should be elaborated as were an eliminator
 Instructs the elaborator that applications of this function should be elaborated like an eliminator.
@@ -760,6 +790,13 @@ Lemmas involving `<` or `≤` can also be marked `@[bound]` for use in the relat
 ## gcongr_forward
  adds a gcongr_forward extension
 
+## gen_constructor_elims
+ generate the `.toCtorIdx` and `.ctor.elim` definitions for the given inductive
+Generate the `.toCtorIdx` and `.ctor.elim` definitions for the given inductive.
+
+This attribute is only meant to be used in `Init.Prelude` to build these constructions for
+types where we did not generate them imediatelly (due to `set_option genCtorIdx false`).
+
 ## ghost_simps
  Simplification rules for ghost equations. 
 

docs/commands.md

@@ -1,6 +1,6 @@
 # Commands
 
-Mathlib version: `a8071348b19ed841a1f46dbd5a25d109bc804711`
+Mathlib version: `b30c0393ac6454d5d43ee1d1a6760c1939a2302b`
 
 ## \#adaptation_note
 Defined in: `adaptationNoteCmd`
@@ -463,7 +463,8 @@ In general, `#guard_msgs` accepts a comma-separated list of configuration clause
 ```lean
 #guard_msgs (configElt,*) in cmd
 ```
-By default, the configuration list is `(check all, whitespace := normalized, ordering := exact)`.
+By default, the configuration list is
+`(check all, whitespace := normalized, ordering := exact, positions := false)`.
 
 Message filters select messages by severity:
 - `info`, `warning`, `error`: (non-trace) messages with the given severity level.
@@ -489,6 +490,11 @@ Message ordering:
 - `ordering := sorted` sorts the messages in lexicographic order.
   This helps with testing commands that are non-deterministic in their ordering.
 
+Position reporting:
+- `positions := true` reports the ranges of all messages relative to the line on which
+  `#guard_msgs` appears.
+- `positions := false` does not report position info.
+
 For example, `#guard_msgs (error, drop all) in cmd` means to check warnings and drop
 everything else.
 
@@ -623,17 +629,6 @@ Another important difference is that the `minImports` *linter* starts counting i
 where the option is set to `true` *downwards*, whereas the `#min_imports` *command* looks at the
 imports needed from the command *upwards*.
 
-## \#import_diff
-Defined in: `«command#import_diff_»`
-
-`#import_diff foo bar ...` computes the new transitive imports that are added to a given file when
-modules `foo, bar, ...` are added to the set of imports of the file. More precisely, it computes the
-import diff between when `foo, bar, ...` are added to the imports and when `foo, bar, ...` are removed
-from the imports.
-
-Note: the command also works when some of the modules passed as arguments are already present in the file's
-imports.
-
 ## \#info_trees
 Defined in: `Lean.infoTreesCmd`
 
@@ -1657,8 +1652,9 @@ docs of `<declName>` by adding `<prefix_string>` before and `<suffix_string>` af
 ## gen_injective_theorems%
 Defined in: `Lean.Parser.Command.genInjectiveTheorems`
 
-This is an auxiliary command for generation constructor injectivity theorems for
+This is an auxiliary command to generate constructor injectivity theorems for
 inductive types defined at `Prelude.lean`.
+Temporarily also controls the generation of the `ctorIdx` definition.
 It is meant for bootstrapping purposes only.
 
 ## grind_pattern
@@ -2318,7 +2314,7 @@ which helps in maintaining the desired abstraction level without affecting globa
 ## section
 Defined in: `Lean.Parser.Command.section`
 
-A `section`/`end` pair delimits the scope of `variable`, `include, `open`, `set_option`, and `local`
+A `section`/`end` pair delimits the scope of `variable`, `include`, `open`, `set_option`, and `local`
 commands. Sections can be nested. `section <id>` provides a label to the section that has to appear
 with the matching `end`. In either case, the `end` can be omitted, in which case the section is
 closed at the end of the file.