11 files changed, 208 insertions, 36 deletions

diff --git a/dev/tools/pre-commit b/dev/tools/pre-commit
index 633913aac6..448e224f2e 100755
--- a/dev/tools/pre-commit
+++ b/dev/tools/pre-commit
@@ -16,6 +16,15 @@ then
     1>&2 echo "Warning: ocamlformat is not in path. Cannot check formatting."
 fi
 
+# Verify that the version of ocamlformat matches the one in .ocamlformat
+# The following command will print an error message if that's not the case
+# (and will print nothing if the versions match)
+if ! echo "let () = ()" | "$ocamlformat" --impl - > /dev/null
+then
+    1>&2 echo "Warning: Cannot check formatting."
+    ocamlformat=true
+fi
+
 1>&2 echo "Auto fixing whitespace and formatting issues..."
 
 # We fix whitespace in the index and in the working tree
@@ -43,7 +52,7 @@ if [ -s "$index" ]; then
     git apply --cached --whitespace=fix "$index"
     git apply --whitespace=fix "$index" 2>/dev/null # no need to repeat yourself
     git diff --cached --name-only -z | xargs -0 dev/tools/check-eof-newline.sh --fix
-    git diff --cached --name-only -z | grep -E '.*\.mli?$' -z | xargs -0 "$ocamlformat" -i || true
+    { git diff --cached --name-only -z | grep -E '.*\.mli?$' -z | xargs -0 "$ocamlformat" -i || true; } 2> /dev/null
     git add -u
     1>&2 echo #newline
 fi
@@ -59,7 +68,7 @@ if [ -s "$tree" ]; then
     1>&2 echo "Fixing unstaged changes..."
     git apply --whitespace=fix "$tree"
     git diff --name-only -z | xargs -0 dev/tools/check-eof-newline.sh --fix
-    git diff --name-only -z | grep -E '.*\.mli?$' -z | xargs -0 "$ocamlformat" -i || true
+    { git diff --name-only -z | grep -E '.*\.mli?$' -z | xargs -0 "$ocamlformat" -i || true; } 2> /dev/null
     1>&2 echo #newline
 fi
 
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/changelog/10-standard-library/11909-fix-≡-level.rst b/doc/changelog/10-standard-library/11909-fix-≡-level.rst
new file mode 100644
index 0000000000..96551be537
--- /dev/null
+++ b/doc/changelog/10-standard-library/11909-fix-≡-level.rst
@@ -0,0 +1,7 @@
+- **Changed:**
+  The level of :g:`≡` in ``Coq.Numbers.Cyclic.Int63.Int63`` is now 70,
+  no associativity, in line with :g:`=`.  Note that this is a minor
+  incompatibility with developments that declare their own :g:`≡`
+  notation and import ``Int63`` (fixes `#11905
+  <https://github.com/coq/coq/issues/11905>`_, `#11909
+  <https://github.com/coq/coq/pull/11909>`_, by Jason Gross).
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/theories/Numbers/Cyclic/Int63/Int63.v b/theories/Numbers/Cyclic/Int63/Int63.v
index c4f738ac39..bacc4a7650 100644
--- a/theories/Numbers/Cyclic/Int63/Int63.v
+++ b/theories/Numbers/Cyclic/Int63/Int63.v
@@ -690,7 +690,7 @@ Proof. now intros h; rewrite (to_Z_inj _ 0 h). Qed.
 Lemma tail00_spec x : φ  x = 0 -> φ (tail0 x) = φ digits.
 Proof. now intros h; rewrite (to_Z_inj _ 0 h). Qed.
 
-Infix "≡" := (eqm wB) (at level 80) : int63_scope.
+Infix "≡" := (eqm wB) (at level 70, no associativity) : int63_scope.
 
 Lemma eqm_mod x y : x mod wB ≡ y mod wB → x ≡ y.
 Proof.
diff --git a/theories/Structures/OrderedTypeEx.v b/theories/Structures/OrderedTypeEx.v
index 288aa0c789..83c690ab71 100644
--- a/theories/Structures/OrderedTypeEx.v
+++ b/theories/Structures/OrderedTypeEx.v
@@ -317,6 +317,82 @@ Module PositiveOrderedTypeBits <: UsualOrderedType.
 
 End PositiveOrderedTypeBits.
 
