20 files changed, 523 insertions, 34 deletions
diff --git a/test-suite/bugs/closed/bug_10669.v b/test-suite/bugs/closed/bug_10669.v
new file mode 100644
index 0000000000..433e300acb
--- /dev/null
+++ b/test-suite/bugs/closed/bug_10669.v
@@ -0,0 +1,12 @@
+
+Context (A0:Type) (B0:A0).
+Definition foo0 := B0.
+
+Set Universe Polymorphism.
+Context (A1:Type) (B1:A1).
+Definition foo1 := B1.
+
+Section S.
+  Context (A2:Type) (B2:A2).
+  Definition foo2 := B2.
+End S.
diff --git a/test-suite/bugs/closed/bug_10757.v b/test-suite/bugs/closed/bug_10757.v
new file mode 100644
index 0000000000..a531f6e563
--- /dev/null
+++ b/test-suite/bugs/closed/bug_10757.v
@@ -0,0 +1,38 @@
+Require Import Program Extraction ExtrOcamlBasic.
+Print sig.
+Section FIXPOINT.
+
+Variable A: Type.
+
+Variable eq: A -> A -> Prop.
+Variable beq: A -> A -> bool.
+Hypothesis beq_eq: forall x y, beq x y = true -> eq x y.
+Hypothesis beq_neq: forall x y, beq x y = false -> ~eq x y.
+
+Variable le: A -> A -> Prop.
+Hypothesis le_trans: forall x y z, le x y -> le y z -> le x z.
+
+Definition gt (x y: A) := le y x /\ ~eq y x.
+Hypothesis gt_wf: well_founded gt.
+
+Variable F: A -> A.
+Hypothesis F_mon: forall x y, le x y -> le (F x) (F y).
+
+Program Fixpoint iterate
+    (x: A) (PRE: le x (F x)) (SMALL: forall z, le (F z) z -> le x z)
+    {wf gt x}
+    : {y : A | eq y (F y) /\ forall z, le (F z) z -> le y z } :=
+  let x' := F x in
+  match beq x x' with
+  | true  => x
+  | false => iterate x' _ _
+  end.
+Next Obligation.
+  split.
+- auto.
+- apply beq_neq. auto.
+Qed.
+
+End FIXPOINT.
+
+Recursive Extraction iterate.
diff --git a/test-suite/bugs/closed/bug_10778.v b/test-suite/bugs/closed/bug_10778.v
new file mode 100644
index 0000000000..25d729b7e6
--- /dev/null
+++ b/test-suite/bugs/closed/bug_10778.v
@@ -0,0 +1,32 @@
+(* Test that fresh avoid the variables of intro patterns but also of
+   simple intro patterns *)
+
+Ltac exploit_main t T pat cleanup
+  :=
+  (lazymatch T with
+   | ?U1 -> ?U2 =>
+       let H := fresh
+       in
+idtac "H=" H;
+         assert U1 as H;
+         [cleanup () | exploit_main (t H) U2 pat ltac:(fun _ => clear H; cleanup ())]
+   | _ =>
+       pose proof t as pat;
+       cleanup ()
+   end).
+
+Tactic Notation "exploit" constr(t) "as" simple_intropattern(pat)
+  :=
+  exploit_main t ltac:(type of t) pat ltac:(fun _ => idtac).
+
+Goal (True -> True) -> True.
+intro H0. exploit H0 as H.
+Abort.
+
+Tactic Notation "exploit'" constr(t) "as" intropattern(pat)
+  :=
+  exploit_main t ltac:(type of t) pat ltac:(fun _ => idtac).
+
+Goal (True -> True) -> True.
+intro H0. exploit' H0 as H.
+Abort.
diff --git a/test-suite/bugs/closed/bug_10888.v b/test-suite/bugs/closed/bug_10888.v
new file mode 100644
index 0000000000..3c2e8011d7
--- /dev/null
+++ b/test-suite/bugs/closed/bug_10888.v
@@ -0,0 +1,11 @@
+
+Module Type T.
+Context {A:Type}.
+End T.
+
+Module M(X:T).
+  Import X.
+  Check X.A.
+  Check A.
+  Definition B := A.
+End M.
diff --git a/test-suite/bugs/closed/bug_9512.v b/test-suite/bugs/closed/bug_9512.v
new file mode 100644
index 0000000000..25285622a9
--- /dev/null
+++ b/test-suite/bugs/closed/bug_9512.v
@@ -0,0 +1,35 @@
+Require Import Coq.ZArith.BinInt Coq.omega.Omega Coq.micromega.Lia.
+
+Set Primitive Projections.
+Record params := { width : Z }.
+Definition p : params := Build_params 64.
+
+Set Printing All.
+
+Goal width p = 0%Z -> width p = 0%Z.
+  intros.
+
+  assert_succeeds (enough True; [omega|]).
+  assert_succeeds (enough True; [lia|]).
+
+(*   H : @eq Z (width p) Z0 *)
+(*   ============================ *)
+(*   @eq Z (width p) Z0 *)
+
+  change tt with tt in H.
+
+(*   H : @eq Z (width p) Z0 *)
+(*   ============================ *)
+(*   @eq Z (width p) Z0 *)
+
+  assert_succeeds (enough True; [lia|]).
+  (* Tactic failure: <tactic closure> fails. *)
+  (* assert_succeeds (enough True; [omega|]). *)
+  (* Tactic failure: <tactic closure> fails. *)
+
+  (* omega. *)
+  (* Error: Omega can't solve this system *)
+
+  lia.
+  (* Tactic failure:  Cannot find witness. *)
+Qed.
diff --git a/test-suite/bugs/opened/bug_1596.v b/test-suite/bugs/opened/bug_1596.v
index 820022d995..27cb731151 100644
--- a/test-suite/bugs/opened/bug_1596.v
+++ b/test-suite/bugs/opened/bug_1596.v
@@ -69,9 +69,8 @@ Definition t := (X.t * Y.t)%type.
     elim (X.lt_not_eq H2 H3).
     elim H0;clear H0;intros.
     right.
-    split.
-    eauto.
-    eauto.
+    split;
+    eauto with ordered_type.
   Qed.
 
   Lemma lt_not_eq : forall (x y:t),(lt x y)->~(eq x y).
@@ -97,7 +96,7 @@ Definition t := (X.t * Y.t)%type.
     apply EQ.
     split;trivial.
     apply GT.
-    right;auto.
+    right;auto with ordered_type.
     apply GT.
     left;trivial.
   Defined.
diff --git a/test-suite/ltac2/constr.v b/test-suite/ltac2/constr.v
new file mode 100644
index 0000000000..39601d99a8
--- /dev/null
+++ b/test-suite/ltac2/constr.v
@@ -0,0 +1,12 @@
+Require Import Ltac2.Constr Ltac2.Init Ltac2.Control.
+Import Unsafe.
+
+Ltac2 Eval match (kind '(nat -> bool)) with
+           | Prod a b c => a
+           | _ => throw Match_failure end.
+
+Set Allow StrictProp.
+Axiom something : SProp.
+Ltac2 Eval match (kind '(forall x : something, bool)) with
+           | Prod a b c => a
+           | _ => throw Match_failure end.
diff --git a/test-suite/micromega/bug_9162.v b/test-suite/micromega/bug_9162.v
new file mode 100644
index 0000000000..4aedf57faf
--- /dev/null
+++ b/test-suite/micromega/bug_9162.v
@@ -0,0 +1,8 @@
+Require Import ZArith Lia.
+Local Open Scope Z_scope.
+
+Goal Z.of_N (Z.to_N 0) = 0.
+Proof. lia. Qed.
+
+Goal forall q, (Z.of_N (Z.to_N 0) = 0 -> q = 0) -> Z.of_N (Z.to_N 0) = q.
+Proof. lia. Qed.
diff --git a/test-suite/output-coqtop/DependentEvars.out b/test-suite/output-coqtop/DependentEvars.out
new file mode 100644
index 0000000000..9ca3fa3357
--- /dev/null
+++ b/test-suite/output-coqtop/DependentEvars.out
@@ -0,0 +1,91 @@
+
+Coq < 
+Coq < Coq < 1 subgoal
+  
+  ============================
+  forall P Q R : Prop, (Q -> R) -> (P -> Q) -> (P -> Q) -> P -> R
+
+(dependent evars: ; in current goal:)
+
+strange_imp_trans < 
+strange_imp_trans < No more subgoals.
+
+(dependent evars: ; in current goal:)
+
+strange_imp_trans < 
+Coq < Coq < 1 subgoal
+  
+  ============================
+  forall P Q : Prop, (P -> Q) /\ P -> Q
+
+(dependent evars: ; in current goal:)
+
+modpon < 
+modpon < No more subgoals.
+
+(dependent evars: ; in current goal:)
+
+modpon < 
+Coq < Coq < 
+Coq < P1 is declared
+P2 is declared
+P3 is declared
+P4 is declared
+
+Coq < p12 is declared
+
+Coq < p123 is declared
+
+Coq < p34 is declared
+
+Coq < Coq < 1 subgoal
+  
+  P1, P2, P3, P4 : Prop
+  p12 : P1 -> P2
+  p123 : (P1 -> P2) -> P3
+  p34 : P3 -> P4
+  ============================
+  P4
+
+(dependent evars: ; in current goal:)
+
+p14 < 
+p14 < 4 focused subgoals
+(shelved: 2)
+  
+  P1, P2, P3, P4 : Prop
+  p12 : P1 -> P2
+  p123 : (P1 -> P2) -> P3
+  p34 : P3 -> P4
+  ============================
+  ?Q -> P4
+
+subgoal 2 is:
+ ?P -> ?Q
+subgoal 3 is:
+ ?P -> ?Q
+subgoal 4 is:
+ ?P
+
+(dependent evars: ?X4:?P, ?X5:?Q; in current goal: ?X5)
+
+p14 < 3 focused subgoals
+(shelved: 2)
+  
+  P1, P2, P3, P4 : Prop
+  p12 : P1 -> P2
+  p123 : (P1 -> P2) -> P3
+  p34 : P3 -> P4
+  ============================
+  ?P -> (?Goal2 -> P4) /\ ?Goal2
+
+subgoal 2 is:
+ ?P -> (?Goal2 -> P4) /\ ?Goal2
+subgoal 3 is:
+ ?P
+
+(dependent evars: ?X4:?P, ?X5 using ?X10 ?X11, ?X10 using ?X11, ?X11:?Goal2; in current goal: ?X4 ?X5 ?X10 ?X11)
+
+p14 < 
+Coq < 
+Coq < 
diff --git a/test-suite/output-coqtop/DependentEvars.v b/test-suite/output-coqtop/DependentEvars.v
new file mode 100644
index 0000000000..5a59054073
--- /dev/null
+++ b/test-suite/output-coqtop/DependentEvars.v
@@ -0,0 +1,24 @@
+Set Printing Dependent Evars Line.
+Lemma strange_imp_trans :
+  forall P Q R : Prop, (Q -> R) -> (P -> Q) -> (P -> Q) -> P -> R.
+Proof.
+  auto.
+Qed.
+
+Lemma modpon : forall P Q : Prop, (P -> Q) /\ P -> Q.
+Proof.
+  tauto.
+Qed.
+
+Section eex.
+  Variables P1 P2 P3 P4 : Prop.
+  Hypothesis p12 : P1 -> P2.
+  Hypothesis p123 : (P1 -> P2) -> P3.
+  Hypothesis p34 : P3 -> P4.
+
+  Lemma p14 : P4.
+  Proof.
+    eapply strange_imp_trans.
+          apply modpon.
+  Abort.
+End eex.
diff --git a/test-suite/output-coqtop/DependentEvars2.out b/test-suite/output-coqtop/DependentEvars2.out
new file mode 100644
index 0000000000..29ebba7c86
--- /dev/null
+++ b/test-suite/output-coqtop/DependentEvars2.out
@@ -0,0 +1,120 @@
+
+Coq < 
+Coq < Coq < 1 subgoal
+  
+  ============================
+  forall P Q R : Prop, (Q -> R) -> (P -> Q) -> (P -> Q) -> P -> R
+
+(dependent evars: ; in current goal:)
+
+strange_imp_trans < 
+strange_imp_trans < No more subgoals.
+
+(dependent evars: ; in current goal:)
+
+strange_imp_trans < 
+Coq < Coq < 1 subgoal
+  
+  ============================
+  forall P Q : Prop, (P -> Q) /\ P -> Q
+
+(dependent evars: ; in current goal:)
+
+modpon < 
+modpon < No more subgoals.
+
+(dependent evars: ; in current goal:)
+
+modpon < 
+Coq < Coq < 
+Coq < P1 is declared
+P2 is declared
+P3 is declared
+P4 is declared
+
+Coq < p12 is declared
+
+Coq < p123 is declared
+
+Coq < p34 is declared
+
+Coq < Coq < 1 subgoal
+  
+  P1, P2, P3, P4 : Prop
+  p12 : P1 -> P2
+  p123 : (P1 -> P2) -> P3
+  p34 : P3 -> P4
+  ============================
+  P4
+
+(dependent evars: ; in current goal:)
+
+p14 < 
+p14 < Second proof:
+
+p14 < 4 focused subgoals
+(shelved: 2)
+  
+  P1, P2, P3, P4 : Prop
+  p12 : P1 -> P2
+  p123 : (P1 -> P2) -> P3
+  p34 : P3 -> P4
+  ============================
+  ?Q -> P4
+
+subgoal 2 is:
+ ?P -> ?Q
+subgoal 3 is:
+ ?P -> ?Q
+subgoal 4 is:
+ ?P
+
+(dependent evars: ?X4:?P, ?X5:?Q; in current goal: ?X5)
+
+p14 < 1 focused subgoal
+(shelved: 2)
+  
+  P1, P2, P3, P4 : Prop
+  p12 : P1 -> P2
+  p123 : (P1 -> P2) -> P3
+  p34 : P3 -> P4
+  ============================
+  ?Q -> P4
+
+(dependent evars: ?X4:?P, ?X5:?Q; in current goal: ?X5)
+
+p14 < This subproof is complete, but there are some unfocused goals.
+Try unfocusing with "}".
+
+3 subgoals
+(shelved: 2)
+
+subgoal 1 is:
+ ?P -> (?Goal2 -> P4) /\ ?Goal2
+subgoal 2 is:
+ ?P -> (?Goal2 -> P4) /\ ?Goal2
+subgoal 3 is:
+ ?P
+
+(dependent evars: ?X4:?P, ?X5 using ?X10 ?X11, ?X10 using ?X11, ?X11:?Goal2; in current goal:)
+
+p14 < 3 focused subgoals
+(shelved: 2)
+  
+  P1, P2, P3, P4 : Prop
+  p12 : P1 -> P2
+  p123 : (P1 -> P2) -> P3
+  p34 : P3 -> P4
+  ============================
+  ?P -> (?Goal2 -> P4) /\ ?Goal2
+
+subgoal 2 is:
+ ?P -> (?Goal2 -> P4) /\ ?Goal2
+subgoal 3 is:
+ ?P
+
+(dependent evars: ?X4:?P, ?X5 using ?X10 ?X11, ?X10 using ?X11, ?X11:?Goal2; in current goal: ?X4 ?X5 ?X10 ?X11)
+
+p14 < 
+Coq < 
+Coq < 
diff --git a/test-suite/output-coqtop/DependentEvars2.v b/test-suite/output-coqtop/DependentEvars2.v
new file mode 100644
index 0000000000..d0f3a4012e
--- /dev/null
+++ b/test-suite/output-coqtop/DependentEvars2.v
@@ -0,0 +1,27 @@
+Set Printing Dependent Evars Line.
+Lemma strange_imp_trans :
+  forall P Q R : Prop, (Q -> R) -> (P -> Q) -> (P -> Q) -> P -> R.
+Proof.
+  auto.
+Qed.
+
+Lemma modpon : forall P Q : Prop, (P -> Q) /\ P -> Q.
+Proof.
+  tauto.
+Qed.
+
+Section eex.
+  Variables P1 P2 P3 P4 : Prop.
+  Hypothesis p12 : P1 -> P2.
+  Hypothesis p123 : (P1 -> P2) -> P3.
+  Hypothesis p34 : P3 -> P4.
+
+  Lemma p14 : P4.
+  Proof.
+    idtac "Second proof:".
+    eapply strange_imp_trans.
+          {
+            apply modpon.
+          }
+  Abort.
+End eex.
diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out
index a89fd64999..d48d8b900f 100644
--- a/test-suite/output/UnivBinders.out
+++ b/test-suite/output/UnivBinders.out
@@ -38,10 +38,10 @@ Argument scopes are [type_scope _]
 bar@{u} = nat
      : Wrap@{u} Set
 (* u |= Set < u *)
-foo@{u UnivBinders.17 v} = 
-Type@{UnivBinders.17} -> Type@{v} -> Type@{u}
-     : Type@{max(u+1,UnivBinders.17+1,v+1)}
-(* u UnivBinders.17 v |=  *)
+foo@{u UnivBinders.18 v} = 
+Type@{UnivBinders.18} -> Type@{v} -> Type@{u}
+     : Type@{max(u+1,UnivBinders.18+1,v+1)}
+(* u UnivBinders.18 v |=  *)
 Type@{i} -> Type@{j}
      : Type@{max(i+1,j+1)}
 (* {j i} |=  *)
@@ -68,19 +68,19 @@ mono
 The command has indeed failed with message:
 Universe u already exists.
 bobmorane = 
-let tt := Type@{UnivBinders.33} in
-let ff := Type@{UnivBinders.35} in tt -> ff
-     : Type@{max(UnivBinders.32,UnivBinders.34)}
+let tt := Type@{UnivBinders.34} in
+let ff := Type@{UnivBinders.36} in tt -> ff
+     : Type@{max(UnivBinders.33,UnivBinders.35)}
 The command has indeed failed with message:
 Universe u already bound.
 foo@{E M N} = 
 Type@{M} -> Type@{N} -> Type@{E}
      : Type@{max(E+1,M+1,N+1)}
 (* E M N |=  *)
-foo@{u UnivBinders.17 v} = 
-Type@{UnivBinders.17} -> Type@{v} -> Type@{u}
-     : Type@{max(u+1,UnivBinders.17+1,v+1)}
-(* u UnivBinders.17 v |=  *)
+foo@{u UnivBinders.18 v} = 
+Type@{UnivBinders.18} -> Type@{v} -> Type@{u}
+     : Type@{max(u+1,UnivBinders.18+1,v+1)}
+(* u UnivBinders.18 v |=  *)
 Inductive Empty@{E} : Type@{E} :=  
 (* E |=  *)
 Record PWrap (A : Type@{E}) : Type@{E} := pwrap { punwrap : A }
@@ -143,26 +143,26 @@ Applied.infunct@{u v} =
 inmod@{u} -> Type@{v}
      : Type@{max(u+1,v+1)}
 (* u v |=  *)
-axfoo@{i UnivBinders.57 UnivBinders.58} :
-Type@{UnivBinders.57} -> Type@{i}
-(* i UnivBinders.57 UnivBinders.58 |=  *)
+axfoo@{i UnivBinders.59 UnivBinders.60} :
+Type@{UnivBinders.59} -> Type@{i}
+(* i UnivBinders.59 UnivBinders.60 |=  *)
 
 axfoo is universe polymorphic
 Argument scope is [type_scope]
 Expands to: Constant UnivBinders.axfoo
-axbar@{i UnivBinders.57 UnivBinders.58} :
-Type@{UnivBinders.58} -> Type@{i}
-(* i UnivBinders.57 UnivBinders.58 |=  *)
+axbar@{i UnivBinders.59 UnivBinders.60} :
+Type@{UnivBinders.60} -> Type@{i}
+(* i UnivBinders.59 UnivBinders.60 |=  *)
 
 axbar is universe polymorphic
 Argument scope is [type_scope]
 Expands to: Constant UnivBinders.axbar
-axfoo' : Type@{axbar'.u0} -> Type@{axbar'.i}
+axfoo' : Type@{axfoo'.u0} -> Type@{axfoo'.i}
 
 axfoo' is not universe polymorphic
 Argument scope is [type_scope]
 Expands to: Constant UnivBinders.axfoo'
-axbar' : Type@{axbar'.u0} -> Type@{axbar'.i}
+axbar' : Type@{axfoo'.u0} -> Type@{axfoo'.i}
 
 axbar' is not universe polymorphic
 Argument scope is [type_scope]
diff --git a/test-suite/prerequisite/ssr_mini_mathcomp.v b/test-suite/prerequisite/ssr_mini_mathcomp.v
index 74f94a9bed..d293dc0533 100644
--- a/test-suite/prerequisite/ssr_mini_mathcomp.v
+++ b/test-suite/prerequisite/ssr_mini_mathcomp.v
@@ -196,7 +196,7 @@ Definition clone_subType U v :=
 
 Variable sT : subType.
 
-CoInductive Sub_spec : sT -> Type := SubSpec x Px : Sub_spec (Sub x Px).
+Variant Sub_spec : sT -> Type := SubSpec x Px : Sub_spec (Sub x Px).
 
 Lemma SubP u : Sub_spec u.
 Proof. by case: sT Sub_spec SubSpec u => T' _ C rec /= _. Qed.
@@ -209,7 +209,7 @@ Definition insub x :=
 
 Definition insubd u0 x := odflt u0 (insub x).
 
-CoInductive insub_spec x : option sT -> Type :=
+Variant insub_spec x : option sT -> Type :=
   | InsubSome u of P x & val u = x : insub_spec x (Some u)
   | InsubNone   of ~~ P x          : insub_spec x None.
 
@@ -568,7 +568,7 @@ Fixpoint nth s n {struct n} :=
 
 Fixpoint rcons s z := if s is x :: s' then x :: rcons s' z else [:: z].
 
-CoInductive last_spec : seq T -> Type :=
+Variant last_spec : seq T -> Type :=
   | LastNil        : last_spec [::]
   | LastRcons s x  : last_spec (rcons s x).
 
@@ -1292,7 +1292,7 @@ Open Scope big_scope.
 (* packages both in in a term in which i occurs; it also depends on the       *)
 (* iterated <op>, as this can give more information on the expected type of   *)
 (* the <general_term>, thus allowing for the insertion of coercions.          *)
-CoInductive bigbody R I := BigBody of I & (R -> R -> R) & bool & R.
+Variant bigbody R I := BigBody of I & (R -> R -> R) & bool & R.
 
 Definition applybig {R I} (body : bigbody R I) x :=
   let: BigBody _ op b v := body in if b then op v x else x.
diff --git a/test-suite/success/CompatCurrentFlag.v b/test-suite/success/CompatCurrentFlag.v
index 81469d79c3..fd6101bf89 100644
--- a/test-suite/success/CompatCurrentFlag.v
+++ b/test-suite/success/CompatCurrentFlag.v
@@ -1,3 +1,3 @@
-(* -*- coq-prog-args: ("-compat" "8.10") -*- *)
+(* -*- coq-prog-args: ("-compat" "8.11") -*- *)
 (** Check that the current compatibility flag actually requires the relevant modules. *)
-Import Coq.Compat.Coq810.
+Import Coq.Compat.Coq811.
diff --git a/test-suite/success/CompatOldFlag.v b/test-suite/success/CompatOldFlag.v
index afeb57f9f2..f774cef44f 100644
--- a/test-suite/success/CompatOldFlag.v
+++ b/test-suite/success/CompatOldFlag.v
@@ -1,5 +1,5 @@
-(* -*- coq-prog-args: ("-compat" "8.8") -*- *)
+(* -*- coq-prog-args: ("-compat" "8.9") -*- *)
 (** Check that the current-minus-two compatibility flag actually requires the relevant modules. *)
+Import Coq.Compat.Coq811.
 Import Coq.Compat.Coq810.
 Import Coq.Compat.Coq89.
-Import Coq.Compat.Coq88.
diff --git a/test-suite/success/CompatOldOldFlag.v b/test-suite/success/CompatOldOldFlag.v
new file mode 100644
index 0000000000..20eef955b4
--- /dev/null
+++ b/test-suite/success/CompatOldOldFlag.v
@@ -0,0 +1,6 @@
+(* -*- coq-prog-args: ("-compat" "8.8") -*- *)
+(** Check that the current-minus-three compatibility flag actually requires the relevant modules. *)
+Import Coq.Compat.Coq811.
+Import Coq.Compat.Coq810.
+Import Coq.Compat.Coq89.
+Import Coq.Compat.Coq88.
diff --git a/test-suite/success/CompatPreviousFlag.v b/test-suite/success/CompatPreviousFlag.v
index c8f75915c8..1c5ccc1a92 100644
--- a/test-suite/success/CompatPreviousFlag.v
+++ b/test-suite/success/CompatPreviousFlag.v
@@ -1,4 +1,4 @@
-(* -*- coq-prog-args: ("-compat" "8.9") -*- *)
+(* -*- coq-prog-args: ("-compat" "8.10") -*- *)
 (** Check that the current-minus-one compatibility flag actually requires the relevant modules. *)
+Import Coq.Compat.Coq811.
 Import Coq.Compat.Coq810.
-Import Coq.Compat.Coq89.
diff --git a/test-suite/success/section_poly.v b/test-suite/success/section_poly.v
new file mode 100644
index 0000000000..1e2201f2de
--- /dev/null
+++ b/test-suite/success/section_poly.v
@@ -0,0 +1,74 @@
+
+
+Section Foo.
+
+  Variable X : Type.
+
+  Polymorphic Section Bar.
+
+  Variable A : Type.
+
+  Definition id (a:A) := a.
+
+End Bar.
+Check id@{_}.
+End Foo.
+Check id@{_}.
+
+Polymorphic Section Foo.
+Variable A : Type.
+Section Bar.
+  Variable B : Type.
+
+  Inductive prod := Prod : A -> B -> prod.
+End Bar.
+Check prod@{_}.
+End Foo.
+Check prod@{_ _}.
+
+Section Foo.
+
+  Universe K.
+  Inductive bla := Bla : Type@{K} -> bla.
+
+  Polymorphic Definition bli@{j} := Type@{j} -> bla.
+
+  Definition bloo := bli@{_}.
+
+  Polymorphic Universe i.
+
+  Fail Definition x := Type.
+  Fail Inductive x : Type := .
+  Polymorphic Definition x := Type.
+  Polymorphic Inductive y : x := .
+
+  Variable A : Type. (* adds a mono univ for the Type, which is unrelated to the others *)
+
+  Fail Variable B : (y : Type@{i}).
+  (* not allowed: mono constraint (about a fresh univ for y) regarding
+  poly univ i *)
+
+  Polymorphic Variable B : Type. (* new polymorphic stuff always OK *)
+
+  Variable C : Type@{i}. (* no new univs so no problems *)
+
+  Polymorphic Definition thing := bloo -> y -> A -> B.
+
+End Foo.
+Check bli@{_}.
+Check bloo@{}.
+
+Check thing@{_ _ _}.
+
+Section Foo.
+
+  Polymorphic Universes i k.
+  Universe j.
+  Fail Constraint i < j.
+  Fail Constraint i < k.
+
+  (* referring to mono univs in poly constraints is OK. *)
+  Polymorphic Constraint i < j. Polymorphic Constraint j < k.
+
+  Polymorphic Definition foo := Type@{j}.
+End Foo.
diff --git a/test-suite/tools/update-compat/run.sh b/test-suite/tools/update-compat/run.sh
index 7ff5571ffb..61273c4f37 100755
--- a/test-suite/tools/update-compat/run.sh
+++ b/test-suite/tools/update-compat/run.sh
@@ -6,4 +6,4 @@ SCRIPT_DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null && pwd )"
 # we assume that the script lives in test-suite/tools/update-compat/,
 # and that update-compat.py lives in dev/tools/
 cd "${SCRIPT_DIR}/../../.."
-dev/tools/update-compat.py --assert-unchanged --release || exit $?
+dev/tools/update-compat.py --assert-unchanged --master || exit $?