14 files changed, 377 insertions, 13 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_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/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/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 d35637d3af..d48d8b900f 100644
--- a/test-suite/output/UnivBinders.out
+++ b/test-suite/output/UnivBinders.out
@@ -157,12 +157,12 @@ Type@{UnivBinders.60} -> Type@{i}
 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/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 $?