+Module Ascii_as_OT <: UsualOrderedType.
+  Definition t := ascii.
+
+  Definition eq := @eq ascii.
+  Definition eq_refl := @eq_refl t.
+  Definition eq_sym := @eq_sym t.
+  Definition eq_trans := @eq_trans t.
+
+  Definition cmp (a b : ascii) : comparison :=
+    N.compare (N_of_ascii a) (N_of_ascii b).
+
+  Lemma cmp_eq (a b : ascii):
+    cmp a b = Eq  <->  a = b.
+  Proof.
+    unfold cmp.
+    rewrite N.compare_eq_iff.
+    split. 2:{ intro. now subst. }
+    intro H.
+    rewrite<- (ascii_N_embedding a).
+    rewrite<- (ascii_N_embedding b).
+    now rewrite H.
+  Qed.
+
+  Lemma cmp_lt_nat (a b : ascii):
+    cmp a b = Lt  <->  (nat_of_ascii a < nat_of_ascii b)%nat.
+  Proof.
+    unfold cmp. unfold nat_of_ascii.
+    rewrite N2Nat.inj_compare.
+    rewrite Nat.compare_lt_iff.
+    reflexivity.
+  Qed.
+
+  Lemma cmp_antisym (a b : ascii):
+    cmp a b = CompOpp (cmp b a).
+  Proof.
+    unfold cmp.
+    apply N.compare_antisym.
+  Qed.
+
+  Definition lt (x y : ascii) := (N_of_ascii x < N_of_ascii y)%N.
+
+  Lemma lt_trans (x y z : ascii):
+    lt x y -> lt y z -> lt x z.
+  Proof.
+    apply N.lt_trans.
+  Qed.
+
+  Lemma lt_not_eq (x y : ascii):
+     lt x y -> x <> y.
+  Proof.
+    intros L H. subst.
+    exact (N.lt_irrefl _ L).
+  Qed.
+
+  Local Lemma compare_helper_eq {a b : ascii} (E : cmp a b = Eq):
+    a = b.
+  Proof.
+    now apply cmp_eq.
+  Qed.
+
+  Local Lemma compare_helper_gt {a b : ascii} (G : cmp a b = Gt):
+    lt b a.
+  Proof.
+    now apply N.compare_gt_iff.
+  Qed.
+
+  Definition compare (a b : ascii) : Compare lt eq a b :=
+    match cmp a b as z return _ = z -> _ with
+    | Lt => fun E => LT E
+    | Gt => fun E => GT (compare_helper_gt E)
+    | Eq => fun E => EQ (compare_helper_eq E)
+    end Logic.eq_refl.
+
+  Definition eq_dec (x y : ascii): {x = y} + { ~ (x = y)} := ascii_dec x y.
+End Ascii_as_OT.
+
 (** [String] is an ordered type with respect to the usual lexical order. *)
 
 Module String_as_OT <: UsualOrderedType.
@@ -378,32 +454,106 @@ Module String_as_OT <: UsualOrderedType.
         apply Nat.lt_irrefl in H2; auto.
   Qed.
 
-  Definition compare x y : Compare lt eq x y.
+  Fixpoint cmp (a b : string) : comparison :=
+    match a, b with
+    | EmptyString, EmptyString => Eq
+    | EmptyString, _ => Lt
+    | String _ _, EmptyString => Gt
+    | String a_head a_tail, String b_head b_tail =>
+      match Ascii_as_OT.cmp a_head b_head with
+      | Lt => Lt
+      | Gt => Gt
+      | Eq => cmp a_tail b_tail
+      end
+    end.
+
+  Lemma cmp_eq (a b : string):
+    cmp a b = Eq  <->  a = b.
   Proof.
