Add a bunch of reproduction files for bugs.

22 files changed, 493 insertions, 0 deletions

diff --git a/test-suite/bugs/opened/2951.v b/test-suite/bugs/opened/2951.v
new file mode 100644
index 000000000..3739247b6
--- /dev/null
+++ b/test-suite/bugs/opened/2951.v
@@ -0,0 +1 @@
+Class C (A: Type) : Type := { f: A }.
diff --git a/test-suite/bugs/opened/3010.v-disabled b/test-suite/bugs/opened/3010.v-disabled
new file mode 100644
index 000000000..f2906bd6a
--- /dev/null
+++ b/test-suite/bugs/opened/3010.v-disabled
@@ -0,0 +1 @@
+Definition em {A R} (k : forall s : sum A _, match s with inl x => R x | inr y => R end) := k (inr (fun x => k (inl x))).
\ No newline at end of file
diff --git a/test-suite/bugs/opened/3045.v b/test-suite/bugs/opened/3045.v
new file mode 100644
index 000000000..b7f40b4ad
--- /dev/null
+++ b/test-suite/bugs/opened/3045.v
@@ -0,0 +1,30 @@
+Set Asymmetric Patterns.
+Generalizable All Variables.
+Set Implicit Arguments.
+Set Universe Polymorphism.
+
+Record SpecializedCategory (obj : Type) :=
+  {
+    Object :> _ := obj;
+    Morphism : obj -> obj -> Type;
+
+    Compose : forall s d d', Morphism d d' -> Morphism s d -> Morphism s d'
+  }.
+
+Arguments Compose {obj} [C s d d'] m1 m2 : rename.
+
+Inductive ReifiedMorphism : forall objC (C : SpecializedCategory objC), C -> C -> Type :=
+| ReifiedComposedMorphism : forall objC C s d d', ReifiedMorphism C d d' -> ReifiedMorphism C s d -> @ReifiedMorphism objC C s d'.
+
+Fixpoint ReifiedMorphismDenote objC C s d (m : @ReifiedMorphism objC C s d) : Morphism C s d :=
+  match m in @ReifiedMorphism objC C s d return Morphism C s d with
+    | ReifiedComposedMorphism _ _ _ _ _ m1 m2 => Compose (@ReifiedMorphismDenote _ _ _ _ m1)
+                                                         (@ReifiedMorphismDenote _ _ _ _ m2)
+  end.
+
+Fixpoint ReifiedMorphismSimplifyWithProof objC C s d (m : @ReifiedMorphism objC C s d)
+: { m' : ReifiedMorphism C s d | ReifiedMorphismDenote m = ReifiedMorphismDenote m' }.
+refine match m with
+         | ReifiedComposedMorphism _ _ s0 d0 d0' m1 m2 => _
+       end; clear m.
+Fail destruct (@ReifiedMorphismSimplifyWithProof _ _ _ _ m1) as [ [] ? ].
diff --git a/test-suite/bugs/opened/3068.v b/test-suite/bugs/opened/3068.v
new file mode 100644
index 000000000..5d3bc0cbc
--- /dev/null
+++ b/test-suite/bugs/opened/3068.v
@@ -0,0 +1,60 @@
+Section Counted_list.
+
+  Variable A : Type.
+
+  Inductive counted_list : nat -> Type :=
+    | counted_nil : counted_list 0
+    | counted_cons : forall(n : nat), 
+        A -> counted_list n -> counted_list (S n).
+
+
+  Fixpoint counted_def_nth{n : nat}(l : counted_list n)
+                          (i : nat)(def : A) : A :=
+    match i with
+      | 0 => match l with
+               | counted_nil => def
+               | counted_cons _ a _ => a
+             end
+      | S i => match l with
+                 | counted_nil => def
+                 | counted_cons _ _ tl => counted_def_nth tl i def
+               end
+    end.
+
+
+  Lemma counted_list_equal_nth_char : 
+    forall(n : nat)(l1 l2 : counted_list n)(def : A),
+      (forall(i : nat), counted_def_nth l1 i def = counted_def_nth l2 i def) ->
+        l1 = l2.
+  Proof.
+    admit.
+  Qed.
+
+End Counted_list.
+
+Implicit Arguments counted_def_nth [A n].
+
+Section Finite_nat_set.
+
+  Variable set_size : nat.
+
+  Definition fnat_subset : Type := counted_list bool set_size.
+
+  Definition fnat_member(fs : fnat_subset)(n : nat) : Prop := 
+    is_true (counted_def_nth fs n false).
+
+
+  Lemma fnat_subset_member_eq : forall(fs1 fs2 : fnat_subset),
+    fs1 = fs2 <->
+      forall(n : nat), fnat_member fs1 n <-> fnat_member fs2 n.
+
+  Proof.
+    intros fs1 fs2.
+    split.
+      intros H n.
+      subst fs1.
+      apply iff_refl.
+    intros H.
+    eapply counted_list_equal_nth_char.
+    intros i.
+    Fail destruct (counted_def_nth fs1 i _ ) eqn:H0.
diff --git a/test-suite/bugs/opened/3071.v b/test-suite/bugs/opened/3071.v
new file mode 100644
index 000000000..611ac6065
--- /dev/null
+++ b/test-suite/bugs/opened/3071.v
@@ -0,0 +1,5 @@
+Definition foo := True.
+
+Section foo.
+  Global Arguments foo / .
+Fail End foo.
diff --git a/test-suite/bugs/opened/3092.v b/test-suite/bugs/opened/3092.v
new file mode 100644
index 000000000..9db21d156
--- /dev/null
+++ b/test-suite/bugs/opened/3092.v
@@ -0,0 +1,9 @@
+Fail Fixpoint le_pred (n1 n2 : nat) (H1 : n1 <= n2) : pred n1 <= pred n2 :=
+  match H1 with
+  | le_n      => le_n (pred _)
+  | le_S _ H2 =>
+    match n2 with
+    | 0   => fun H3 => H3
+    | S _ => le_S _ _
+    end (le_pred _ _ H2)
+  end.
diff --git a/test-suite/bugs/opened/3100.v b/test-suite/bugs/opened/3100.v
new file mode 100644
index 000000000..6f35a74dc
--- /dev/null
+++ b/test-suite/bugs/opened/3100.v
@@ -0,0 +1,9 @@
+Fixpoint F (n : nat) (A : Type) : Type :=
+  match n with
+  | 0 => True
+  | S n => forall (x : A), F n (x = x)
+  end.
+
+Goal forall A n, (forall (x : A) (e : x = x), F n (e = e)).
+intros A n.
+Fail change (forall x, F n (x = x)) with (F (S n)).
diff --git a/test-suite/bugs/opened/3166.v b/test-suite/bugs/opened/3166.v
new file mode 100644
index 000000000..e1c29a954
--- /dev/null
+++ b/test-suite/bugs/opened/3166.v
@@ -0,0 +1,83 @@
+Set Asymmetric Patterns.
+
+Section eq.
+  Let A := { X : Type & X }.
+  Let B := (fun x : A => projT1 x).
+  Let T := (fun (a' : A) (b' : B a') => projT2 a' = b').
+  Let T' := T.
+  Let t1T := (fun _ : A => unit).
+  Let f1 := (fun x (_ : t1T x) => projT2 x).
+  Let t1 := (fun x (y : t1T x) => @eq_refl (projT1 x) (projT2 x)).
+  Let t1T' := t1T.
+  Let f1' := f1.
+  Let t1' := t1.
+
+  Theorem eq_matches_commute
+          a' b' (t' : T a' b')
+          (rta : forall b'', T' a' b'' -> A)
+          (rtb : forall b'' t'', B (rta b'' t''))
+          (rt1 : forall y, T _ (rtb (f1' a' y) (@t1' a' y)))
+          (R : forall (b : B (rta b' t')), T _ b -> Type)
+          (r1 : forall y, R (f1 _ y) (@t1 _ y))
+  : match
+      match t' as t0' in (@eq _ _ b0') return T (rta b0' t0') (rtb b0' t0') with
+        | eq_refl => rt1 tt
+      end
+      as t0 in (@eq _ _ b0)
+      return R b0 t0
+    with
+      | eq_refl => r1 tt
+    end
+    =
+    match t'
+          as t0' in (@eq _ _ b0')
+          return (forall (R : forall (b : B (rta b0' t0')), T _ b -> Type)
+                         (r1 : forall y, R (f1 _ y) (@t1 _ y)),
+                    R _ (match t0' as t0'0 in (@eq _ _ b0'0) return T (rta b0'0 t0'0) (rtb b0'0 t0'0) with
+                           | eq_refl => rt1 tt
+                         end))
+    with
+      | eq_refl => fun _ r1 =>
+                      match rt1 tt with
+                        | eq_refl => r1 tt
+                      end
+    end R r1.
+  Proof.
+    destruct t'; reflexivity.
+  Defined.
+
+  Theorem eq_match_beta2
+          a b (t : T a b)
+          X
+          (R : forall b' (t' : T a b'), X b' -> Type)
+          (r1 : forall y x, R _ (@t1 _ y) x)
+          x
+  : match t as t' in (@eq _ _ b') return forall x, R b' t' x with
+      | eq_refl => r1 tt
+    end (x b)
+    =
+    match t as t' in (@eq _ _ b') return R b' t' (x b') with
+      | eq_refl => r1 tt (x _)
+    end.
+  Proof.
+    destruct t; reflexivity.
+  Defined.
+End eq.
+
+Definition typeof {T} (_ : T) := T.
+
+Eval compute in (eq_sym (eq_sym _)).
+Goal forall T (x y : T) (p : x = y), True.
+  intros.
+  pose proof
+       (@eq_matches_commute
+          (existT (fun T => T) T x) y p
+          (fun b'' _ => existT (fun T => T) T b'')
+          (fun _ _ => x)
+          (fun _ => eq_refl)
+          (fun x' _ => x' = y)
+          (fun _ => eq_refl)
+        ) as H0.
+  compute in H0.
+  change (fun (x' : T) (_ : y = x') => x' = y) with ((fun y => fun (x' : T) (_ : y = x') => x' = y) y) in H0.
+  Fail pose proof (fun k => @eq_trans _ _ _ k H0).
diff --git a/test-suite/bugs/opened/3186.v-disabled b/test-suite/bugs/opened/3186.v-disabled
new file mode 100644
index 000000000..d0bcb920c
--- /dev/null
+++ b/test-suite/bugs/opened/3186.v-disabled
@@ -0,0 +1,4 @@
+Fixpoint a (_:unit):=
+match eq_refl with
+|eq_refl => a
+end.
\ No newline at end of file
diff --git a/test-suite/bugs/opened/3209.v b/test-suite/bugs/opened/3209.v
new file mode 100644
index 000000000..3203afa13
--- /dev/null
+++ b/test-suite/bugs/opened/3209.v
@@ -0,0 +1,17 @@
+Inductive eqT {A} (x : A) : A -> Type :=
+  reflT : eqT x x.
+Definition Bi_inv (A B : Type) (f : (A -> B)) :=
+  sigT (fun (g : B -> A) =>
+          sigT (fun (h : B -> A) =>
+                  sigT (fun (α : forall b : B, eqT (f (g b)) b) =>
+                          forall a : A, eqT (h (f a)) a))).
+Definition TEquiv (A B : Type) := sigT (fun (f : A -> B) => Bi_inv _ _ f).
+
+Axiom UA : forall (A B : Type), TEquiv (TEquiv A B) (eqT A B).
+Definition idtoeqv {A B} (e : eqT A B) : TEquiv A B :=
+  sigT_rect (fun _ => TEquiv A B)
+            (fun (f : TEquiv A B -> eqT A B) H =>
+               sigT_rect (fun _ => TEquiv A B)
+                         (fun g _ => g e)
+                         H)
+            (UA A B).
diff --git a/test-suite/bugs/opened/3258.v b/test-suite/bugs/opened/3258.v
new file mode 100644
index 000000000..69a543044
--- /dev/null
+++ b/test-suite/bugs/opened/3258.v
@@ -0,0 +1,35 @@
+Require Import Coq.Classes.Morphisms Coq.Classes.RelationClasses Coq.Program.Program Coq.Setoids.Setoid.
+
+Global Set Implicit Arguments.
+
+Hint Extern 0 => apply reflexivity : typeclass_instances.
+
+Inductive Comp : Type -> Type :=
+| Pick : forall A, (A -> Prop) -> Comp A.
+
+Axiom computes_to : forall A, Comp A -> A -> Prop.
+
+Axiom refine : forall {A} (old : Comp A) (new : Comp A), Prop.
+
+Global Instance refine_PreOrder A : PreOrder (@refine A).
+Admitted.
+
+Add Parametric Morphism A
+: (@Pick A)
+    with signature
+    (pointwise_relation _ (flip impl))
+      ==> (@refine A)
+      as refine_flip_impl_Pick.
+  admit.
+Defined.
+Definition remove_forall_eq' A x B (P : A -> B -> Prop) : pointwise_relation _ impl (P x) (fun z => forall y : A, y = x -> P y z).
+  admit.
+Defined.
+Goal forall A B (x : A) (P : _ -> _ -> Prop),
+       refine (Pick (fun n : B => forall y, y = x -> P y n))
+              (Pick (fun n : B => P x n)).
+Proof.
+  intros.
+  setoid_rewrite (@remove_forall_eq' _ _ _ _).
+  Undo.
+  Fail setoid_rewrite (@remove_forall_eq' _ _ _).
diff --git a/test-suite/bugs/opened/3320.v b/test-suite/bugs/opened/3320.v
new file mode 100644
index 000000000..05cf73281
--- /dev/null
+++ b/test-suite/bugs/opened/3320.v
@@ -0,0 +1,4 @@
+Goal forall x : nat, True.
+  fix 1.
+  assumption.
+Fail Qed.
diff --git a/test-suite/bugs/opened/3408.v b/test-suite/bugs/opened/3408.v
new file mode 100644
index 000000000..921f64155
--- /dev/null
+++ b/test-suite/bugs/opened/3408.v
@@ -0,0 +1,163 @@
+Require Import BinPos.
+
+Inductive expr : Type :=
+  Var : nat -> expr
+| App : expr -> expr -> expr
+| Abs : unit -> expr -> expr.
+
+Inductive expr_acc
+: expr -> expr -> Prop :=
+  acc_App_l : forall f a : expr,
+                expr_acc f (App f a)
+| acc_App_r : forall f a : expr,
+                expr_acc a (App f a)
+| acc_Abs : forall (t : unit) (e : expr),
+              expr_acc e (Abs t e).
+
+Theorem wf_expr_acc : well_founded expr_acc.
+Proof.
+  red.
+  refine (fix rec a : Acc expr_acc a :=
+            match a as a return Acc expr_acc a with
+              | Var v => Acc_intro _ (fun y (_H : expr_acc y (Var v)) =>
+                                        match _H in expr_acc z Z
+                                              return match Z return Prop with
+                                                         | Var _ => Acc _ y
+                                                         | _ => True
+                                                       end
+                                        with
+                                          | acc_App_l _ _ => I
+                                          | _ => I
+                                        end)
+              | App f x => Acc_intro _ (fun y (pf : expr_acc y (App f x)) =>
+                                          match pf in expr_acc z Z
+                                                return match Z return Prop with
+                                                         | App a b => f = a -> x = b -> Acc expr_acc z
+                                                         | _ => True
+                                                       end
+                                          with
+                                            | acc_App_l f' x' => fun pf _ => match pf in _ = z return
+                                                                                   Acc expr_acc z
+                                                                             with
+                                                                               | eq_refl => rec f
+                                                                             end
+                                            | acc_App_r f' x' => fun _ pf => match pf in _ = z return
+                                                                                   Acc expr_acc z
+                                                                             with
+                                                                               | eq_refl => rec x
+                                                                             end
+                                            | _ => I
+                                          end eq_refl eq_refl)
+              | Abs t e => Acc_intro _ (fun y (pf : expr_acc y (Abs t e)) =>
+                                          match pf in expr_acc z Z
+                                                return match Z return Prop with
+                                                         | Abs a b => e = b -> Acc expr_acc z
+                                                         | _ => True
+                                                       end
+                                          with
+                                            | acc_Abs f x => fun pf => match pf in _ = z return
+                                                                             Acc expr_acc z
+                                                                       with
+                                                                         | eq_refl => rec e
+                                                                       end
+                                            | _ => I
+                                          end eq_refl)
+            end).
+Defined.
+
+Theorem wf_expr_acc_delay : well_founded expr_acc.
+Proof.
+  red.
+  refine (fix rec a : Acc expr_acc a :=
+            match a as a return Acc expr_acc a with
+              | Var v => Acc_intro _ (fun y (_H : expr_acc y (Var v)) =>
+                                        match _H in expr_acc z Z
+                                              return match Z return Prop with
+                                                         | Var _ => Acc _ y
+                                                         | _ => True
+                                                       end
+                                        with
+                                          | acc_App_l _ _ => I
+                                          | _ => I
+                                        end)
+              | App f x => Acc_intro _ (fun y (pf : expr_acc y (App f x)) =>
+                                          match pf in expr_acc z Z
+                                                return match Z return Prop with
+                                                         | App a b => (unit -> Acc expr_acc a) -> (unit -> Acc expr_acc b) -> Acc expr_acc z
+                                                         | _ => True
+                                                       end
+                                          with
+                                            | acc_App_l f' x' => fun pf _ => pf tt
+                                            | acc_App_r f' x' => fun _ pf => pf tt
+                                            | _ => I
+                                          end (fun _ => rec f) (fun _ => rec x))
+              | Abs t e => Acc_intro _ (fun y (pf : expr_acc y (Abs t e)) =>
+                                          match pf in expr_acc z Z
+                                                return match Z return Prop with
+                                                         | Abs a b => (unit -> Acc expr_acc b) -> Acc expr_acc z
+                                                         | _ => True
+                                                       end
+                                          with
+                                            | acc_Abs f x => fun pf => pf tt
+                                            | _ => I
+                                          end (fun _ => rec e))
+            end); 
+    try solve [ inversion _H ].
+Defined.
+
+Fixpoint build_large (n : nat) : expr :=
+  match n with
+    | 0 => Var 0
+    | S n =>
+      let e := build_large n in
+      App e e
+  end.
+
+Section guard.
+  Context {A : Type} {R : A -> A -> Prop}.
+
+  Fixpoint guard  (n : nat) (wfR : well_founded R) : well_founded R :=
+    match n with
+      | 0 => wfR
+      | S n0 =>
+        fun x : A =>
+          Acc_intro x
+                    (fun (y : A) (_ : R y x) => guard n0 (guard n0 wfR) y)
+    end.
+End guard.
+
+
+Definition sizeF_delay : expr -> positive.
+refine
+  (@Fix expr (expr_acc)
+       (wf_expr_acc_delay)
+       (fun _ => positive)
+       (fun e =>
+          match e as e return (forall l, expr_acc l e -> positive) -> positive with
+            | Var _ => fun _ => 1
+            | App l r => fun rec => @rec l _ + @rec r _
+            | Abs _ e => fun rec => 1 + @rec e _
+          end%positive)).
+eapply acc_App_l.
+eapply acc_App_r.
+eapply acc_Abs.
+Defined.
+
+Definition sizeF_guard : expr -> positive.
+refine
+  (@Fix expr (expr_acc)
+       (guard 5 wf_expr_acc)
+       (fun _ => positive)
+       (fun e =>
+          match e as e return (forall l, expr_acc l e -> positive) -> positive with
+            | Var _ => fun _ => 1
+            | App l r => fun rec => @rec l _ + @rec r _
+            | Abs _ e => fun rec => 1 + @rec e _
+          end%positive)).
+eapply acc_App_l.
+eapply acc_App_r.
+eapply acc_Abs.
+Defined.
+
+Time Eval native_compute in sizeF_delay (build_large 2).
+Fail Time Eval native_compute in sizeF_guard (build_large 2).
diff --git a/test-suite/bugs/opened/3410.v b/test-suite/bugs/opened/3410.v
new file mode 100644
index 000000000..0d259181a
--- /dev/null
+++ b/test-suite/bugs/opened/3410.v
@@ -0,0 +1 @@
+Fail repeat match goal with H:_ |- _ => setoid_rewrite X in H end.
diff --git a/test-suite/bugs/opened/3417.v b/test-suite/bugs/opened/3417.v
new file mode 100644
index 000000000..355fd17ff
--- /dev/null
+++ b/test-suite/bugs/opened/3417.v
@@ -0,0 +1,3 @@
+Goal forall {T}(a b : T), b=a -> {c | c=b}.
+intros T a b H.
+Fail setoid_rewrite H.
diff --git a/test-suite/bugs/opened/3461.v b/test-suite/bugs/opened/3461.v
new file mode 100644
index 000000000..1ca05a743
--- /dev/null
+++ b/test-suite/bugs/opened/3461.v
@@ -0,0 +1,4 @@
+Lemma foo (b : bool) :
+  exists x : nat, x = x.
+Proof.
+eexists; Fail eexact (eq_refl b).
diff --git a/test-suite/bugs/opened/3463.v b/test-suite/bugs/opened/3463.v
new file mode 100644
index 000000000..541db37fb
--- /dev/null
+++ b/test-suite/bugs/opened/3463.v
@@ -0,0 +1,13 @@
+Tactic Notation "test1" open_constr(t) ident(r):=
+  pose t.
+Tactic Notation "test2" constr(r) open_constr(t):=
+  pose t.
+Tactic Notation "test3" open_constr(t) constr(r):=
+  pose t.
+
+Goal True.
+  test1 (1 + _) nat.
+  test2 nat (1 + _).
+  test3 (1 + _) nat.
+  test3 (1 + _ : nat) nat.
+
diff --git a/test-suite/bugs/opened/3467.v b/test-suite/bugs/opened/3467.v
new file mode 100644
index 000000000..900bfc34b
--- /dev/null
+++ b/test-suite/bugs/opened/3467.v
@@ -0,0 +1,6 @@
+Module foo.
+  Notation x := $(exact I)$.
+End foo.
+Module bar.
+  Fail Include foo.
+End bar.
diff --git a/test-suite/bugs/opened/3478.v-disabled b/test-suite/bugs/opened/3478.v-disabled
new file mode 100644
index 000000000..cc926b216
--- /dev/null
+++ b/test-suite/bugs/opened/3478.v-disabled
@@ -0,0 +1,8 @@
+Set Primitive Projections.
+Record foo := { foom :> Type }.
+Canonical Structure default_foo := fun T => {| foom := T |}.
+Record bar T := { bar1 : T }.
+Goal forall (s : foo) (x : foom s), True.
+Proof.
+  intros.
+  Timeout 1 pose (x : bar _) as x'.
\ No newline at end of file
diff --git a/test-suite/bugs/opened/3487.v b/test-suite/bugs/opened/3487.v
new file mode 100644
index 000000000..ba7a5c98f
--- /dev/null
+++ b/test-suite/bugs/opened/3487.v
@@ -0,0 +1,8 @@
+Notation bar := $(exact I)$.
+Notation foo := bar (only parsing).
+Class baz := { x : False }.
+Instance: baz.
+Admitted.
+Definition baz0 := ((_ : baz) = (_ : baz)).
+Definition foo1 := (foo = foo).
+Fail Definition baz1 := prod ((_ : baz) = (_ : baz)) (foo = foo).
diff --git a/test-suite/bugs/opened/3490.v b/test-suite/bugs/opened/3490.v
new file mode 100644
index 000000000..e7a5caa1d
--- /dev/null
+++ b/test-suite/bugs/opened/3490.v
@@ -0,0 +1,27 @@
+Inductive T : Type :=                                                                                        
+| Var : nat -> T                                                                                                 
+| Arr : T -> T -> T.                                                                                             
+
+Inductive Tele : list T -> Type :=                                                                               
+| Tnil  : @Tele nil                                                                                              
+| Tcons : forall ls, forall (t : @Tele ls) (l : T), @Tele (l :: ls). 
+
+Fail Fixpoint TeleD (ls : list T) (t : Tele ls) {struct t}
+   : { x : Type & x -> nat -> Type } :=
+     match t return { x : Type & x -> nat -> Type } with
+       | Tnil => @existT Type (fun x => x -> nat -> Type) unit (fun (_ : unit) (_ : nat) => unit)
+       | Tcons ls t' l =>
+         let (result, get) := TeleD ls t' in
+         @existT Type (fun x => x -> nat -> Type)
+                 { v : result & (fix TD (t : T) {struct t} :=
+                                   match  t with
+                                     | Var n =>
+                                       get v n
+                                     | Arr a b => TD a -> TD b
+                                   end) l }
+                 (fun x n =>
+                    match n return Type with
+                      | 0 => projT2 x
+                      | S n => get (projT1 x) n
+                    end)
+     end.
diff --git a/test-suite/bugs/opened/3491.v b/test-suite/bugs/opened/3491.v
new file mode 100644
index 000000000..9837b0ecb
--- /dev/null
+++ b/test-suite/bugs/opened/3491.v
@@ -0,0 +1,2 @@
+Fail Inductive list (A : Type) (T := A) : Type :=
+    nil : list A | cons : T -> list T -> list A.