Merge branch 'v8.6'

6 files changed, 317 insertions, 5 deletions

diff --git a/test-suite/bugs/closed/5180.v b/test-suite/bugs/closed/5180.v
new file mode 100644
index 000000000..261092ee6
--- /dev/null
+++ b/test-suite/bugs/closed/5180.v
@@ -0,0 +1,64 @@
+Universes a b c ω ω'.
+Definition Typeω := Type@{ω}.
+Definition Type2 : Typeω := Type@{c}.
+Definition Type1 : Type2 := Type@{b}.
+Definition Type0 : Type1 := Type@{a}.
+
+Set Universe Polymorphism.
+Set Printing Universes.
+
+Definition Typei' (n : nat)
+  := match n return Type@{ω'} with
+     | 0 => Type0
+     | 1 => Type1
+     | 2 => Type2
+     | _ => Typeω
+     end.
+Definition TypeOfTypei' {n} (x : Typei' n) : Type@{ω'}
+  := match n return Typei' n -> Type@{ω'} with
+     | 0 | 1 | 2 | _ => fun x => x
+     end x.
+Definition Typei (n : nat) : Typei' (S n)
+  := match n return Typei' (S n) with
+     | 0 => Type0
+     | 1 => Type1
+     | _ => Type2
+     end.
+Definition TypeOfTypei {n} (x : TypeOfTypei' (Typei n)) : Type@{ω'}
+  := match n return TypeOfTypei' (Typei n) -> Type@{ω'} with
+     | 0 | 1 | _ => fun x => x
+     end x.
+Check Typei 0 : Typei 1.
+Check Typei 1 : Typei 2.
+
+Definition lift' {n} : TypeOfTypei' (Typei n) -> TypeOfTypei' (Typei (S n))
+  := match n return TypeOfTypei' (Typei n) -> TypeOfTypei' (Typei (S n)) with
+     | 0 | 1 | 2 | _ => fun x => (x : Type)
+     end.
+Definition lift'' {n} : TypeOfTypei' (Typei n) -> TypeOfTypei' (Typei (S n))
+  := match n return TypeOfTypei' (Typei n) -> TypeOfTypei' (Typei (S n)) with
+     | 0 | 1 | 2 | _ => fun x => x
+     end. (* The command has indeed failed with message:
+In environment
+n : nat
+x : TypeOfTypei' (Typei 0)
+The term "x" has type "TypeOfTypei' (Typei 0)" while it is expected to have type
+ "TypeOfTypei' (Typei 1)" (universe inconsistency: Cannot enforce b = a because  a < b).
+ *)
+Check (fun x : TypeOfTypei' (Typei 0) => TypeOfTypei' (Typei 1)).
+
+Definition lift''' {n} : TypeOfTypei' (Typei n) -> TypeOfTypei' (Typei (S n)).
+  refine match n return TypeOfTypei' (Typei n) -> TypeOfTypei' (Typei (S n))  with
+         | 0 | 1 | 2 | _ => fun x => _
+         end.
+  exact x.
+  Undo.
+  (* The command has indeed failed with message:
+In environment
+n : nat
+x : TypeOfTypei' (Typei 0)
+The term "x" has type "TypeOfTypei' (Typei 0)" while it is expected to have type
+ "TypeOfTypei' (Typei 1)" (universe inconsistency: Cannot enforce b = a because  a < b).
+ *)
+  all:compute in *.
+  all:exact x.
\ No newline at end of file
diff --git a/test-suite/bugs/closed/5188.v b/test-suite/bugs/closed/5188.v
new file mode 100644
index 000000000..e29ebfb4e
--- /dev/null
+++ b/test-suite/bugs/closed/5188.v
@@ -0,0 +1,5 @@
+Set Printing All.
+Axiom relation : forall (T : Type), Set.
+Axiom T : forall A (R : relation A), Set.
+Set Printing Universes.
+Parameter (A:_) (R:_) (e:@T A R).
diff --git a/test-suite/bugs/closed/5208.v b/test-suite/bugs/closed/5208.v
new file mode 100644
index 000000000..b7a684a27
--- /dev/null
+++ b/test-suite/bugs/closed/5208.v
@@ -0,0 +1,222 @@
+Require Import Program.
+
+Require Import Coq.Strings.String.
+Require Import Coq.Strings.Ascii.
+Require Import Coq.Numbers.BinNums.
+
+Set Implicit Arguments.
+Set Strict Implicit.
+Set Universe Polymorphism.
+Set Printing Universes.
+
+Local Open Scope positive.
+
+Definition field : Type := positive.
+
+Section poly.
+  Universe U.
+
+  Inductive fields : Type :=
+  | pm_Leaf : fields
+  | pm_Branch : fields -> option Type@{U} -> fields -> fields.
+
+  Definition fields_left (f : fields) : fields :=
+    match f with
+    | pm_Leaf => pm_Leaf
+    | pm_Branch l _ _ => l
+    end.
+
+  Definition fields_right (f : fields) : fields :=
+    match f with
+    | pm_Leaf => pm_Leaf
+    | pm_Branch _ _ r => r
+    end.
+
+  Definition fields_here (f : fields) : option Type@{U} :=
+    match f with
+    | pm_Leaf => None
+    | pm_Branch _ s _ => s
+    end.
+
+  Fixpoint fields_get (p : field) (m : fields) {struct p} : option Type@{U} :=
+    match p with
+      | xH => match m with
+                | pm_Leaf => None
+                | pm_Branch _ x _ => x
+              end
+      | xO p' => fields_get p' match m with
+                               | pm_Leaf => pm_Leaf
+                               | pm_Branch L _ _ => L
+                             end
+      | xI p' => fields_get p' match m with
+                               | pm_Leaf => pm_Leaf
+                               | pm_Branch _ _ R => R
+                             end
+    end.
+
+  Definition fields_leaf : fields := pm_Leaf.
+
+  Inductive member (val : Type@{U}) : fields -> Type :=
+  | pmm_H : forall L R, member val (pm_Branch L (Some val) R)
+  | pmm_L : forall (V : option Type@{U}) L R, member val L -> member val (pm_Branch L V R)
+  | pmm_R : forall (V : option Type@{U}) L R, member val R -> member val (pm_Branch L V R).
+  Arguments pmm_H {_ _ _}.
+  Arguments pmm_L {_ _ _ _} _.
+  Arguments pmm_R {_ _ _ _} _.
+
+  Fixpoint get_member (val : Type@{U}) p {struct p}
+  : forall m, fields_get p m = @Some Type@{U} val -> member val m :=
+    match p as p return forall m, fields_get p m = @Some Type@{U} val -> member@{U} val m with
+      | xH => fun m =>
+        match m as m return fields_get xH m = @Some Type@{U} val -> member@{U} val m with
+        | pm_Leaf => fun pf : None = @Some Type@{U} _ =>
+                       match pf in _ = Z return match Z with
+                                                | Some _ => _
+                                                | None => unit
+                                                end
+                       with
+                       | eq_refl => tt
+                       end
+        | pm_Branch _ None _ => fun pf : None = @Some Type@{U} _ =>
+                                  match pf in _ = Z return match Z with
+                                                           | Some _ => _
+                                                           | None => unit
+                                                           end
+                                  with
+                                  | eq_refl => tt
+                                  end
+        | pm_Branch _ (Some x) _ => fun pf : @Some Type@{U} x = @Some Type@{U} val =>
+                                      match eq_sym pf in _ = Z return member@{U} val (pm_Branch _ Z _) with
+                                      | eq_refl => pmm_H
+                                      end
+        end
+      | xO p' => fun m =>
+        match m as m return fields_get (xO p') m = @Some Type@{U} val -> member@{U} val m with
+        | pm_Leaf => fun pf : fields_get p' pm_Leaf = @Some Type@{U} val =>
+                       @get_member _ p' pm_Leaf pf
+        | pm_Branch l _ _ => fun pf : fields_get p' l = @Some Type@{U} val =>
+                       @pmm_L _ _ _ _ (@get_member _ p' l pf)
+        end
+      | xI p' => fun m =>
+        match m as m return fields_get (xI p') m = @Some Type@{U} val -> member@{U} val m with
+        | pm_Leaf => fun pf : fields_get p' pm_Leaf = @Some Type@{U} val =>
+                       @get_member _ p' pm_Leaf pf
+        | pm_Branch l _ r => fun pf : fields_get p' r = @Some Type@{U} val =>
+                               @pmm_R _ _ _ _ (@get_member _ p' r pf)
+        end
+    end.
+
+  Inductive record : fields -> Type :=
+  | pr_Leaf : record pm_Leaf
+  | pr_Branch : forall L R (V : option Type@{U}),
+      record L ->
+      match V return Type@{U} with
+        | None => unit
+        | Some t => t
+      end ->
+      record R ->
+      record (pm_Branch L V R).
+
+
+  Definition record_left {L} {V : option Type@{U}} {R}
+             (r : record (pm_Branch L V R)) : record L :=
+    match r in record z
+          return match z with
+                 | pm_Branch L _ _ => record L
+                 | _ => unit
+                 end
+    with
+      | pr_Branch _ l _ _ => l
+      | pr_Leaf => tt
+    end.
+Set Printing All.
+  Definition record_at {L} {V : option Type@{U}} {R} (r : record (pm_Branch L V R))
+  : match V return Type@{U} with
+    | None => unit
+    | Some t => t
+    end :=
+    match r in record z
+          return match z (* return ?X *) with
+                 | pm_Branch _ V _ => match V return Type@{U} with
+                                     | None => unit
+                                     | Some t => t
+                                     end
+                 | _ => unit
+                 end
+    with
+      | pr_Branch _ _ v _ => v
+      | pr_Leaf => tt
+    end.
+
+  Definition record_here {L : fields} (v : Type@{U}) {R : fields}
+             (r : record (pm_Branch L (@Some Type@{U} v) R)) : v :=
+    match r in record z
+          return match z return Type@{U} with
+                 | pm_Branch _ (Some v) _ => v
+                 | _ => unit
+                 end
+    with
+      | pr_Branch _ _ v _ => v
+      | pr_Leaf => tt
+    end.
+
+  Definition record_right {L V R} (r : record (pm_Branch L V R)) : record R :=
+    match r in record z return match z with
+                                  | pm_Branch _ _ R => record R
+                                  | _ => unit
+                                end
+    with
+      | pr_Branch _ _ _ r => r
+      | pr_Leaf => tt
+    end.
+
+  Fixpoint record_get {val : Type@{U}} {pm : fields} (m : member val pm) : record pm -> val :=
+    match m in member _ pm return record pm -> val with
+      | pmm_H => fun r => record_here r
+      | pmm_L m' => fun r => record_get m' (record_left r)
+      | pmm_R m' => fun r => record_get m' (record_right r)
+    end.
+
+  Fixpoint record_set {val : Type@{U}} {pm : fields} (m : member val pm) (x : val) {struct m}
+  : record pm -> record pm :=
+    match m in member _ pm return record pm -> record pm with
+    | pmm_H => fun r =>
+      pr_Branch (Some _)
+                (record_left r)
+                x
+                (record_right r)
+    | pmm_L m' => fun r =>
+      pr_Branch _
+                (record_set m' x (record_left r))
+                (record_at r)
+                (record_right r)
+    | pmm_R m' => fun r =>
+      pr_Branch _ (record_left r)
+                (record_at r)
+                (record_set m' x (record_right r))
+    end.
+End poly.
+Axiom cheat : forall {A}, A.
+Lemma record_get_record_set_different:
+  forall (T: Type) (vars: fields)
+    (pmr pmw: member T vars)
+    (diff: pmr <> pmw)
+    (r: record vars) (val: T),
+    record_get pmr (record_set pmw val r) = record_get pmr r.
+Proof.
+  intros.
+  revert pmr diff r val.
+  induction pmw; simpl; intros.
+  - dependent destruction pmr.
+    + congruence.
+    + auto.
+    + auto.
+  - dependent destruction pmr.
+    + auto.
+    + simpl. apply IHpmw. congruence.
+    + auto.
+  - dependent destruction pmr.
+    + auto.
+    + auto.
+    + simpl. apply IHpmw. congruence.
+Qed.
diff --git a/test-suite/output/Tactics.out b/test-suite/output/Tactics.out
index 9949658c4..239edd1da 100644
--- a/test-suite/output/Tactics.out
+++ b/test-suite/output/Tactics.out
@@ -1,4 +1,4 @@
 Ltac f H := split; [ a H | e H ]
 Ltac g := match goal with
-          | |- context [if ?X then _ else _] => case X
+          | |- context [ if ?X then _ else _ ] => case X
           end
diff --git a/test-suite/success/Inductive.v b/test-suite/success/Inductive.v
index 9661b3bfa..f746def5c 100644
--- a/test-suite/success/Inductive.v
+++ b/test-suite/success/Inductive.v
@@ -162,3 +162,24 @@ Inductive L (A:Type) (T:=A) : Type := C : L nat -> L A.
    hit the Inductiveops.get_arity bug mentioned above (see #3491) *)
 
 Inductive IND6 (A:Type) (T:=A) := CONS6 : IND6 T -> IND6 A.
+
+
+Module TemplateProp.
+
+  (** Check lowering of a template universe polymorphic inductive to Prop *)
+  
+  Inductive Foo (A : Type) : Type := foo : A -> Foo A.
+  
+  Check Foo True : Prop.
+
+End TemplateProp.
+
+Module PolyNoLowerProp.
+
+  (** Check lowering of a general universe polymorphic inductive to Prop is _failing_ *)
+  
+  Polymorphic Inductive Foo (A : Type) : Type := foo : A -> Foo A.
+  
+  Fail Check Foo True : Prop.
+
+End PolyNoLowerProp.
diff --git a/test-suite/success/Typeclasses.v b/test-suite/success/Typeclasses.v
index f62427ef4..6b1f0315b 100644
--- a/test-suite/success/Typeclasses.v
+++ b/test-suite/success/Typeclasses.v
@@ -98,7 +98,7 @@ Goal exists R, @Refl nat R.
   solve [typeclasses eauto with foo].
 Qed.
 
-(* Set Typeclasses Compatibility "8.5". *)
+Set Typeclasses Compatibility "8.5".
 Parameter f : nat -> Prop.
 Parameter g : nat -> nat -> Prop.
 Parameter h : nat -> nat -> nat -> Prop.
@@ -108,8 +108,7 @@ Axiom c : forall x y z, h x y z -> f x -> f y.
 Hint Resolve a b c : mybase.
 Goal forall x y z, h x y z -> f x -> f y.
   intros.
-  Set Typeclasses Debug.
-  typeclasses eauto with mybase.
+  Fail Timeout 1 typeclasses eauto with mybase. (* Loops now *)
   Unshelve.
 Abort.
 End bt.
@@ -138,7 +137,8 @@ Notation "'return' t" := (unit t).
 Class A `(e: T) := { a := True }.
 Class B `(e_: T) := { e := e_; sg_ass :> A e }.
 
-Set Typeclasses Debug.
+(* Set Typeclasses Debug. *)
+(* Set Typeclasses Debug Verbosity 2. *)
 
 Goal forall `{B T}, Prop.
   intros. apply a.