Modification de la test suite pour intégrer des tests spécifiques aux

bugs soumis sur Coq-bugs.



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10068 85f007b7-540e-0410-9357-904b9bb8a0f7

18 files changed, 600 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/shouldsucceed/1243.v b/test-suite/bugs/closed/shouldsucceed/1243.v
new file mode 100644
index 000000000..7d6781db2
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1243.v
@@ -0,0 +1,12 @@
+Require Import ZArith.
+Require Import Arith.
+Open Scope Z_scope.
+
+Theorem r_ex : (forall x y:nat, x + y = x + y)%nat.
+Admitted.
+
+Theorem r_ex' : forall x y:nat, (x + y = x + y)%nat.
+Admitted.
+
+
+
diff --git a/test-suite/bugs/closed/shouldsucceed/1302.v b/test-suite/bugs/closed/shouldsucceed/1302.v
new file mode 100644
index 000000000..e94dfcfb0
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1302.v
@@ -0,0 +1,22 @@
+Module Type T.
+
+Parameter A : Type.
+
+Inductive L : Type :=
+| L0 : L (* without this constructor, it works right *)
+| L1 :  A -> L.
+
+End T.
+
+Axiom Tp : Type.
+
+Module TT : T.
+
+Definition A : Type := Tp.
+
+Inductive L : Type :=
+| L0 : L
+| L1 :  A -> L.
+
+End TT.
+
diff --git a/test-suite/bugs/closed/shouldsucceed/1419.v b/test-suite/bugs/closed/shouldsucceed/1419.v
new file mode 100644
index 000000000..d021107d1
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1419.v
@@ -0,0 +1,8 @@
+Goal True.
+  set(a := 0).
+  set(b := a).
+  unfold a in b.
+  clear a.
+  Eval vm_compute in  b.
+  trivial.
+Qed.
diff --git a/test-suite/bugs/closed/shouldsucceed/1446.v b/test-suite/bugs/closed/shouldsucceed/1446.v
new file mode 100644
index 000000000..d4e7cea81
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1446.v
@@ -0,0 +1,20 @@
+Lemma not_true_eq_false : forall (b:bool), b <> true -> b = false.
+Proof.
+ destruct b;intros;trivial. 
+ elim H. 
+ exact (refl_equal true). 
+Qed.
+
+Section BUG.
+
+ Variable b : bool.
+ Hypothesis H  : b <> true.
+ Hypothesis H0 : b = true.
+ Hypothesis H1 : b <> true.
+
+ Goal False.
+  rewrite (not_true_eq_false _ H) in * |-. 
+  contradiction.
+ Qed.
+
+End BUG.
diff --git a/test-suite/bugs/closed/shouldsucceed/1448.v b/test-suite/bugs/closed/shouldsucceed/1448.v
new file mode 100644
index 000000000..bd016c995
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1448.v
@@ -0,0 +1,26 @@
+Require Import Relations.
+Require Import Ring_theory.
+Require Import Ring_base.
+
+Variable R : Type.
+Variable Rone Rzero : R.
+Variable Rplus Rmult Rminus : R -> R -> R.
+Variable Rneg : R -> R.
+
+Lemma my_ring_theory : @ring_theory R Rzero Rone Rplus Rmult Rminus Rneg (@eq
+R).
+Admitted.
+
+Variable Req : R -> R -> Prop.
+
+Hypothesis Req_refl : reflexive _ Req.
+Hypothesis Req_sym : symmetric _ Req.
+Hypothesis Req_trans : transitive _ Req.
+
+Add Relation R Req
+  reflexivity proved by Req_refl
+  symmetry proved by Req_sym
+  transitivity proved by Req_trans
+  as Req_rel.
+
+Add Ring my_ring : my_ring_theory (abstract).
diff --git a/test-suite/bugs/closed/shouldsucceed/1477.v b/test-suite/bugs/closed/shouldsucceed/1477.v
new file mode 100644
index 000000000..dfc8c3280
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1477.v
@@ -0,0 +1,18 @@
+Inductive I : Set :=
+  | A : nat -> nat -> I
+  | B : nat -> nat -> I.
+
+Definition foo1 (x:I) : nat :=
+  match x with
+    | A a b | B a b => S b
+  end.
+
+Definition foo2 (x:I) : nat :=
+  match x with
+    | A _ b | B b _ => S b
+  end.
+
+Definition foo (x:I) : nat :=
+  match x with
+    | A a b | B b a => S b
+  end.
diff --git a/test-suite/bugs/closed/shouldsucceed/1483.v b/test-suite/bugs/closed/shouldsucceed/1483.v
new file mode 100644
index 000000000..a3d7f1683
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1483.v
@@ -0,0 +1,10 @@
+Require Import BinPos.
+
+Definition P := (fun x : positive => x = xH).
+
+Goal forall (p q : positive), P q -> q = p -> P p.
+intros; congruence.
+Qed.
+
+
+
diff --git a/test-suite/bugs/closed/shouldsucceed/1507.v b/test-suite/bugs/closed/shouldsucceed/1507.v
new file mode 100644
index 000000000..32e6489c5
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1507.v
@@ -0,0 +1,121 @@
+(*
+   Implementing reals a la Stolzenberg
+
+   Danko Ilik, March 2007
+   svn revision: $Id$
+
+   XField.v -- (unfinished) axiomatisation of the theories of real and
+               rational intervals.
+*)
+
+Definition associative (A:Type)(op:A->A->A) := 
+  forall x y z:A, op (op x y) z = op x (op y z).
+
+Definition commutative (A:Type)(op:A->A->A) := 
+  forall x y:A, op x y = op y x.
+
+Definition trichotomous (A:Type)(R:A->A->Prop) :=
+  forall x y:A, R x y \/ x=y \/ R y x.
+
+Definition relation (A:Type) := A -> A -> Prop.
+Definition reflexive (A:Type)(R:relation A) := forall x:A, R x x.
+Definition transitive (A:Type)(R:relation A) := 
+  forall x y z:A, R x y -> R y z -> R x z.
+Definition symmetric (A:Type)(R:relation A) := forall x y:A, R x y -> R y x.
+
+Record interval (X:Set)(le:X->X->Prop) : Set :=
+  interval_make {
+    interval_left : X;
+    interval_right : X;
+    interval_nonempty : le interval_left interval_right
+  }.
+
+Record I (grnd:Set)(le:grnd->grnd->Prop) : Type := Imake {
+  Icar    := interval grnd le;
+  Iplus   : Icar -> Icar -> Icar;
+  Imult   : Icar -> Icar -> Icar;
+  Izero   : Icar;
+  Ione    : Icar;
+  Iopp    : Icar -> Icar;
+  Iinv    : Icar -> Icar;
+  Ic      : Icar -> Icar -> Prop; (* consistency *)
+  (* monoids *)
+  Iplus_assoc    : associative Icar Iplus;
+  Imult_assoc    : associative Icar Imult;
+  (* abelian groups *)
+  Iplus_comm     : commutative Icar Iplus;
+  Imult_comm     : commutative Icar Imult;
+  Iplus_0_l      : forall x:Icar, Ic (Iplus Izero x) x;
+  Iplus_0_r      : forall x:Icar, Ic (Iplus x Izero) x;
+  Imult_0_l      : forall x:Icar, Ic (Imult Ione x) x;
+  Imult_0_r      : forall x:Icar, Ic (Imult x Ione) x;
+  Iplus_opp_r    : forall x:Icar, Ic (Iplus x (Iopp x)) (Izero);
+  Imult_inv_r    : forall x:Icar, ~(Ic x Izero) -> Ic (Imult x (Iinv x)) Ione;
+  (* distributive laws *)
+  Imult_plus_distr_l : forall x x' y y' z z' z'', 
+    Ic x x' -> Ic y y' -> Ic z z' -> Ic z z'' ->
+    Ic (Imult (Iplus x y) z) (Iplus (Imult x' z') (Imult y' z''));
+  (* order and lattice structure *)
+  Ilt          : Icar -> Icar -> Prop;
+  Ilc          := fun (x y:Icar) => Ilt x y \/ Ic x y;
+  Isup         : Icar -> Icar -> Icar;
+  Iinf         : Icar -> Icar -> Icar;
+  Ilt_trans    : transitive _ lt;
+  Ilt_trich    : forall x y:Icar, Ilt x y \/ Ic x y \/ Ilt y x;
+  Isup_lub     : forall x y z:Icar, Ilc x z -> Ilc y z -> Ilc (Isup x y) z;
+  Iinf_glb     : forall x y z:Icar, Ilc x y -> Ilc x z -> Ilc x (Iinf y z);
+  (* order preserves operations? *)
+  (* properties of Ic *)
+  Ic_refl   : reflexive _ Ic;
+  Ic_sym    : symmetric _ Ic
+}.
+
+Definition interval_set (X:Set)(le:X->X->Prop) := 
+  (interval X le) -> Prop. (* can be Set as well *)
+Check interval_set.
+Check Ic.
+Definition consistent (X:Set)(le:X->X->Prop)(TI:I X le)(p:interval_set X le) :=
+  forall I J:interval X le, p I -> p J -> (Ic X le TI) I J.
+Check consistent.
+(* define 'fine' *)
+
+Record N (grnd:Set)(le:grnd->grnd->Prop)(grndI:I grnd le) : Type := Nmake {
+  Ncar    := interval_set grnd le;
+  Nplus   : Ncar -> Ncar -> Ncar;
+  Nmult   : Ncar -> Ncar -> Ncar;
+  Nzero   : Ncar;
+  None    : Ncar;
+  Nopp    : Ncar -> Ncar;
+  Ninv    : Ncar -> Ncar;
+  Nc      : Ncar -> Ncar -> Prop; (* Ncistency *)
+  (* monoids *)
+  Nplus_assoc    : associative Ncar Nplus;
+  Nmult_assoc    : associative Ncar Nmult;
+  (* abelian groups *)
+  Nplus_comm     : commutative Ncar Nplus;
+  Nmult_comm     : commutative Ncar Nmult;
+  Nplus_0_l      : forall x:Ncar, Nc (Nplus Nzero x) x;
+  Nplus_0_r      : forall x:Ncar, Nc (Nplus x Nzero) x;
+  Nmult_0_l      : forall x:Ncar, Nc (Nmult None x) x;
+  Nmult_0_r      : forall x:Ncar, Nc (Nmult x None) x;
+  Nplus_opp_r    : forall x:Ncar, Nc (Nplus x (Nopp x)) (Nzero);
+  Nmult_inv_r    : forall x:Ncar, ~(Nc x Nzero) -> Nc (Nmult x (Ninv x)) None;
+  (* distributive laws *)
+  Nmult_plus_distr_l : forall x x' y y' z z' z'', 
+    Nc x x' -> Nc y y' -> Nc z z' -> Nc z z'' ->
+    Nc (Nmult (Nplus x y) z) (Nplus (Nmult x' z') (Nmult y' z''));
+  (* order and lattice structure *)
+  Nlt          : Ncar -> Ncar -> Prop;
+  Nlc          := fun (x y:Ncar) => Nlt x y \/ Nc x y;
+  Nsup         : Ncar -> Ncar -> Ncar;
+  Ninf         : Ncar -> Ncar -> Ncar;
+  Nlt_trans    : transitive _ lt;
+  Nlt_trich    : forall x y:Ncar, Nlt x y \/ Nc x y \/ Nlt y x;
+  Nsup_lub     : forall x y z:Ncar, Nlc x z -> Nlc y z -> Nlc (Nsup x y) z;
+  Ninf_glb     : forall x y z:Ncar, Nlc x y -> Nlc x z -> Nlc x (Ninf y z);
+  (* order preserves operations? *)
+  (* properties of Nc *)
+  Nc_refl   : reflexive _ Nc;
+  Nc_sym    : symmetric _ Nc
+}.
+
diff --git a/test-suite/bugs/closed/shouldsucceed/1519.v b/test-suite/bugs/closed/shouldsucceed/1519.v
new file mode 100644
index 000000000..66bab241d
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1519.v
@@ -0,0 +1,14 @@
+Section S.
+
+  Variable A:Prop.
+  Variable W:A.
+
+  Remark T: A -> A.
+    intro Z.
+    rename W into Z_.
+    rename Z into W.
+    rename Z_ into Z.
+    exact Z.
+  Qed.
+
+End S.
diff --git a/test-suite/bugs/closed/shouldsucceed/1568.v b/test-suite/bugs/closed/shouldsucceed/1568.v
new file mode 100644
index 000000000..9f10f7490
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1568.v
@@ -0,0 +1,13 @@
+CoInductive A: Set :=
+  mk_A: B -> A
+with B: Set :=
+  mk_B: A -> B.
+
+CoFixpoint a:A := mk_A b 
+with b:B := mk_B a.
+
+Goal b = match a with mk_A a1 => a1 end.
+  simpl. reflexivity.
+Qed.
+
+
diff --git a/test-suite/bugs/closed/shouldsucceed/1576.v b/test-suite/bugs/closed/shouldsucceed/1576.v
new file mode 100644
index 000000000..c9ebbd142
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1576.v
@@ -0,0 +1,38 @@
+Module Type TA.
+Parameter t : Set.
+End TA.
+
+Module Type TB.
+Declare Module A: TA.
+End TB.
+
+Module Type TC.
+Declare Module B : TB.
+End TC.
+
+Module Type TD.
+
+Declare Module B: TB .
+Declare Module C: TC 
+    with Module B := B  . 
+End TD.
+
+Module Type TE.
+Declare Module D : TD.
+End TE.
+
+Module Type TF.
+Declare Module E:  TE.
+End TF.
+
+Module G (D: TD). 
+Module B' := D.C.B.
+End G.
+
+Module H  (F: TF).
+Module I := G(F.E.D).
+End H.
+
+Declare Module F:  TF.
+Module K := H(F).
+
diff --git a/test-suite/bugs/closed/shouldsucceed/1582.v b/test-suite/bugs/closed/shouldsucceed/1582.v
new file mode 100644
index 000000000..47953a66f
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1582.v
@@ -0,0 +1,15 @@
+Require Import Peano_dec.
+
+Definition fact_F : 
+  forall (n:nat),
+  (forall m, m<n -> nat) ->
+  nat.
+refine 
+  (fun n fact_rec =>
+     if eq_nat_dec n 0 then 
+        1
+     else
+        let fn := fact_rec (n-1) _ in
+        n * fn).
+Admitted.
+
diff --git a/test-suite/bugs/closed/shouldsucceed/1618.v b/test-suite/bugs/closed/shouldsucceed/1618.v
new file mode 100644
index 000000000..a90290bfb
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1618.v
@@ -0,0 +1,23 @@
+Inductive A: Set :=
+| A1: nat -> A.
+
+Definition A_size (a: A) : nat :=
+  match a with
+    | A1 n => 0
+  end.
+
+Require Import Recdef. 
+
+Function n3 (P: A -> Prop) (f: forall n, P (A1 n)) (a: A) {struct a} : P a :=
+  match a  return (P a) with
+    | A1 n => f n
+  end.
+
+
+Function n1 (P: A -> Prop) (f: forall n, P (A1 n)) (a: A) {measure A_size a} :
+P
+a :=
+  match a return (P a) with
+    | A1 n => f n
+  end.
+
diff --git a/test-suite/bugs/closed/shouldsucceed/348.v b/test-suite/bugs/closed/shouldsucceed/348.v
new file mode 100644
index 000000000..28cc5cb1e
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/348.v
@@ -0,0 +1,13 @@
+Module Type S.
+  Parameter empty: Set.
+End S.
+
+Module D (M:S).
+  Import M.
+  Definition empty:=nat.
+End D.
+
+Module D' (M:S).
+  Import M.
+  Definition empty:Set. exact nat. Save.
+End D'.
diff --git a/test-suite/bugs/closed/shouldsucceed/38.v b/test-suite/bugs/closed/shouldsucceed/38.v
new file mode 100644
index 000000000..7bc04b1fe
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/38.v
@@ -0,0 +1,22 @@
+Require Import Setoid.
+
+Variable A : Set.
+
+Inductive liste : Set :=
+| vide : liste
+| c : A -> liste -> liste.
+
+Inductive e : A -> liste -> Prop := 
+| ec : forall (x : A) (l : liste), e x (c x l)
+| ee : forall (x y : A) (l : liste), e x l -> e x (c y l).
+
+Definition same := fun (l m : liste) => forall (x : A), e x l <-> e x m.
+
+Definition same_refl (x:liste) : (same x x).
+  unfold same; split; intros; trivial.
+Save.
+
+Goal forall (x:liste), (same x x).
+  intro.
+  apply (same_refl x).
+Qed.
diff --git a/test-suite/bugs/closed/shouldsucceed/545.v b/test-suite/bugs/closed/shouldsucceed/545.v
new file mode 100644
index 000000000..926af7dd1
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/545.v
@@ -0,0 +1,5 @@
+Require Export Reals.
+
+Parameter toto : nat -> nat -> nat.
+
+Notation " e # f " := (toto e f) (at level 30, f at level 0).
diff --git a/test-suite/bugs/closed/shouldsucceed/846.v b/test-suite/bugs/closed/shouldsucceed/846.v
new file mode 100644
index 000000000..a963b225f
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/846.v
@@ -0,0 +1,213 @@
+Set Implicit Arguments.
+
+Open Scope type_scope.
+
+Inductive One : Set := inOne: One.
+
+Definition maybe: forall A B:Set,(A -> B) -> One + A -> One + B.
+Proof.
+  intros A B f c.
+  case c.
+  left; assumption.
+  right; apply f; assumption.
+Defined.
+
+Definition id (A:Set)(a:A):=a.
+
+Definition LamF (X: Set -> Set)(A:Set) :Set :=
+  A + (X A)*(X A) + X(One + A).
+
+Definition LamF' (X: Set -> Set)(A:Set) :Set :=
+  LamF X A.
+
+Require Import List.
+Require Import Bool.
+
+Definition index := list bool.
+
+Inductive L (A:Set) : index -> Set :=
+  initL: A -> L A nil
+  | pluslL: forall l:index, One -> L A (false::l) 
+  | plusrL: forall l:index, L A l -> L A (false::l)
+  | varL: forall l:index, L A l -> L A (true::l)
+  | appL: forall l:index, L A (true::l) -> L A (true::l) -> L A (true::l)
+  | absL: forall l:index, L A (true::false::l) -> L A (true::l).
+
+Scheme L_rec_simp := Minimality for L Sort Set.
+
+Definition Lam' (A:Set) := L A (true::nil).
+
+Definition aczelapp: forall (l1 l2: index)(A:Set), L (L A l2) l1 -> L A
+  (l1++l2).
+Proof.
+  intros l1 l2 A.
+  generalize l1.
+  clear l1.
+  (* Check (fun i:index => L A (i++l2)). *)
+  apply (L_rec_simp (A:=L A l2) (fun i:index => L A (i++l2))).
+  trivial.
+  intros l o.
+  simpl app.
+  apply pluslL; assumption.
+  intros l _ t.
+  simpl app.
+  apply plusrL; assumption.
+  intros l _ t.
+  simpl app.
+  apply varL; assumption.
+  intros l _ t1 _ t2.
+  simpl app in *|-*.
+  Check 0.
+  apply appL; [exact t1| exact t2].
+  intros l _ t.
+  simpl app in *|-*.
+  Check 0.
+  apply absL; assumption.
+Defined.
+
+Definition monL: forall (l:index)(A:Set)(B:Set), (A->B) -> L A l -> L B l.
+Proof.
+  intros l A B f.
+  intro t.
+  elim t.
+  intro a.
+  exact (initL (f a)).
+  intros i u.
+  exact (pluslL _ _ u).
+  intros i _ r.
+  exact (plusrL r).
+  intros i _ r.
+  exact (varL r).
+  intros i _ r1 _ r2.
+  exact (appL r1 r2).
+  intros i _ r.
+  exact (absL r).
+Defined.
+
+Definition lam': forall (A B:Set), (A -> B) -> Lam' A -> Lam' B.
+Proof.
+  intros A B f t.
+  unfold Lam' in *|-*.
+  Check 0.
+  exact (monL f t).
+Defined.
+
+Definition inLam': forall A:Set, LamF' Lam' A -> Lam' A.
+Proof.
+  intros A [[a|[t1 t2]]|r].
+  unfold Lam'.
+  exact (varL (initL a)).
+  exact (appL t1 t2).
+  unfold Lam' in * |- *.
+  Check 0.
+  apply absL.
+  change (L A ((true::nil) ++ (false::nil))).
+  apply aczelapp.
+  (* Check (fun x:One + A =>  (match (maybe (fun a:A => initL a) x) with
+    | inl u => pluslL _ _ u
+    | inr t' => plusrL t' end)). *)
+  exact (monL (fun x:One + A =>
+    (match (maybe (fun a:A => initL a) x) with
+       | inl u => pluslL _ _ u
+       | inr t' => plusrL t' end)) r). 
+Defined.
+
+Section minimal.
+
+Definition sub1 (F G: Set -> Set):= forall A:Set, F A->G A.
+Hypothesis G: Set -> Set.
+Hypothesis step: sub1 (LamF' G) G.
+
+Fixpoint L'(A:Set)(i:index){struct i} : Set :=
+  match i with 
+    nil => A
+    | false::l => One + L' A l
+    | true::l => G (L' A l)
+  end. 
+
+Definition LinL': forall (A:Set)(i:index), L A i -> L' A i.
+Proof.
+  intros A i t.
+  elim t.
+  intro a.
+  unfold L'.
+  assumption.
+  intros l u.
+  left; assumption.
+  intros l _ r.
+  right; assumption.
+  intros l _ r.
+  apply (step (A:=L' A l)).
+  exact (inl _ (inl _ r)).
+  intros l _ r1 _ r2.
+  apply (step (A:=L' A l)).
+  (* unfold L' in * |- *.
+  Check 0. *)
+  exact (inl _ (inr _ (pair r1 r2))).
+  intros l _ r.
+  apply  (step (A:=L' A l)).
+  exact (inr _ r).
+Defined.
+
+Definition L'inG: forall A: Set, L' A (true::nil) -> G A.
+Proof.
+  intros A t.
+  unfold L' in t.
+  assumption.
+Defined.
+
+Definition Itbasic: sub1 Lam' G.
+Proof.
+  intros A t.
+  apply L'inG.
+  unfold Lam' in t.
+  exact (LinL' t).
+Defined.
+
+End minimal.
+
+Definition recid := Itbasic inLam'.
+
+Definition L'Lam'inL: forall (i:index)(A:Set), L' Lam' A i -> L A i.
+Proof.
+  intros i A t.
+  induction i.
+  unfold L' in t.
+  apply initL.
+  assumption.
+  induction a.
+  simpl L' in t.
+  apply (aczelapp (l1:=true::nil) (l2:=i)). 
+  exact (lam' IHi t).
+  simpl L' in t.
+  induction t.
+  exact (pluslL _ _ a).
+  exact (plusrL (IHi b)).
+Defined.
+
+
+Lemma recidgen: forall(A:Set)(i:index)(t:L A i), L'Lam'inL i A (LinL' inLam' t)
+  = t.
+Proof.
+  intros A i t.
+  induction t.
+  trivial.
+  trivial.
+  simpl.
+  rewrite IHt.
+  trivial.
+  simpl L'Lam'inL.
+  rewrite IHt.
+  trivial.
+  simpl L'Lam'inL.
+  simpl L'Lam'inL in IHt1.
+  unfold lam' in IHt1.
+  simpl L'Lam'inL in IHt2.
+  unfold lam' in IHt2.
+
+  (* going on. This fails for the original solution. *)
+  rewrite IHt1.
+  rewrite IHt2.
+  trivial.
+Abort. (* one goal still left *)
+
diff --git a/test-suite/bugs/closed/shouldsucceed/931.v b/test-suite/bugs/closed/shouldsucceed/931.v
new file mode 100644
index 000000000..21f15e721
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/931.v
@@ -0,0 +1,7 @@
+Parameter P : forall n : nat, n=n -> Prop.
+
+Goal Prop.
+  refine (P _ _).
+  instantiate (1:=0).
+  trivial.
+Qed.