9 files changed, 129 insertions, 15 deletions
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/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 $?