3 files changed, 98 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/4622.v b/test-suite/bugs/closed/4622.v
new file mode 100644
index 0000000000..ffa478cb87
--- /dev/null
+++ b/test-suite/bugs/closed/4622.v
@@ -0,0 +1,24 @@
+Set Primitive Projections.
+
+Record foo : Type := bar { x : unit }.
+
+Goal forall t u, bar t = bar u -> t = u.
+Proof.
+  intros.
+  injection H.
+  trivial.
+Qed.
+(* Was: Error: Pattern-matching expression on an object of inductive type foo has invalid information. *)
+
+(** Dependent pattern-matching is ok on this one as it has eta *)
+Definition baz (x : foo) :=
+  match x as x' return x' = x' with
+  | bar u => eq_refl
+  end.
+
+Inductive foo' : Type := bar' {x' : unit; y: foo'}.
+(** Dependent pattern-matching is not ok on this one *)
+Fail Definition baz' (x : foo') :=
+  match x as x' return x' = x' with
+  | bar' u y => eq_refl
+  end.
diff --git a/test-suite/bugs/closed/4873.v b/test-suite/bugs/closed/4873.v
new file mode 100644
index 0000000000..f2f917b4e7
--- /dev/null
+++ b/test-suite/bugs/closed/4873.v
@@ -0,0 +1,72 @@
+Require Import Coq.Classes.Morphisms.
+Require Import Relation_Definitions.
+Require Import Coq.Compat.Coq85.
+
+Fixpoint tuple' T n : Type :=
+  match n with
+  | O => T
+  | S n' => (tuple' T n' * T)%type
+  end.
+
+Definition tuple T n : Type :=
+  match n with
+  | O => unit
+  | S n' => tuple' T n'
+  end.
+
+Fixpoint to_list' {T} (n:nat) {struct n} : tuple' T n -> list T :=
+  match n with
+  | 0 => fun x => (x::nil)%list
+  | S n' => fun xs : tuple' T (S n') => let (xs', x) := xs in (x :: to_list' n' xs')%list
+  end.
+
+Definition to_list {T} (n:nat) : tuple T n -> list T :=
+  match n with
+  | 0 => fun _ => nil
+  | S n' => fun xs : tuple T (S n') => to_list' n' xs
+  end.
+
+Program Fixpoint from_list' {T} (y:T) (n:nat) (xs:list T) : length xs = n -> tuple' T n :=
+  match n return _ with
+  | 0 =>
+    match xs return (length xs = 0 -> tuple' T 0) with
+    | nil => fun _ => y
+    | _ => _ (* impossible *)
+    end
+  | S n' =>
+    match xs return (length xs = S n' -> tuple' T (S n')) with
+    | cons x xs' => fun _ => (from_list' x n' xs' _, y)
+    | _ => _ (* impossible *)
+    end
+  end.
+Goal True.
+  pose from_list'_obligation_3 as e.
+  repeat (let e' := fresh in
+          rename e into e';
+          (pose (e' nat) as e || pose (e' 0) as e || pose (e' nil) as e || pose (e' eq_refl) as e);
+          subst e').
+  progress hnf in e.
+  pose (eq_refl : e = eq_refl).
+  exact I.
+Qed.
+
+Program Definition from_list {T} (n:nat) (xs:list T) : length xs = n -> tuple T n :=
+match n return _ with
+| 0 =>
+    match xs return (length xs = 0 -> tuple T 0) with
+    | nil => fun _ : 0 = 0 => tt
+    | _ => _ (* impossible *)
+    end
+| S n' =>
+    match xs return (length xs = S n' -> tuple T (S n')) with
+    | cons x xs' => fun _ => from_list' x n' xs' _
+    | _ => _ (* impossible *)
+    end
+end.
+
+Lemma to_list_from_list : forall {T} (n:nat) (xs:list T) pf, to_list n (from_list n xs pf) = xs.
+Proof.
+  destruct xs; simpl; intros; subst; auto.
+  generalize dependent t. simpl in *.
+  induction xs; simpl in *; intros; congruence.
+Qed.
+\ No newline at end of file
diff --git a/test-suite/success/primitiveproj.v b/test-suite/success/primitiveproj.v
index b5e6ccd618..2fa7704941 100644
--- a/test-suite/success/primitiveproj.v
+++ b/test-suite/success/primitiveproj.v
@@ -47,7 +47,9 @@ Check _.(next) : option Y.
 Lemma eta_ind (y : Y) : y = Build_Y y.(next).
 Proof. Fail reflexivity. Abort.
 
+Inductive Fdef := { Fa : nat ; Fb := Fa; Fc : Fdef }.
 
+Fail Scheme Fdef_rec := Induction for Fdef Sort Prop.
 
 (* 
   Rules for parsing and printing of primitive projections and their eta expansions.