-    generalize dependent y.
-    induction x as [ | a s1]; destruct y as [ | b s2].
-    - apply EQ; constructor.
-    - apply LT; constructor.
-    - apply GT; constructor.
-    - destruct ((nat_of_ascii a) ?= (nat_of_ascii b))%nat eqn:ltb.
-      + assert (a = b).
-        {
-          apply Nat.compare_eq in ltb.
-          assert (ascii_of_nat (nat_of_ascii a)
-                  = ascii_of_nat (nat_of_ascii b)) by auto.
-          repeat rewrite ascii_nat_embedding in H.
-          auto.
-        }
-        subst.
-        destruct (IHs1 s2).
-        * apply LT; constructor; auto.
-        * apply EQ. unfold eq in e. subst. constructor; auto.
-        * apply GT; constructor; auto.
-      + apply nat_compare_lt in ltb.
-        apply LT; constructor; auto.
-      + apply nat_compare_gt in ltb.
-        apply GT; constructor; auto.
-  Defined.
+    revert b.
+    induction a, b; try easy.
+    cbn.
+    remember (Ascii_as_OT.cmp _ _) as c eqn:Heqc. symmetry in Heqc.
+    destruct c; split; try discriminate;
+      try rewrite Ascii_as_OT.cmp_eq in Heqc; try subst;
+      try rewrite IHa; intro H.
+    { now subst. }
+    { now inversion H. }
+    { inversion H; subst. rewrite<- Heqc. now rewrite Ascii_as_OT.cmp_eq. }
+    { inversion H; subst. rewrite<- Heqc. now rewrite Ascii_as_OT.cmp_eq. }
+  Qed.
+
+  Lemma cmp_antisym (a b : string):
+    cmp a b = CompOpp (cmp b a).
+  Proof.
+    revert b.
+    induction a, b; try easy.
+    cbn. rewrite IHa. clear IHa.
+    remember (Ascii_as_OT.cmp _ _) as c eqn:Heqc. symmetry in Heqc.
+    destruct c; rewrite Ascii_as_OT.cmp_antisym in Heqc;
+      destruct Ascii_as_OT.cmp; cbn in *; easy.
+  Qed.
+
+  Lemma cmp_lt (a b : string):
+    cmp a b = Lt  <->  lt a b.
+  Proof.
+    revert b.
+    induction a as [ | a_head a_tail ], b; try easy; cbn.
+    { split; trivial. intro. apply lts_empty. }
+    remember (Ascii_as_OT.cmp _ _) as c eqn:Heqc. symmetry in Heqc.
+    destruct c; split; intro H; try discriminate; trivial.
+    {
+      rewrite Ascii_as_OT.cmp_eq in Heqc. subst.
+      apply String_as_OT.lts_tail.
+      apply IHa_tail.
+      assumption.
+    }
+    {
+      rewrite Ascii_as_OT.cmp_eq in Heqc. subst.
+      inversion H; subst. { rewrite IHa_tail. assumption. }
+      exfalso. apply (Nat.lt_irrefl (nat_of_ascii a)). assumption.
+    }
+    {
+      apply String_as_OT.lts_head.
+      rewrite<- Ascii_as_OT.cmp_lt_nat.
+      assumption.
+    }
+    {
+      exfalso. inversion H; subst.
+      {
+         assert(X: Ascii_as_OT.cmp a a = Eq). { apply Ascii_as_OT.cmp_eq. trivial. }
+         rewrite Heqc in X. discriminate.
+      }
+      rewrite<- Ascii_as_OT.cmp_lt_nat in *. rewrite Heqc in *. discriminate.
+    }
+  Qed.
+
+  Local Lemma compare_helper_lt {a b : string} (L : cmp a b = Lt):
+    lt a b.
+  Proof.
+    now apply cmp_lt.
+  Qed.
+
+  Local Lemma compare_helper_gt {a b : string} (G : cmp a b = Gt):
+    lt b a.
+  Proof.
+    rewrite cmp_antisym in G.
+    rewrite CompOpp_iff in G.
+    now apply cmp_lt.
+  Qed.
+
+  Local Lemma compare_helper_eq {a b : string} (E : cmp a b = Eq):
+    a = b.
+  Proof.
+    now apply cmp_eq.
+  Qed.
+
+  Definition compare (a b : string) : Compare lt eq a b :=
+    match cmp a b as z return _ = z -> _ with
+    | Lt => fun E => LT (compare_helper_lt E)
+    | Gt => fun E => GT (compare_helper_gt E)
+    | Eq => fun E => EQ (compare_helper_eq E)
+    end Logic.eq_refl.
 
   Definition eq_dec (x y : string): {x = y} + { ~ (x = y)} := string_dec x y.
 End String_as_OT.
diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in
index f72b99c57c..597351db9b 100644
--- a/tools/CoqMakefile.in
+++ b/tools/CoqMakefile.in
@@ -54,7 +54,7 @@ OCAMLWARN         := $(COQMF_WARN)
 #
 # Parameters are make variable assignments.
 # They can be passed to (each call to) make on the command line.
-# They can also be put in @LOCAL_FILE@ once an for all.
+# They can also be put in @LOCAL_FILE@ once and for all.
 # For retro-compatibility reasons they can be put in the _CoqProject, but this
 # practice is discouraged since _CoqProject better not contain make specific
 # code (be nice to user interfaces).
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) }