Merge PR #11534: Support universe bindings and universe constraints in Let definitions.

Reviewed-by: SkySkimmer

6 files changed, 13 insertions, 7 deletions

diff --git a/doc/changelog/07-commands-and-options/11534-let-with-annotations.rst b/doc/changelog/07-commands-and-options/11534-let-with-annotations.rst
new file mode 100644
index 0000000000..7bcbb9a8e3
--- /dev/null
+++ b/doc/changelog/07-commands-and-options/11534-let-with-annotations.rst
@@ -0,0 +1,3 @@
+- **Added:** Support for universe bindings and universe contrainsts in
+  :cmd:`Let` definitions (`#11534
+  <https://github.com/coq/coq/pull/11534>`_, by Théo Zimmermann).
diff --git a/doc/sphinx/language/core/sections.rst b/doc/sphinx/language/core/sections.rst
index 9ad8df2b1b..df50dbafe3 100644
--- a/doc/sphinx/language/core/sections.rst
+++ b/doc/sphinx/language/core/sections.rst
@@ -72,7 +72,7 @@ Sections create local contexts which can be shared across multiple definitions.
    Most commands, like :cmd:`Hint`, :cmd:`Notation`, option management, … which
    appear inside a section are canceled when the section is closed.
 
-.. cmd:: Let @ident @def_body
+.. cmd:: Let @ident_decl @def_body
          Let Fixpoint @fix_definition {* with @fix_definition }
          Let CoFixpoint @cofix_definition {* with @cofix_definition }
    :name: Let; Let Fixpoint; Let CoFixpoint
diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar
index 272d17bb35..dc7e0fba37 100644
--- a/doc/tools/docgram/fullGrammar
+++ b/doc/tools/docgram/fullGrammar
@@ -773,7 +773,7 @@ gallina: [
 | assumption_token inline assum_list
 | assumptions_token inline assum_list
 | def_token ident_decl def_body
-| "Let" identref def_body
+| "Let" ident_decl def_body
 | finite_token LIST1 inductive_definition SEP "with"
 | "Fixpoint" LIST1 rec_definition SEP "with"
 | "Let" "Fixpoint" LIST1 rec_definition SEP "with"
@@ -1027,7 +1027,6 @@ gallina_ext: [
 | "Module" "Type" identref LIST0 module_binder check_module_types is_module_type
 | "Declare" "Module" export_token identref LIST0 module_binder ":" module_type_inl
 | "Section" identref
-| "Chapter" identref
 | "End" identref
 | "Collection" identref ":=" section_subset_expr
 | "Require" export_token LIST1 global
diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar
index 0c9d7a853b..535976b7d9 100644
--- a/doc/tools/docgram/orderedGrammar
+++ b/doc/tools/docgram/orderedGrammar
@@ -851,7 +851,7 @@ command: [
 | thm_token ident_decl LIST0 binder ":" type LIST0 [ "with" ident_decl LIST0 binder ":" type ]
 | assumption_token OPT ( "Inline" OPT ( "(" num ")" ) ) [ LIST1 ( "(" assumpt ")" ) | assumpt ]
 | [ "Definition" | "Example" ] ident_decl def_body
-| "Let" ident def_body
+| "Let" ident_decl def_body
 | "Inductive" inductive_definition LIST0 ( "with" inductive_definition )
 | "Fixpoint" fix_definition LIST0 ( "with" fix_definition )
 | "Let" "Fixpoint" fix_definition LIST0 ( "with" fix_definition )
@@ -873,7 +873,6 @@ command: [
 | "Module" "Type" ident LIST0 module_binder LIST0 ( "<:" module_type_inl ) OPT ( ":=" LIST1 module_type_inl SEP "<+" )
 | "Declare" "Module" OPT [ "Import" | "Export" ] ident LIST0 module_binder ":" module_type_inl
 | "Section" ident
-| "Chapter" ident
 | "End" ident
 | "Collection" ident ":=" section_subset_expr
 | "Require" OPT [ "Import" | "Export" ] LIST1 qualid
diff --git a/test-suite/success/let_universes.v b/test-suite/success/let_universes.v
new file mode 100644
index 0000000000..c780ec010f
--- /dev/null
+++ b/test-suite/success/let_universes.v
@@ -0,0 +1,5 @@
+Section S.
+Let bla@{} := Prop.
+Let bli@{u} := Type@{u}.
+Fail Let blo@{} := Type.
+End S.
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 31fc54c1fa..1f52641b82 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -199,8 +199,8 @@ GRAMMAR EXTEND Gram
             VernacAssumption (stre, nl, bl) }
       | d = def_token; id = ident_decl; b = def_body ->
           { VernacDefinition (d, name_of_ident_decl id, b) }
-      | IDENT "Let"; id = identref; b = def_body ->
-          { VernacDefinition ((DoDischarge, Let), (lname_of_lident id, None), b) }
+      | IDENT "Let"; id = ident_decl; b = def_body ->
+          { VernacDefinition ((DoDischarge, Let), name_of_ident_decl id, b) }
       (* Gallina inductive declarations *)
       | f = finite_token; indl = LIST1 inductive_definition SEP "with" ->
           { VernacInductive (f, indl) }