9 files changed, 90 insertions, 14 deletions
diff --git a/doc/changelog/07-commands-and-options/12070-native-compiler-disabled.rst b/doc/changelog/07-commands-and-options/12070-native-compiler-disabled.rst
new file mode 100644
index 0000000000..0f30b5f5e8
--- /dev/null
+++ b/doc/changelog/07-commands-and-options/12070-native-compiler-disabled.rst
@@ -0,0 +1,5 @@
+- **Changed:**
+  Ignore -native-compiler option when built without native compute
+  support.
+  (`#12070 <https://github.com/coq/coq/pull/12070>`_,
+  by Pierre Roux).
diff --git a/doc/changelog/08-tools/12037-coqdoc-preformatted.rst b/doc/changelog/08-tools/12037-coqdoc-preformatted.rst
new file mode 100644
index 0000000000..bf65719516
--- /dev/null
+++ b/doc/changelog/08-tools/12037-coqdoc-preformatted.rst
@@ -0,0 +1,6 @@
+- **Fixed:**
+  ``coqdoc`` now reports the location of a mismatched opening ``[[`` instead of
+  throwing an uninformative exception.
+  (`#12037 <https://github.com/coq/coq/pull/12037>`_,
+  fixes `#9670 <https://github.com/coq/coq/issues/9670>`_,
+  by Lysxia).
diff --git a/doc/changelog/10-standard-library/11957-signotations.rst b/doc/changelog/10-standard-library/11957-signotations.rst
new file mode 100644
index 0000000000..fc5d434274
--- /dev/null
+++ b/doc/changelog/10-standard-library/11957-signotations.rst
@@ -0,0 +1,4 @@
+- **Added:**
+  notations for sigma types: ``{ x & P & Q }``, ``{ ' pat & P }``, ``{ ' pat & P & Q }``
+  (`#11957 <https://github.com/coq/coq/pull/11957>`_,
+  by Olivier Laurent).
diff --git a/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg b/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg
index 73d94c2a51..8c2090f3be 100644
--- a/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg
+++ b/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg
@@ -286,8 +286,8 @@ END
 VERNAC COMMAND EXTEND ExploreProof CLASSIFIED AS QUERY
 | ![ proof_query ] [ "ExploreProof" ] ->
   { fun ~pstate ->
-    let sigma, env = Pfedit.get_current_context pstate in
-    let pprf = Proof.partial_proof (Proof_global.get_proof pstate) in
+    let sigma, env = Declare.get_current_context pstate in
+    let pprf = Proof.partial_proof (Declare.Proof.get_proof pstate) in
     Feedback.msg_notice
       (Pp.prlist_with_sep Pp.fnl (Printer.pr_econstr_env env sigma) pprf)
   }
diff --git a/doc/plugin_tutorial/tuto1/src/simple_declare.ml b/doc/plugin_tutorial/tuto1/src/simple_declare.ml
index 8c4dc0e8a6..b94b1fc657 100644
--- a/doc/plugin_tutorial/tuto1/src/simple_declare.ml
+++ b/doc/plugin_tutorial/tuto1/src/simple_declare.ml
@@ -1,8 +1,6 @@
-let edeclare ?hook ~name ~poly ~scope ~kind ~opaque ~udecl ~impargs sigma body tyopt  =
-  DeclareDef.declare_definition ~name ~scope ~kind ~impargs ?hook
-    ~opaque ~poly ~udecl ~types:tyopt ~body sigma
-
 let declare_definition ~poly name sigma body =
   let udecl = UState.default_univ_decl in
-  edeclare ~name ~poly ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior)
-    ~kind:Decls.(IsDefinition Definition) ~opaque:false ~impargs:[] ~udecl sigma body None
+  let scope = DeclareDef.Global Declare.ImportDefaultBehavior in
+  let kind = Decls.(IsDefinition Definition) in
+  DeclareDef.declare_definition ~name ~scope ~kind ~impargs:[] ~udecl
+    ~opaque:false ~poly ~types:None ~body sigma
diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index 78b1f02383..57c8683aaa 100644
--- a/doc/sphinx/language/gallina-extensions.rst
+++ b/doc/sphinx/language/gallina-extensions.rst
@@ -422,7 +422,12 @@ are now available through the dot notation.
    If :n:`@module_binder`\s are specified, declares a functor with parameters given by the list of
    :token:`module_binder`\s.
 
-.. cmd:: Import {+ @qualid }
+.. cmd:: Import {+ @filtered_import }
+
+   .. insertprodn filtered_import filtered_import
+
+   .. prodn::
+      filtered_import ::= @qualid {? ( {+, @qualid {? ( .. ) } } ) }
 
    If :token:`qualid` denotes a valid basic module (i.e. its module type is a
    signature), makes its components available by their short names.
@@ -465,12 +470,50 @@ are now available through the dot notation.
 
          Check B.T.
 
-.. cmd:: Export {+ @qualid }
+   Appending a module name with a parenthesized list of names will
+   make only those names available with short names, not other names
+   defined in the module nor will it activate other features.
+
+   The names to import may be constants, inductive types and
+   constructors, and notation aliases (for instance, Ltac definitions
+   cannot be selectively imported). If they are from an inner module
+   to the one being imported, they must be prefixed by the inner path.
+
+   The name of an inductive type may also be followed by ``(..)`` to
+   import it, its constructors and its eliminators if they exist. For
+   this purpose "eliminator" means a constant in the same module whose
+   name is the inductive type's name suffixed by one of ``_sind``,
+   ``_ind``, ``_rec`` or ``_rect``.
+
+   .. example::
+
+      .. coqtop:: reset in
+
+         Module A.
+         Module B.
+         Inductive T := C.
+         Definition U := nat.
+         End B.
+         Definition Z := Prop.
+         End A.
+         Import A(B.T(..), Z).
+
+      .. coqtop:: all
+
+         Check B.T.
+         Check B.C.
+         Check Z.
+         Fail Check B.U.
+         Check A.B.U.
+
+.. cmd:: Export {+ @filtered_import }
    :name: Export
 
    Similar to :cmd:`Import`, except that when the module containing this command
    is imported, the :n:`{+ @qualid }` are imported as well.
 
+   The selective import syntax also works with Export.
+
    .. exn:: @qualid is not a module.
       :undocumented:
 
diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg
index a01f57eb22..5034d9a3c9 100644
--- a/doc/tools/docgram/common.edit_mlg
+++ b/doc/tools/docgram/common.edit_mlg
@@ -511,6 +511,12 @@ strategy_flag: [
 | OPTINREF
 ]
 
+filtered_import: [
+| REPLACE global "(" LIST1 one_import_filter_name SEP "," ")"
+| WITH global OPT [ "(" LIST1 one_import_filter_name SEP "," ")" ]
+| DELETE global
+]
+
 functor_app_annot: [
 | OPTINREF
 ]
@@ -1582,6 +1588,7 @@ SPLICE: [
 | searchabout_queries
 | locatable
 | scope_delimiter
+| one_import_filter_name
 ] (* end SPLICE *)
 
 RENAME: [
diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar
index dc7e0fba37..04c20a7203 100644
--- a/doc/tools/docgram/fullGrammar
+++ b/doc/tools/docgram/fullGrammar
@@ -1031,8 +1031,8 @@ gallina_ext: [
 | "Collection" identref ":=" section_subset_expr
 | "Require" export_token LIST1 global
 | "From" global "Require" export_token LIST1 global
-| "Import" LIST1 global
-| "Export" LIST1 global
+| "Import" LIST1 filtered_import
+| "Export" LIST1 filtered_import
 | "Include" module_type_inl LIST0 ext_module_expr
 | "Include" "Type" module_type_inl LIST0 ext_module_type
 | "Transparent" LIST1 smart_global
@@ -1057,6 +1057,15 @@ gallina_ext: [
 | "Export" "Unset" option_table
 ]
 
+filtered_import: [
+| global
+| global "(" LIST1 one_import_filter_name SEP "," ")"
+]
+
+one_import_filter_name: [
+| global OPT [ "(" ".." ")" ]
+]
+
 export_token: [
 | "Import"
 | "Export"
diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar
index ac986f9adf..e71c80f829 100644
--- a/doc/tools/docgram/orderedGrammar
+++ b/doc/tools/docgram/orderedGrammar
@@ -497,6 +497,10 @@ constructor: [
 | ident LIST0 binder OPT of_type
 ]
 
+filtered_import: [
+| qualid OPT [ "(" LIST1 ( qualid OPT [ "(" ".." ")" ] ) SEP "," ")" ]
+]
+
 cofix_definition: [
 | ident_decl LIST0 binder OPT ( ":" type ) OPT [ ":=" term ] OPT decl_notations
 ]
@@ -849,8 +853,8 @@ command: [
 | "Collection" ident ":=" section_subset_expr
 | "Require" OPT [ "Import" | "Export" ] LIST1 qualid
 | "From" dirpath "Require" OPT [ "Import" | "Export" ] LIST1 qualid
-| "Import" LIST1 qualid
-| "Export" LIST1 qualid
+| "Import" LIST1 filtered_import
+| "Export" LIST1 filtered_import
 | "Include" module_type_inl LIST0 ( "<+" module_expr_inl )
 | "Include" "Type" LIST1 module_type_inl SEP "<+"
 | "Transparent" LIST1 smart_qualid