2 files changed, 55 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/bug_8785.v b/test-suite/bugs/closed/bug_8785.v
new file mode 100644
index 0000000000..b10569499e
--- /dev/null
+++ b/test-suite/bugs/closed/bug_8785.v
@@ -0,0 +1,44 @@
+Universe u v w.
+Inductive invertible {X:Type@{u}} {Y:Type} (f:X->Y) : Prop := .
+
+Inductive FiniteT : Type -> Prop :=
+  | add_finite: forall T:Type@{v}, FiniteT T -> FiniteT (option T)
+  | bij_finite: forall (X:Type@{w}) (Y:Type) (f:X->Y), FiniteT X ->
+    invertible f -> FiniteT Y.
+
+Set Printing Universes.
+
+Axiom a : False.
+(*
+Constraint v <= u.
+Constraint v <= w.
+*)
+Lemma finite_subtype: forall (X:Type) (P:X->Prop),
+  FiniteT X -> (forall x:X, P x \/ ~ P x) ->
+  FiniteT {x:X | P x}.
+Proof.
+intros.
+induction H.
+
+destruct (H0 None).
+elim a.
+
+pose (g := fun (x:{x:T | P (Some x)}) =>
+  match x return {x:option T | P x} with
+    | exist _ x0 i => exist (fun x:option T => P x) (Some x0) i
+  end).
+apply bij_finite with _ g.
+apply IHFiniteT.
+intro; apply H0.
+elim a.
+
+pose (g := fun (x:{x:X | P (f x)}) =>
+  match x with
+  | exist _ x0 i => exist (fun x:Y => P x) (f x0) i
+  end).
+apply bij_finite with _ g.
+apply IHFiniteT.
+intro; apply H0.
+elim a.
+
+Qed.
diff --git a/test-suite/bugs/closed/bug_8794.v b/test-suite/bugs/closed/bug_8794.v
new file mode 100644
index 0000000000..5ff0b30260
--- /dev/null
+++ b/test-suite/bugs/closed/bug_8794.v
@@ -0,0 +1,11 @@
+(* This used to raise an anomaly in 8.8 *)
+
+Inductive T := Tau (t : T).
+
+Notation idT t := (match t with Tau t => Tau t end).
+
+Lemma match_itree : forall (t : T), t = idT t.
+Proof. destruct t; auto. Qed.
+
+Lemma what (k : unit -> T) : k tt = k tt.
+Proof. rewrite match_itree. Abort.