Support universe bindings and universe constraints in Let definitions.

Let vs Definition / Example syntax was split in 7c28130 for parsing
reasons: so that the new Let Fixpoint and Let CoFixpoint syntax could
be introduced.  This split is probably the reason why Let was
overlooked when support for universe bindings and universe constraints
were added to Definition and variants.

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) }