summaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/bugs/closed')
-rw-r--r--test-suite/bugs/closed/shouldfail/1898.v5
-rw-r--r--test-suite/bugs/closed/shouldsucceed/121.v2
-rw-r--r--test-suite/bugs/closed/shouldsucceed/1791.v38
-rw-r--r--test-suite/bugs/closed/shouldsucceed/1891.v13
-rw-r--r--test-suite/bugs/closed/shouldsucceed/1900.v8
-rw-r--r--test-suite/bugs/closed/shouldsucceed/1901.v11
-rw-r--r--test-suite/bugs/closed/shouldsucceed/1907.v7
-rw-r--r--test-suite/bugs/closed/shouldsucceed/1918.v377
-rw-r--r--test-suite/bugs/closed/shouldsucceed/1925.v22
-rw-r--r--test-suite/bugs/closed/shouldsucceed/1931.v29
-rw-r--r--test-suite/bugs/closed/shouldsucceed/1935.v21
-rw-r--r--test-suite/bugs/closed/shouldsucceed/1963.v19
-rw-r--r--test-suite/bugs/closed/shouldsucceed/1977.v4
-rw-r--r--test-suite/bugs/closed/shouldsucceed/1981.v5
-rw-r--r--test-suite/bugs/closed/shouldsucceed/2001.v20
-rw-r--r--test-suite/bugs/closed/shouldsucceed/2017.v15
-rw-r--r--test-suite/bugs/closed/shouldsucceed/2021.v23
-rw-r--r--test-suite/bugs/closed/shouldsucceed/2027.v11
18 files changed, 629 insertions, 1 deletions
diff --git a/test-suite/bugs/closed/shouldfail/1898.v b/test-suite/bugs/closed/shouldfail/1898.v
new file mode 100644
index 00000000..92490eb9
--- /dev/null
+++ b/test-suite/bugs/closed/shouldfail/1898.v
@@ -0,0 +1,5 @@
+(* folding should not allow circular dependencies *)
+
+Lemma bug_fold_unfold : True.
+ set (h := 1).
+ fold h in h.
diff --git a/test-suite/bugs/closed/shouldsucceed/121.v b/test-suite/bugs/closed/shouldsucceed/121.v
index d193aa73..8c5a3885 100644
--- a/test-suite/bugs/closed/shouldsucceed/121.v
+++ b/test-suite/bugs/closed/shouldsucceed/121.v
@@ -4,7 +4,7 @@ Section Setoid_Bug.
Variable X:Type -> Type.
Variable Xeq : forall A, (X A) -> (X A) -> Prop.
-Hypothesis Xst : forall A, Equivalence (X A) (Xeq A).
+Hypothesis Xst : forall A, Equivalence (Xeq A).
Variable map : forall A B, (A -> B) -> X A -> X B.
diff --git a/test-suite/bugs/closed/shouldsucceed/1791.v b/test-suite/bugs/closed/shouldsucceed/1791.v
new file mode 100644
index 00000000..694f056e
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1791.v
@@ -0,0 +1,38 @@
+(* simpl performs eta expansion *)
+
+Set Implicit Arguments.
+Require Import List.
+
+Definition k0 := Set.
+Definition k1 := k0 -> k0.
+
+(** iterating X n times *)
+Fixpoint Pow (X:k1)(k:nat){struct k}:k1:=
+ match k with 0 => fun X => X
+ | S k' => fun A => X (Pow X k' A)
+ end.
+
+Parameter Bush: k1.
+Parameter BushToList: forall (A:k0), Bush A -> list A.
+
+Definition BushnToList (n:nat)(A:k0)(t:Pow Bush n A): list A.
+Proof.
+ intros.
+ induction n.
+ exact (t::nil).
+ simpl in t.
+ exact (flat_map IHn (BushToList t)).
+Defined.
+
+Parameter bnil : forall (A:k0), Bush A.
+Axiom BushToList_bnil: forall (A:k0), BushToList (bnil A) = nil(A:=A).
+
+Lemma BushnToList_bnil (n:nat)(A:k0):
+ BushnToList (S n) A (bnil (Pow Bush n A)) = nil.
+Proof.
+ intros.
+ simpl.
+ rewrite BushToList_bnil.
+ simpl.
+ reflexivity.
+Qed.
diff --git a/test-suite/bugs/closed/shouldsucceed/1891.v b/test-suite/bugs/closed/shouldsucceed/1891.v
new file mode 100644
index 00000000..11124cdd
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1891.v
@@ -0,0 +1,13 @@
+(* Check evar-evar unification *)
+ Inductive T (A: Set): Set := mkT: unit -> T A.
+
+ Definition f (A: Set) (l: T A): unit := tt.
+
+ Implicit Arguments f [A].
+
+ Lemma L (x: T unit): (unit -> T unit) -> unit.
+ Proof.
+ refine (fun x => match x return _ with mkT n => fun g => f (g _) end).
+ trivial.
+ Qed.
+
diff --git a/test-suite/bugs/closed/shouldsucceed/1900.v b/test-suite/bugs/closed/shouldsucceed/1900.v
new file mode 100644
index 00000000..cf03efda
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1900.v
@@ -0,0 +1,8 @@
+Parameter A : Type .
+
+Definition eq_A := @eq A.
+
+Goal forall x, eq_A x x.
+intros.
+reflexivity.
+Qed. \ No newline at end of file
diff --git a/test-suite/bugs/closed/shouldsucceed/1901.v b/test-suite/bugs/closed/shouldsucceed/1901.v
new file mode 100644
index 00000000..598db366
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1901.v
@@ -0,0 +1,11 @@
+Require Import Relations.
+
+Record Poset{A:Type}(Le : relation A) : Type :=
+ Build_Poset
+ {
+ Le_refl : forall x : A, Le x x;
+ Le_trans : forall x y z : A, Le x y -> Le y z -> Le x z;
+ Le_antisym : forall x y : A, Le x y -> Le y x -> x = y }.
+
+Definition nat_Poset : Poset Peano.le.
+Admitted. \ No newline at end of file
diff --git a/test-suite/bugs/closed/shouldsucceed/1907.v b/test-suite/bugs/closed/shouldsucceed/1907.v
new file mode 100644
index 00000000..55fc8231
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1907.v
@@ -0,0 +1,7 @@
+(* An example of type inference *)
+
+Axiom A : Type.
+Definition f (x y : A) := x.
+Axiom g : forall x y : A, f x y = y -> Prop.
+Axiom x : A.
+Check (g x _ (refl_equal x)).
diff --git a/test-suite/bugs/closed/shouldsucceed/1918.v b/test-suite/bugs/closed/shouldsucceed/1918.v
new file mode 100644
index 00000000..9d4a3e04
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1918.v
@@ -0,0 +1,377 @@
+(** Occur-check for Meta (up to delta) *)
+
+(** LNMItPredShort.v Version 2.0 July 2008 *)
+(** does not need impredicative Set, runs under V8.2, tested with SVN 11296 *)
+
+(** Copyright Ralph Matthes, I.R.I.T., C.N.R.S. & University of Toulouse*)
+
+
+Set Implicit Arguments.
+
+(** the universe of all monotypes *)
+Definition k0 := Set.
+
+(** the type of all type transformations *)
+Definition k1 := k0 -> k0.
+
+(** the type of all rank-2 type transformations *)
+Definition k2 := k1 -> k1.
+
+(** polymorphic identity *)
+Definition id : forall (A:Set), A -> A := fun A x => x.
+
+(** composition *)
+Definition comp (A B C:Set)(g:B->C)(f:A->B) : A->C := fun x => g (f x).
+
+Infix "o" := comp (at level 90).
+
+Definition sub_k1 (X Y:k1) : Type :=
+ forall A:Set, X A -> Y A.
+
+Infix "c_k1" := sub_k1 (at level 60).
+
+(** monotonicity *)
+Definition mon (X:k1) : Type := forall (A B:Set), (A -> B) -> X A -> X B.
+
+(** extensionality *)
+Definition ext (X:k1)(h: mon X): Prop :=
+ forall (A B:Set)(f g:A -> B),
+ (forall a, f a = g a) -> forall r, h _ _ f r = h _ _ g r.
+
+(** first functor law *)
+Definition fct1 (X:k1)(m: mon X) : Prop :=
+ forall (A:Set)(x:X A), m _ _ (id(A:=A)) x = x.
+
+(** second functor law *)
+Definition fct2 (X:k1)(m: mon X) : Prop :=
+ forall (A B C:Set)(f:A -> B)(g:B -> C)(x:X A),
+ m _ _ (g o f) x = m _ _ g (m _ _ f x).
+
+(** pack up the good properties of the approximation into
+ the notion of an extensional functor *)
+Record EFct (X:k1) : Type := mkEFct
+ { m : mon X;
+ e : ext m;
+ f1 : fct1 m;
+ f2 : fct2 m }.
+
+(** preservation of extensional functors *)
+Definition pEFct (F:k2) : Type :=
+ forall (X:k1), EFct X -> EFct (F X).
+
+
+(** we show some closure properties of pEFct, depending on such properties
+ for EFct *)
+
+Definition moncomp (X Y:k1)(mX:mon X)(mY:mon Y): mon (fun A => X(Y A)).
+Proof.
+ red.
+ intros X Y mX mY A B f x.
+ exact (mX (Y A)(Y B) (mY A B f) x).
+Defined.
+
+(** closure under composition *)
+Lemma compEFct (X Y:k1): EFct X -> EFct Y -> EFct (fun A => X(Y A)).
+Proof.
+ intros X Y ef1 ef2.
+ apply (mkEFct(m:=moncomp (m ef1) (m ef2))); red; intros; unfold moncomp.
+(* prove ext *)
+ apply (e ef1).
+ intro.
+ apply (e ef2); trivial.
+(* prove fct1 *)
+ rewrite (e ef1 (m ef2 (id (A:=A))) (id(A:=Y A))).
+ apply (f1 ef1).
+ intro.
+ apply (f1 ef2).
+(* prove fct2 *)
+ rewrite (e ef1 (m ef2 (g o f))((m ef2 g)o(m ef2 f))).
+ apply (f2 ef1).
+ intro.
+ unfold comp at 2.
+ apply (f2 ef2).
+Defined.
+
+Corollary comppEFct (F G:k2): pEFct F -> pEFct G ->
+ pEFct (fun X A => F X (G X A)).
+Proof.
+ red.
+ intros.
+ apply compEFct; auto.
+Defined.
+
+(** closure under sums *)
+Lemma sumEFct (X Y:k1): EFct X -> EFct Y -> EFct (fun A => X A + Y A)%type.
+Proof.
+ intros X Y ef1 ef2.
+ set (m12:=fun (A B:Set)(f:A->B) x => match x with
+ | inl y => inl _ (m ef1 f y)
+ | inr y => inr _ (m ef2 f y)
+ end).
+ apply (mkEFct(m:=m12)); red; intros.
+(* prove ext *)
+ destruct r.
+ simpl.
+ apply (f_equal (fun x=>inl (A:=X B) (Y B) x)).
+ apply (e ef1); trivial.
+ simpl.
+ apply (f_equal (fun x=>inr (X B) (B:=Y B) x)).
+ apply (e ef2); trivial.
+(* prove fct1 *)
+ destruct x.
+ simpl.
+ apply (f_equal (fun x=>inl (A:=X A) (Y A) x)).
+ apply (f1 ef1).
+ simpl.
+ apply (f_equal (fun x=>inr (X A) (B:=Y A) x)).
+ apply (f1 ef2).
+(* prove fct2 *)
+ destruct x.
+ simpl.
+ rewrite (f2 ef1); reflexivity.
+ simpl.
+ rewrite (f2 ef2); reflexivity.
+Defined.
+
+Corollary sumpEFct (F G:k2): pEFct F -> pEFct G ->
+ pEFct (fun X A => F X A + G X A)%type.
+Proof.
+ red.
+ intros.
+ apply sumEFct; auto.
+Defined.
+
+(** closure under products *)
+Lemma prodEFct (X Y:k1): EFct X -> EFct Y -> EFct (fun A => X A * Y A)%type.
+Proof.
+ intros X Y ef1 ef2.
+ set (m12:=fun (A B:Set)(f:A->B) x => match x with
+ (x1,x2) => (m ef1 f x1, m ef2 f x2) end).
+ apply (mkEFct(m:=m12)); red; intros.
+(* prove ext *)
+ destruct r as [x1 x2].
+ simpl.
+ apply injective_projections; simpl.
+ apply (e ef1); trivial.
+ apply (e ef2); trivial.
+(* prove fct1 *)
+ destruct x as [x1 x2].
+ simpl.
+ apply injective_projections; simpl.
+ apply (f1 ef1).
+ apply (f1 ef2).
+(* prove fct2 *)
+ destruct x as [x1 x2].
+ simpl.
+ apply injective_projections; simpl.
+ apply (f2 ef1).
+ apply (f2 ef2).
+Defined.
+
+Corollary prodpEFct (F G:k2): pEFct F -> pEFct G ->
+ pEFct (fun X A => F X A * G X A)%type.
+Proof.
+ red.
+ intros.
+ apply prodEFct; auto.
+Defined.
+
+(** the identity in k2 preserves extensional functors *)
+Lemma idpEFct: pEFct (fun X => X).
+Proof.
+ red.
+ intros.
+ assumption.
+Defined.
+
+(** a variant for the eta-expanded identity *)
+Lemma idpEFct_eta: pEFct (fun X A => X A).
+Proof.
+ red.
+ intros X ef.
+ destruct ef as [m0 e0 f01 f02].
+ change (mon X) with (mon (fun A => X A)) in m0.
+ apply (mkEFct (m:=m0) e0 f01 f02).
+Defined.
+
+(** the identity in k1 "is" an extensional functor *)
+Lemma idEFct: EFct (fun A => A).
+Proof.
+ set (mId:=fun A B (f:A->B)(x:A) => f x).
+ apply (mkEFct(m:=mId)).
+ red.
+ intros.
+ unfold mId.
+ apply H.
+ red.
+ reflexivity.
+ red.
+ reflexivity.
+Defined.
+
+(** constants in k2 *)
+Lemma constpEFct (X:k1): EFct X -> pEFct (fun _ => X).
+Proof.
+ red.
+ intros.
+ assumption.
+Defined.
+
+(** constants in k1 *)
+Lemma constEFct (C:Set): EFct (fun _ => C).
+Proof.
+ intro.
+ set (mC:=fun A B (f:A->B)(x:C) => x).
+ apply (mkEFct(m:=mC)); red; intros; unfold mC; reflexivity.
+Defined.
+
+
+(** the option type *)
+Lemma optionEFct: EFct (fun (A:Set) => option A).
+ apply (mkEFct (X:=fun (A:Set) => option A)(m:=option_map)); red; intros.
+ destruct r.
+ simpl.
+ rewrite H.
+ reflexivity.
+ reflexivity.
+ destruct x; reflexivity.
+ destruct x; reflexivity.
+Defined.
+
+
+(** natural transformations from (X,mX) to (Y,mY) *)
+Definition NAT(X Y:k1)(j:X c_k1 Y)(mX:mon X)(mY:mon Y) : Prop :=
+ forall (A B:Set)(f:A->B)(t:X A), j B (mX A B f t) = mY _ _ f (j A t).
+
+
+Module Type LNMIt_Type.
+
+Parameter F:k2.
+Parameter FpEFct: pEFct F.
+Parameter mu20: k1.
+Definition mu2: k1:= fun A => mu20 A.
+Parameter mapmu2: mon mu2.
+Definition MItType: Type :=
+ forall G : k1, (forall X : k1, X c_k1 G -> F X c_k1 G) -> mu2 c_k1 G.
+Parameter MIt0 : MItType.
+Definition MIt : MItType:= fun G s A t => MIt0 s t.
+Definition InType : Type :=
+ forall (X:k1)(ef:EFct X)(j: X c_k1 mu2),
+ NAT j (m ef) mapmu2 -> F X c_k1 mu2.
+Parameter In : InType.
+Axiom mapmu2Red : forall (A:Set)(X:k1)(ef:EFct X)(j: X c_k1 mu2)
+ (n: NAT j (m ef) mapmu2)(t: F X A)(B:Set)(f:A->B),
+ mapmu2 f (In ef n t) = In ef n (m (FpEFct ef) f t).
+Axiom MItRed : forall (G : k1)
+ (s : forall X : k1, X c_k1 G -> F X c_k1 G)(X : k1)(ef:EFct X)(j: X c_k1 mu2)
+ (n: NAT j (m ef) mapmu2)(A:Set)(t:F X A),
+ MIt s (In ef n t) = s X (fun A => (MIt s (A:=A)) o (j A)) A t.
+Definition mu2IndType : Prop :=
+ forall (P : (forall A : Set, mu2 A -> Prop)),
+ (forall (X : k1)(ef:EFct X)(j : X c_k1 mu2)(n: NAT j (m ef) mapmu2),
+ (forall (A : Set) (x : X A), P A (j A x)) ->
+ forall (A:Set)(t : F X A), P A (In ef n t)) ->
+ forall (A : Set) (r : mu2 A), P A r.
+Axiom mu2Ind : mu2IndType.
+
+End LNMIt_Type.
+
+(** BushDepPredShort.v Version 0.2 July 2008 *)
+(** does not need impredicative Set, produces stack overflow under V8.2, tested
+with SVN 11296 *)
+
+(** Copyright Ralph Matthes, I.R.I.T., C.N.R.S. & University of Toulouse *)
+
+Set Implicit Arguments.
+
+Require Import List.
+
+Definition listk1 (A:Set) : Set := list A.
+Open Scope type_scope.
+
+Definition BushF(X:k1)(A:Set) := unit + A * X (X A).
+
+Definition bushpEFct : pEFct BushF.
+Proof.
+ unfold BushF.
+ apply sumpEFct.
+ apply constpEFct.
+ apply constEFct.
+ apply prodpEFct.
+ apply constpEFct.
+ apply idEFct.
+ apply comppEFct.
+ apply idpEFct.
+ apply idpEFct_eta.
+Defined.
+
+Module Type BUSH := LNMIt_Type with Definition F:=BushF
+ with Definition FpEFct :=
+bushpEFct.
+
+Module Bush (BushBase:BUSH).
+
+Definition Bush : k1 := BushBase.mu2.
+
+Definition bush : mon Bush := BushBase.mapmu2.
+
+End Bush.
+
+
+Definition Id : k1 := fun X => X.
+
+Fixpoint Pow (X:k1)(k:nat){struct k}:k1:=
+ match k with 0 => Id
+ | S k' => fun A => X (Pow X k' A)
+ end.
+
+Fixpoint POW (k:nat)(X:k1)(m:mon X){struct k} : mon (Pow X k) :=
+ match k return mon (Pow X k)
+ with 0 => fun _ _ f => f
+ | S k' => fun _ _ f => m _ _ (POW k' m f)
+ end.
+
+Module Type BushkToList_Type.
+
+Declare Module Import BP: BUSH.
+Definition F:=BushF.
+Definition FpEFct:= bushpEFct.
+Definition mu20 := mu20.
+Definition mu2 := mu2.
+Definition mapmu2 := mapmu2.
+Definition MItType:= MItType.
+Definition MIt0 := MIt0.
+Definition MIt := MIt.
+Definition InType := InType.
+Definition In := In.
+Definition mapmu2Red:=mapmu2Red.
+Definition MItRed:=MItRed.
+Definition mu2IndType:=mu2IndType.
+Definition mu2Ind:=mu2Ind.
+
+Definition Bush:= mu2.
+Module BushM := Bush BP.
+
+Parameter BushkToList: forall(k:nat)(A:k0)(t:Pow Bush k A), list A.
+Axiom BushkToList0: forall(A:k0)(t:Pow Bush 0 A), BushkToList 0 A t = t::nil.
+
+End BushkToList_Type.
+
+Module BushDep (BushkToListM:BushkToList_Type).
+
+Module Bush := Bush BushkToListM.
+
+Import Bush.
+Import BushkToListM.
+
+
+Lemma BushkToList0NAT: NAT(Y:=listk1) (BushkToList 0) (POW 0 bush) map.
+Proof.
+ red.
+ intros.
+ simpl.
+ rewrite BushkToList0.
+(* stack overflow for coqc and coqtop *)
+
+
+Abort.
diff --git a/test-suite/bugs/closed/shouldsucceed/1925.v b/test-suite/bugs/closed/shouldsucceed/1925.v
new file mode 100644
index 00000000..17eb721a
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1925.v
@@ -0,0 +1,22 @@
+(* Check that the analysis of projectable rel's in an evar instance is up to
+ aliases *)
+
+Require Import List.
+
+Definition compose (A B C : Type) (g : B -> C) (f : A -> B) : A -> C :=
+ fun x : A => g(f x).
+
+Definition map_fuse' :
+ forall (A B C : Type) (g : B -> C) (f : A -> B) (xs : list A),
+ (map g (map f xs)) = map (compose _ _ _ g f) xs
+ :=
+ fun A B C g f =>
+ (fix loop (ys : list A) {struct ys} :=
+ match ys as ys return (map g (map f ys)) = map (compose _ _ _ g f) ys
+ with
+ | nil => refl_equal nil
+ | x :: xs =>
+ match loop xs in eq _ a return eq _ ((g (f x)) :: a) with
+ | refl_equal => refl_equal (map g (map f (x :: xs)))
+ end
+ end).
diff --git a/test-suite/bugs/closed/shouldsucceed/1931.v b/test-suite/bugs/closed/shouldsucceed/1931.v
new file mode 100644
index 00000000..bc8be78f
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1931.v
@@ -0,0 +1,29 @@
+
+
+Set Implicit Arguments.
+
+Inductive T (A:Set) : Set :=
+ app : T A -> T A -> T A.
+
+Fixpoint map (A B:Set)(f:A->B)(t:T A) : T B :=
+ match t with
+ app t1 t2 => app (map f t1)(map f t2)
+ end.
+
+Fixpoint subst (A B:Set)(f:A -> T B)(t:T A) :T B :=
+ match t with
+ app t1 t2 => app (subst f t1)(subst f t2)
+ end.
+
+(* This is the culprit: *)
+Definition k0:=Set.
+
+(** interaction of subst with map *)
+Lemma substLaw1 (A:k0)(B C:Set)(f: A -> B)(g:B -> T C)(t: T A):
+ subst g (map f t) = subst (fun x => g (f x)) t.
+Proof.
+ intros.
+ generalize B C f g; clear B C f g.
+ induction t; intros; simpl.
+ f_equal.
+Admitted.
diff --git a/test-suite/bugs/closed/shouldsucceed/1935.v b/test-suite/bugs/closed/shouldsucceed/1935.v
new file mode 100644
index 00000000..641dcb7a
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1935.v
@@ -0,0 +1,21 @@
+Definition f (n:nat) := n = n.
+
+Lemma f_refl : forall n , f n.
+intros. reflexivity.
+Qed.
+
+Definition f' (x:nat) (n:nat) := n = n.
+
+Lemma f_refl' : forall n , f' n n.
+Proof.
+ intros. reflexivity.
+Qed.
+
+Require Import ZArith.
+
+Definition f'' (a:bool) := if a then eq (A:= Z) else Zlt.
+
+Lemma f_refl'' : forall n , f'' true n n.
+Proof.
+ intro. reflexivity.
+Qed.
diff --git a/test-suite/bugs/closed/shouldsucceed/1963.v b/test-suite/bugs/closed/shouldsucceed/1963.v
new file mode 100644
index 00000000..11e2ee44
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1963.v
@@ -0,0 +1,19 @@
+(* Check that "dependent inversion" behaves correctly w.r.t to universes *)
+
+Require Import Eqdep.
+
+Set Implicit Arguments.
+
+Inductive illist(A:Type) : nat -> Type :=
+ illistn : illist A 0
+| illistc : forall n:nat, A -> illist A n -> illist A (S n).
+
+Inductive isig (A:Type)(P:A -> Type) : Type :=
+ iexists : forall x : A, P x -> isig P.
+
+Lemma inv : forall (A:Type)(n n':nat)(ts':illist A n'), n' = S n ->
+ isig (fun t => isig (fun ts =>
+ eq_dep nat (fun n => illist A n) n' ts' (S n) (illistc t ts))).
+Proof.
+intros.
+dependent inversion ts'.
diff --git a/test-suite/bugs/closed/shouldsucceed/1977.v b/test-suite/bugs/closed/shouldsucceed/1977.v
new file mode 100644
index 00000000..28715040
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1977.v
@@ -0,0 +1,4 @@
+Inductive T {A} : Prop := c : A -> T.
+Goal (@T nat).
+apply c. exact 0.
+Qed.
diff --git a/test-suite/bugs/closed/shouldsucceed/1981.v b/test-suite/bugs/closed/shouldsucceed/1981.v
new file mode 100644
index 00000000..0c3b96da
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1981.v
@@ -0,0 +1,5 @@
+Implicit Arguments ex_intro [A].
+
+Goal exists n : nat, True.
+ eapply ex_intro. exact 0. exact I.
+Qed.
diff --git a/test-suite/bugs/closed/shouldsucceed/2001.v b/test-suite/bugs/closed/shouldsucceed/2001.v
new file mode 100644
index 00000000..323021de
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2001.v
@@ -0,0 +1,20 @@
+(* Automatic computing of guard in "Theorem with"; check that guard is not
+ computed when the user explicitly indicated it *)
+
+Inductive T : Set :=
+| v : T.
+
+Definition f (s:nat) (t:T) : nat.
+fix 2.
+intros s t.
+refine
+ match t with
+ | v => s
+ end.
+Defined.
+
+Lemma test :
+ forall s, f s v = s.
+Proof.
+reflexivity.
+Qed.
diff --git a/test-suite/bugs/closed/shouldsucceed/2017.v b/test-suite/bugs/closed/shouldsucceed/2017.v
new file mode 100644
index 00000000..948cea3e
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2017.v
@@ -0,0 +1,15 @@
+(* Some check of Miller's pattern inference - used to fail in 8.2 due
+ first to the presence of aliases, secondly due to the absence of
+ restriction of the potential interesting variables to the subset of
+ variables effectively occurring in the term to instantiate *)
+
+Set Implicit Arguments.
+
+Variable choose : forall(P : bool -> Prop)(H : exists x, P x), bool.
+
+Variable H : exists x : bool, True.
+
+Definition coef :=
+match Some true with
+ Some _ => @choose _ H |_ => true
+end .
diff --git a/test-suite/bugs/closed/shouldsucceed/2021.v b/test-suite/bugs/closed/shouldsucceed/2021.v
new file mode 100644
index 00000000..e598e5ae
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2021.v
@@ -0,0 +1,23 @@
+(* correct failure of injection/discriminate on types whose inductive
+ status derives from the substitution of an argument *)
+
+Inductive t : nat -> Type :=
+| M : forall n: nat, nat -> t n.
+
+Lemma eq_t : forall n n' m m',
+ existT (fun B : Type => B) (t n) (M n m) =
+ existT (fun B : Type => B) (t n') (M n' m') -> True.
+Proof.
+ intros.
+ injection H.
+ intro Ht.
+ exact I.
+Qed.
+
+Lemma eq_t' : forall n n' : nat,
+ existT (fun B : Type => B) (t n) (M n 0) =
+ existT (fun B : Type => B) (t n') (M n' 1) -> True.
+Proof.
+ intros.
+ discriminate H || exact I.
+Qed.
diff --git a/test-suite/bugs/closed/shouldsucceed/2027.v b/test-suite/bugs/closed/shouldsucceed/2027.v
new file mode 100644
index 00000000..fb53c6ef
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2027.v
@@ -0,0 +1,11 @@
+
+Parameter T : Type -> Type.
+Parameter f : forall {A}, T A -> T A.
+Parameter P : forall {A}, T A -> Prop.
+Axiom f_id : forall {A} (l : T A), f l = l.
+
+Goal forall A (p : T A), P p.
+Proof.
+ intros.
+ rewrite <- f_id.
+Admitted. \ No newline at end of file