From 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Wed, 21 Jul 2010 09:46:51 +0200
Subject: Imported Upstream snapshot 8.3~beta0+13298

---
 test-suite/bugs/closed/shouldsucceed/1100.v |  2 +-
 test-suite/bugs/closed/shouldsucceed/1322.v |  2 +-
 test-suite/bugs/closed/shouldsucceed/1411.v |  2 +-
 test-suite/bugs/closed/shouldsucceed/1414.v | 41 +++++++++----------
 test-suite/bugs/closed/shouldsucceed/1416.v | 27 +++++++++++++
 test-suite/bugs/closed/shouldsucceed/1425.v |  2 +-
 test-suite/bugs/closed/shouldsucceed/1446.v |  8 ++--
 test-suite/bugs/closed/shouldsucceed/1507.v | 14 +++----
 test-suite/bugs/closed/shouldsucceed/1568.v |  2 +-
 test-suite/bugs/closed/shouldsucceed/1576.v |  6 +--
 test-suite/bugs/closed/shouldsucceed/1582.v |  6 +--
 test-suite/bugs/closed/shouldsucceed/1618.v |  2 +-
 test-suite/bugs/closed/shouldsucceed/1634.v |  2 +-
 test-suite/bugs/closed/shouldsucceed/1643.v |  1 -
 test-suite/bugs/closed/shouldsucceed/1683.v |  2 +-
 test-suite/bugs/closed/shouldsucceed/1711.v | 34 ++++++++++++++++
 test-suite/bugs/closed/shouldsucceed/1738.v |  6 +--
 test-suite/bugs/closed/shouldsucceed/1740.v |  2 +-
 test-suite/bugs/closed/shouldsucceed/1775.v |  2 +-
 test-suite/bugs/closed/shouldsucceed/1776.v |  2 +-
 test-suite/bugs/closed/shouldsucceed/1784.v | 14 +++----
 test-suite/bugs/closed/shouldsucceed/1791.v |  2 +-
 test-suite/bugs/closed/shouldsucceed/1844.v |  2 +-
 test-suite/bugs/closed/shouldsucceed/1891.v |  2 +-
 test-suite/bugs/closed/shouldsucceed/1901.v |  6 +--
 test-suite/bugs/closed/shouldsucceed/1905.v |  2 +-
 test-suite/bugs/closed/shouldsucceed/1918.v | 39 +++++++++---------
 test-suite/bugs/closed/shouldsucceed/1925.v | 10 ++---
 test-suite/bugs/closed/shouldsucceed/1931.v |  4 +-
 test-suite/bugs/closed/shouldsucceed/1935.v |  4 +-
 test-suite/bugs/closed/shouldsucceed/1939.v | 19 +++++++++
 test-suite/bugs/closed/shouldsucceed/1944.v |  9 +++++
 test-suite/bugs/closed/shouldsucceed/1951.v | 63 +++++++++++++++++++++++++++++
 test-suite/bugs/closed/shouldsucceed/1981.v |  2 +-
 test-suite/bugs/closed/shouldsucceed/2001.v | 10 +++--
 test-suite/bugs/closed/shouldsucceed/2017.v |  6 +--
 test-suite/bugs/closed/shouldsucceed/2083.v | 27 +++++++++++++
 test-suite/bugs/closed/shouldsucceed/2095.v | 19 +++++++++
 test-suite/bugs/closed/shouldsucceed/2108.v | 22 ++++++++++
 test-suite/bugs/closed/shouldsucceed/2117.v | 56 +++++++++++++++++++++++++
 test-suite/bugs/closed/shouldsucceed/2123.v | 11 +++++
 test-suite/bugs/closed/shouldsucceed/2127.v | 11 +++++
 test-suite/bugs/closed/shouldsucceed/2135.v |  9 +++++
 test-suite/bugs/closed/shouldsucceed/2136.v | 61 ++++++++++++++++++++++++++++
 test-suite/bugs/closed/shouldsucceed/2137.v | 52 ++++++++++++++++++++++++
 test-suite/bugs/closed/shouldsucceed/2139.v | 24 +++++++++++
 test-suite/bugs/closed/shouldsucceed/2145.v | 20 +++++++++
 test-suite/bugs/closed/shouldsucceed/2193.v | 31 ++++++++++++++
 test-suite/bugs/closed/shouldsucceed/2231.v |  3 ++
 test-suite/bugs/closed/shouldsucceed/2244.v | 19 +++++++++
 test-suite/bugs/closed/shouldsucceed/2255.v | 21 ++++++++++
 test-suite/bugs/closed/shouldsucceed/2281.v | 50 +++++++++++++++++++++++
 test-suite/bugs/closed/shouldsucceed/2295.v | 11 +++++
 test-suite/bugs/closed/shouldsucceed/2299.v | 13 ++++++
 test-suite/bugs/closed/shouldsucceed/2300.v | 15 +++++++
 test-suite/bugs/closed/shouldsucceed/335.v  |  5 +++
 test-suite/bugs/closed/shouldsucceed/38.v   |  2 +-
 test-suite/bugs/closed/shouldsucceed/846.v  | 10 ++---
 58 files changed, 741 insertions(+), 110 deletions(-)
 create mode 100644 test-suite/bugs/closed/shouldsucceed/1416.v
 create mode 100644 test-suite/bugs/closed/shouldsucceed/1711.v
 create mode 100644 test-suite/bugs/closed/shouldsucceed/1939.v
 create mode 100644 test-suite/bugs/closed/shouldsucceed/1944.v
 create mode 100644 test-suite/bugs/closed/shouldsucceed/1951.v
 create mode 100644 test-suite/bugs/closed/shouldsucceed/2083.v
 create mode 100644 test-suite/bugs/closed/shouldsucceed/2095.v
 create mode 100644 test-suite/bugs/closed/shouldsucceed/2108.v
 create mode 100644 test-suite/bugs/closed/shouldsucceed/2117.v
 create mode 100644 test-suite/bugs/closed/shouldsucceed/2123.v
 create mode 100644 test-suite/bugs/closed/shouldsucceed/2127.v
 create mode 100644 test-suite/bugs/closed/shouldsucceed/2135.v
 create mode 100644 test-suite/bugs/closed/shouldsucceed/2136.v
 create mode 100644 test-suite/bugs/closed/shouldsucceed/2137.v
 create mode 100644 test-suite/bugs/closed/shouldsucceed/2139.v
 create mode 100644 test-suite/bugs/closed/shouldsucceed/2145.v
 create mode 100644 test-suite/bugs/closed/shouldsucceed/2193.v
 create mode 100644 test-suite/bugs/closed/shouldsucceed/2231.v
 create mode 100644 test-suite/bugs/closed/shouldsucceed/2244.v
 create mode 100644 test-suite/bugs/closed/shouldsucceed/2255.v
 create mode 100644 test-suite/bugs/closed/shouldsucceed/2281.v
 create mode 100644 test-suite/bugs/closed/shouldsucceed/2295.v
 create mode 100644 test-suite/bugs/closed/shouldsucceed/2299.v
 create mode 100644 test-suite/bugs/closed/shouldsucceed/2300.v
 create mode 100644 test-suite/bugs/closed/shouldsucceed/335.v

(limited to 'test-suite/bugs/closed/shouldsucceed')

diff --git a/test-suite/bugs/closed/shouldsucceed/1100.v b/test-suite/bugs/closed/shouldsucceed/1100.v
index 6d619c74..32c78b4b 100644
--- a/test-suite/bugs/closed/shouldsucceed/1100.v
+++ b/test-suite/bugs/closed/shouldsucceed/1100.v
@@ -6,7 +6,7 @@ Parameter PQ : forall n, P n <-> Q n.
 
 Lemma PQ2 : forall n, P n -> Q n.
   intros.
-  rewrite PQ in H. 
+  rewrite PQ in H.
   trivial.
 Qed.
 
diff --git a/test-suite/bugs/closed/shouldsucceed/1322.v b/test-suite/bugs/closed/shouldsucceed/1322.v
index 7e21aa7c..1ec7d452 100644
--- a/test-suite/bugs/closed/shouldsucceed/1322.v
+++ b/test-suite/bugs/closed/shouldsucceed/1322.v
@@ -7,7 +7,7 @@ Variable I_eq :I -> I -> Prop.
 Variable I_eq_equiv : Setoid_Theory I I_eq.
 
 (* Add Relation I I_eq
-  reflexivity proved by I_eq_equiv.(Seq_refl I I_eq) 
+  reflexivity proved by I_eq_equiv.(Seq_refl I I_eq)
   symmetry proved by I_eq_equiv.(Seq_sym I I_eq)
   transitivity proved by I_eq_equiv.(Seq_trans I I_eq)
 as I_eq_relation. *)
diff --git a/test-suite/bugs/closed/shouldsucceed/1411.v b/test-suite/bugs/closed/shouldsucceed/1411.v
index e330d46f..a1a7b288 100644
--- a/test-suite/bugs/closed/shouldsucceed/1411.v
+++ b/test-suite/bugs/closed/shouldsucceed/1411.v
@@ -23,7 +23,7 @@ Program Fixpoint fetch t p (x:Exact t p) {struct t} :=
    match t, p with
    | No p' , nil      => p'
    | No p' , _::_     => unreachable nat _
-   | Br l r, nil      => unreachable nat _ 
+   | Br l r, nil      => unreachable nat _
    | Br l r, true::t  => fetch l t _
    | Br l r, false::t => fetch r t _
    end.
diff --git a/test-suite/bugs/closed/shouldsucceed/1414.v b/test-suite/bugs/closed/shouldsucceed/1414.v
index d3c00808..495a16bc 100644
--- a/test-suite/bugs/closed/shouldsucceed/1414.v
+++ b/test-suite/bugs/closed/shouldsucceed/1414.v
@@ -7,8 +7,8 @@ Inductive t : Set :=
   | Node : t -> data -> t -> Z -> t.
 
 Parameter avl : t -> Prop.
-Parameter bst : t -> Prop. 
-Parameter In : data -> t -> Prop. 
+Parameter bst : t -> Prop.
+Parameter In : data -> t -> Prop.
 Parameter cardinal : t -> nat.
 Definition card2 (s:t*t) := let (s1,s2) := s in cardinal s1 + cardinal s2.
 
@@ -16,26 +16,25 @@ Parameter split : data -> t -> t*(bool*t).
 Parameter join : t -> data -> t -> t.
 Parameter add : data -> t -> t.
 
-Program Fixpoint union 
-  (s:t*t)
-  (hb1: bst (fst s))(ha1: avl (fst s))(hb2: bst (snd s))(hb2: avl (snd s)) 
-  { measure card2 s } : 
-  {s' : t | bst s' /\ avl s' /\ forall x, In x s' <-> In x (fst s) \/ In x (snd
-s)} := 
-  match s with 
-    | (Leaf,t2) => t2
-    | (t1,Leaf) => t1
-    | (Node l1 v1 r1 h1, Node l2 v2 r2 h2) =>        
+Program Fixpoint union
+  (s u:t)
+  (hb1: bst s)(ha1: avl s)(hb2: bst u)(hb2: avl u)
+  { measure (cardinal s + cardinal u) } :
+  {s' : t | bst s' /\ avl s' /\ forall x, In x s' <-> In x s \/ In x u} :=
+  match s, u with
+    | Leaf,t2 => t2
+    | t1,Leaf => t1
+    | Node l1 v1 r1 h1, Node l2 v2 r2 h2 =>
         if (Z_ge_lt_dec h1 h2) then
-          if (Z_eq_dec h2 1) 
-          then add v2 (fst s)
+          if (Z_eq_dec h2 1)
+          then add v2 s
           else
-            let (l2', r2') := split v1 (snd s) in
-            join (union (l1,l2') _ _ _ _) v1 (union (r1,snd r2') _ _ _ _)
+            let (l2', r2') := split v1 u in
+            join (union l1 l2' _ _ _ _) v1 (union r1 (snd r2') _ _ _ _)
         else
-          if (Z_eq_dec h1 1) 
-          then add v1 (snd s) 
+          if (Z_eq_dec h1 1)
+          then add v1 s
           else
-            let (l1', r1') := split v2 (fst s) in
-            join (union (l1',l2) _ _ _ _) v2 (union (snd r1',r2) _ _ _ _)
-  end. 
+            let (l1', r1') := split v2 u in
+            join (union l1' l2 _ _ _ _) v2 (union (snd r1') r2 _ _ _ _)
+  end.
diff --git a/test-suite/bugs/closed/shouldsucceed/1416.v b/test-suite/bugs/closed/shouldsucceed/1416.v
new file mode 100644
index 00000000..da67d9b0
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1416.v
@@ -0,0 +1,27 @@
+Set Implicit Arguments.
+
+Record Place (Env A: Type) : Type := {
+  read: Env -> A ;
+  write: Env -> A -> Env ;
+  write_read: forall (e:Env), (write e (read e))=e
+}.
+
+Hint Rewrite -> write_read: placeeq.
+
+Record sumPl (Env A B: Type) (vL:(Place Env A)) (vR:(Place Env B)) : Type :=
+ {
+   mkEnv: A -> B -> Env ;
+   mkEnv2writeL: forall (e:Env) (x:A), (mkEnv x (read vR e))=(write vL e x)
+ }.
+
+(* when the following line is commented, the bug does not appear *)
+Hint Rewrite -> mkEnv2writeL: placeeq.
+
+Lemma autorewrite_raise_anomaly: forall (Env A:Type) (e: Env) (p:Place Env A),
+  (exists e1:Env, e=(write p e1 (read p e))).
+Proof.
+  intros Env A e p; eapply ex_intro.
+  autorewrite with placeeq. (* Here is the bug *)
+  auto.
+Qed.
+
diff --git a/test-suite/bugs/closed/shouldsucceed/1425.v b/test-suite/bugs/closed/shouldsucceed/1425.v
index 8e26209a..6be30174 100644
--- a/test-suite/bugs/closed/shouldsucceed/1425.v
+++ b/test-suite/bugs/closed/shouldsucceed/1425.v
@@ -1,4 +1,4 @@
-Require Import Setoid. 
+Require Import Setoid.
 
 Parameter recursion : forall A : Set, A -> (nat -> A -> A) -> nat -> A.
 
diff --git a/test-suite/bugs/closed/shouldsucceed/1446.v b/test-suite/bugs/closed/shouldsucceed/1446.v
index d4e7cea8..8cb2d653 100644
--- a/test-suite/bugs/closed/shouldsucceed/1446.v
+++ b/test-suite/bugs/closed/shouldsucceed/1446.v
@@ -1,8 +1,8 @@
 Lemma not_true_eq_false : forall (b:bool), b <> true -> b = false.
 Proof.
- destruct b;intros;trivial. 
- elim H. 
- exact (refl_equal true). 
+ destruct b;intros;trivial.
+ elim H.
+ exact (refl_equal true).
 Qed.
 
 Section BUG.
@@ -13,7 +13,7 @@ Section BUG.
  Hypothesis H1 : b <> true.
 
  Goal False.
-  rewrite (not_true_eq_false _ H) in * |-. 
+  rewrite (not_true_eq_false _ H) in * |-.
   contradiction.
  Qed.
 
diff --git a/test-suite/bugs/closed/shouldsucceed/1507.v b/test-suite/bugs/closed/shouldsucceed/1507.v
index b484c7dc..f1872a2b 100644
--- a/test-suite/bugs/closed/shouldsucceed/1507.v
+++ b/test-suite/bugs/closed/shouldsucceed/1507.v
@@ -2,16 +2,16 @@
    Implementing reals a la Stolzenberg
 
    Danko Ilik, March 2007
-   svn revision: $Id: 1507.v 10068 2007-08-10 12:06:59Z notin $
+   svn revision: $Id$
 
    XField.v -- (unfinished) axiomatisation of the theories of real and
                rational intervals.
 *)
 
-Definition associative (A:Type)(op:A->A->A) := 
+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) := 
+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) :=
@@ -19,7 +19,7 @@ Definition trichotomous (A:Type)(R:A->A->Prop) :=
 
 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) := 
+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.
 
@@ -52,7 +52,7 @@ Record I (grnd:Set)(le:grnd->grnd->Prop) : Type := Imake {
   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'', 
+  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 *)
@@ -70,7 +70,7 @@ Record I (grnd:Set)(le:grnd->grnd->Prop) : Type := Imake {
   Ic_sym    : symmetric _ Ic
 }.
 
-Definition interval_set (X:Set)(le:X->X->Prop) := 
+Definition interval_set (X:Set)(le:X->X->Prop) :=
   (interval X le) -> Prop. (* can be Set as well *)
 Check interval_set.
 Check Ic.
@@ -101,7 +101,7 @@ Record N (grnd:Set)(le:grnd->grnd->Prop)(grndI:I grnd le) : Type := Nmake {
   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'', 
+  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 *)
diff --git a/test-suite/bugs/closed/shouldsucceed/1568.v b/test-suite/bugs/closed/shouldsucceed/1568.v
index 9f10f749..3609e9c8 100644
--- a/test-suite/bugs/closed/shouldsucceed/1568.v
+++ b/test-suite/bugs/closed/shouldsucceed/1568.v
@@ -3,7 +3,7 @@ CoInductive A: Set :=
 with B: Set :=
   mk_B: A -> B.
 
-CoFixpoint a:A := mk_A b 
+CoFixpoint a:A := mk_A b
 with b:B := mk_B a.
 
 Goal b = match a with mk_A a1 => a1 end.
diff --git a/test-suite/bugs/closed/shouldsucceed/1576.v b/test-suite/bugs/closed/shouldsucceed/1576.v
index c9ebbd14..3621f7a1 100644
--- a/test-suite/bugs/closed/shouldsucceed/1576.v
+++ b/test-suite/bugs/closed/shouldsucceed/1576.v
@@ -13,8 +13,8 @@ End TC.
 Module Type TD.
 
 Declare Module B: TB .
-Declare Module C: TC 
-    with Module B := B  . 
+Declare Module C: TC
+    with Module B := B  .
 End TD.
 
 Module Type TE.
@@ -25,7 +25,7 @@ Module Type TF.
 Declare Module E:  TE.
 End TF.
 
-Module G (D: TD). 
+Module G (D: TD).
 Module B' := D.C.B.
 End G.
 
diff --git a/test-suite/bugs/closed/shouldsucceed/1582.v b/test-suite/bugs/closed/shouldsucceed/1582.v
index 47953a66..be5d3dd2 100644
--- a/test-suite/bugs/closed/shouldsucceed/1582.v
+++ b/test-suite/bugs/closed/shouldsucceed/1582.v
@@ -1,12 +1,12 @@
 Require Import Peano_dec.
 
-Definition fact_F : 
+Definition fact_F :
   forall (n:nat),
   (forall m, m<n -> nat) ->
   nat.
-refine 
+refine
   (fun n fact_rec =>
-     if eq_nat_dec n 0 then 
+     if eq_nat_dec n 0 then
         1
      else
         let fn := fact_rec (n-1) _ in
diff --git a/test-suite/bugs/closed/shouldsucceed/1618.v b/test-suite/bugs/closed/shouldsucceed/1618.v
index a90290bf..a9b067ce 100644
--- a/test-suite/bugs/closed/shouldsucceed/1618.v
+++ b/test-suite/bugs/closed/shouldsucceed/1618.v
@@ -6,7 +6,7 @@ Definition A_size (a: A) : nat :=
     | A1 n => 0
   end.
 
-Require Import Recdef. 
+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
diff --git a/test-suite/bugs/closed/shouldsucceed/1634.v b/test-suite/bugs/closed/shouldsucceed/1634.v
index e0c540f3..0150c250 100644
--- a/test-suite/bugs/closed/shouldsucceed/1634.v
+++ b/test-suite/bugs/closed/shouldsucceed/1634.v
@@ -18,7 +18,7 @@ Add Parametric Relation a : (S a) Seq
 
 Goal forall (a : A) (x y : S a), Seq x y -> Seq x y.
   intros a x y H.
-  setoid_replace x with y. 
+  setoid_replace x with y.
   reflexivity.
   trivial.
 Qed.
diff --git a/test-suite/bugs/closed/shouldsucceed/1643.v b/test-suite/bugs/closed/shouldsucceed/1643.v
index 4114987d..879a65b1 100644
--- a/test-suite/bugs/closed/shouldsucceed/1643.v
+++ b/test-suite/bugs/closed/shouldsucceed/1643.v
@@ -10,7 +10,6 @@ Definition decomp_func (s:Str) :=
 
 Theorem decomp s: s = decomp_func s.
 Proof.
-  intros s.
   case s; simpl; reflexivity.
 Qed.
 
diff --git a/test-suite/bugs/closed/shouldsucceed/1683.v b/test-suite/bugs/closed/shouldsucceed/1683.v
index 1571ee20..3e99694b 100644
--- a/test-suite/bugs/closed/shouldsucceed/1683.v
+++ b/test-suite/bugs/closed/shouldsucceed/1683.v
@@ -30,7 +30,7 @@ Add Parametric Relation A : (ms_type A) (ms_eq A)
 Hypothesis foobar : forall n, ms_eq CR (IRasCR (foo IR n)) (foo CRasCRing n).
 
 Goal forall (b:ms_type CR),
- ms_eq CR (IRasCR (foo IR O)) b -> 
+ ms_eq CR (IRasCR (foo IR O)) b ->
  ms_eq CR (IRasCR (foo IR O)) b.
 intros b H.
 rewrite foobar.
diff --git a/test-suite/bugs/closed/shouldsucceed/1711.v b/test-suite/bugs/closed/shouldsucceed/1711.v
new file mode 100644
index 00000000..e16612e3
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1711.v
@@ -0,0 +1,34 @@
+(* Test for evar map consistency - was failing at some point and was *)
+(* assumed to be solved from revision 10151 (but using a bad fix) *)
+
+Require Import List.
+Set Implicit Arguments.
+
+Inductive rose : Set := Rose : nat -> list rose -> rose.
+
+Section RoseRec.
+Variables (P: rose -> Set)(L: list rose -> Set).
+Hypothesis
+  (R: forall n rs, L rs -> P (Rose n rs))
+  (Lnil: L nil)
+  (Lcons: forall r rs, P r -> L rs -> L (cons r rs)).
+
+Fixpoint rose_rec2 (t:rose) {struct t} : P t :=
+  match t as x return P x with
+  | Rose n rs =>
+    R n ((fix rs_ind (l' : list rose): L l' :=
+         match l' as x return L x with
+         | nil => Lnil
+         | cons t tl => Lcons (rose_rec2 t) (rs_ind tl)
+         end)
+         rs)
+  end.
+End RoseRec.
+
+Lemma rose_map : rose -> rose.
+Proof. intro H; elim H using rose_rec2 with
+    (L:=fun _ => list rose); (* was assumed to fail here *)
+(*  (L:=fun (_:list rose) => list rose); *)
+  clear H; simpl; intros.
+  exact (Rose n rs). exact nil. exact (H::H0).
+Defined.
diff --git a/test-suite/bugs/closed/shouldsucceed/1738.v b/test-suite/bugs/closed/shouldsucceed/1738.v
index 0deed366..c2926a2b 100644
--- a/test-suite/bugs/closed/shouldsucceed/1738.v
+++ b/test-suite/bugs/closed/shouldsucceed/1738.v
@@ -5,10 +5,10 @@ Module SomeSetoids (Import M:FSetInterface.S).
 Lemma Equal_refl : forall s, s[=]s.
 Proof. red; split; auto. Qed.
 
-Add Relation t Equal 
- reflexivity proved by Equal_refl 
+Add Relation t Equal
+ reflexivity proved by Equal_refl
  symmetry proved by eq_sym
- transitivity proved by eq_trans 
+ transitivity proved by eq_trans
  as EqualSetoid.
 
 Add Morphism Empty with signature Equal ==> iff as Empty_m.
diff --git a/test-suite/bugs/closed/shouldsucceed/1740.v b/test-suite/bugs/closed/shouldsucceed/1740.v
index d9ce546a..ec4a7a6b 100644
--- a/test-suite/bugs/closed/shouldsucceed/1740.v
+++ b/test-suite/bugs/closed/shouldsucceed/1740.v
@@ -17,7 +17,7 @@ Goal f =
       | n, O => n
       | _, _ => O
     end.
-  unfold f. 
+  unfold f.
   reflexivity.
 Qed.
 
diff --git a/test-suite/bugs/closed/shouldsucceed/1775.v b/test-suite/bugs/closed/shouldsucceed/1775.v
index dab4120b..932949a3 100644
--- a/test-suite/bugs/closed/shouldsucceed/1775.v
+++ b/test-suite/bugs/closed/shouldsucceed/1775.v
@@ -13,7 +13,7 @@ Goal forall s k k' m,
   (pl k' (nexists (fun w => (nexists (fun b => pl (pair w w)
     (pl (pair s b)
     (nexists (fun w0 => (nexists (fun a => pl (pair b w0)
-      (nexists (fun w1 => (nexists (fun c => pl 
+      (nexists (fun w1 => (nexists (fun c => pl
         (pair a w1) (pl (pair a c) k))))))))))))))) m.
 intros.
 eapply plImp; [ | eauto | intros ].
diff --git a/test-suite/bugs/closed/shouldsucceed/1776.v b/test-suite/bugs/closed/shouldsucceed/1776.v
index abf85455..58491f9d 100644
--- a/test-suite/bugs/closed/shouldsucceed/1776.v
+++ b/test-suite/bugs/closed/shouldsucceed/1776.v
@@ -10,7 +10,7 @@ Definition nexists (P:nat -> nat -> Prop) : nat -> Prop :=
 
 Goal forall a A m,
   True ->
-  (pl A (nexists (fun x => (nexists 
+  (pl A (nexists (fun x => (nexists
     (fun y => pl (pair a (S x)) (pair a (S y))))))) m.
 Proof.
   intros.
diff --git a/test-suite/bugs/closed/shouldsucceed/1784.v b/test-suite/bugs/closed/shouldsucceed/1784.v
index 5855b168..718b0e86 100644
--- a/test-suite/bugs/closed/shouldsucceed/1784.v
+++ b/test-suite/bugs/closed/shouldsucceed/1784.v
@@ -56,16 +56,16 @@ Require Import Program.
 
 Program Fixpoint lt_dec (x y:sv) { struct x } : {slt x y}+{~slt x y} :=
   match x with
-    | I x => 
+    | I x =>
       match y with
         | I y => if (Z_eq_dec x y) then in_left else in_right
         | S ys => in_right
       end
-    | S xs => 
+    | S xs =>
       match y with
         | I y => in_right
         | S ys =>
-          let fix list_in (xs ys:list sv) {struct xs} : 
+          let fix list_in (xs ys:list sv) {struct xs} :
             {slist_in xs ys} + {~slist_in xs ys} :=
             match xs with
               | nil => in_left
@@ -76,8 +76,8 @@ Program Fixpoint lt_dec (x y:sv) { struct x } : {slt x y}+{~slt x y} :=
                     | y::ys => if lt_dec x y then in_left else if elem_in
                       ys then in_left else in_right
                   end
-                in 
-                if elem_in ys then 
+                in
+                if elem_in ys then
                   if list_in xs ys then in_left else in_right
                 else in_right
             end
@@ -90,12 +90,12 @@ Next Obligation. intro H; inversion H. Defined.
 Next Obligation. intro H; inversion H. Defined.
 Next Obligation. intro H; inversion H; subst. Defined.
 Next Obligation.
-  intro H1; contradict H. inversion H1; subst. assumption. 
+  intro H1; contradict H. inversion H1; subst. assumption.
   contradict H0; assumption. Defined.
 Next Obligation.
   intro H1; contradict H0. inversion H1; subst. assumption. Defined.
 Next Obligation.
-  intro H0; contradict H. inversion H0; subst. assumption. Defined.
+  intro H1; contradict H. inversion H1; subst. assumption. Defined.
 Next Obligation.
   intro H0; contradict H. inversion H0; subst; auto. Defined.
 
diff --git a/test-suite/bugs/closed/shouldsucceed/1791.v b/test-suite/bugs/closed/shouldsucceed/1791.v
index 694f056e..be0e8ae8 100644
--- a/test-suite/bugs/closed/shouldsucceed/1791.v
+++ b/test-suite/bugs/closed/shouldsucceed/1791.v
@@ -9,7 +9,7 @@ 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)   
+             |  S k' => fun A => X (Pow X k' A)
   end.
 
 Parameter Bush: k1.
diff --git a/test-suite/bugs/closed/shouldsucceed/1844.v b/test-suite/bugs/closed/shouldsucceed/1844.v
index 545f2615..5627612f 100644
--- a/test-suite/bugs/closed/shouldsucceed/1844.v
+++ b/test-suite/bugs/closed/shouldsucceed/1844.v
@@ -188,7 +188,7 @@ with exec_finish: function -> outcome -> store -> value -> store -> Prop :=
 
 with exec_function: function -> store -> value -> store -> Prop :=
  | exec_function_intro: forall f st out st1 v st',
-     exec f.(fn_body) st out st1 -> 
+     exec f.(fn_body) st out st1 ->
      exec_finish f out st1 v st' ->
      exec_function f st v st'.
 
diff --git a/test-suite/bugs/closed/shouldsucceed/1891.v b/test-suite/bugs/closed/shouldsucceed/1891.v
index 11124cdd..2d90a2f1 100644
--- a/test-suite/bugs/closed/shouldsucceed/1891.v
+++ b/test-suite/bugs/closed/shouldsucceed/1891.v
@@ -7,7 +7,7 @@
 
   Lemma L (x: T unit): (unit -> T unit) -> unit.
   Proof.
-    refine (fun x => match x return _ with mkT n => fun g => f (g _) end).
+    refine (match x return _ with mkT n => fun g => f (g _) end).
     trivial.
   Qed.
 
diff --git a/test-suite/bugs/closed/shouldsucceed/1901.v b/test-suite/bugs/closed/shouldsucceed/1901.v
index 598db366..7d86adbf 100644
--- a/test-suite/bugs/closed/shouldsucceed/1901.v
+++ b/test-suite/bugs/closed/shouldsucceed/1901.v
@@ -2,9 +2,9 @@ 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_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.
diff --git a/test-suite/bugs/closed/shouldsucceed/1905.v b/test-suite/bugs/closed/shouldsucceed/1905.v
index fb2725c9..8c81d751 100644
--- a/test-suite/bugs/closed/shouldsucceed/1905.v
+++ b/test-suite/bugs/closed/shouldsucceed/1905.v
@@ -5,7 +5,7 @@ Axiom t : Set.
 Axiom In : nat -> t -> Prop.
 Axiom InE : forall (x : nat) (s:t), impl (In x s) True.
 
-Goal forall a s, 
+Goal forall a s,
  In a s -> False.
 Proof.
  intros a s Ia.
diff --git a/test-suite/bugs/closed/shouldsucceed/1918.v b/test-suite/bugs/closed/shouldsucceed/1918.v
index 9d4a3e04..9d92fe12 100644
--- a/test-suite/bugs/closed/shouldsucceed/1918.v
+++ b/test-suite/bugs/closed/shouldsucceed/1918.v
@@ -35,7 +35,7 @@ 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 B:Set)(f g:A -> B),
         (forall a, f a = g a) -> forall r, h _ _ f r = h _ _ g r.
 
 (** first functor law *)
@@ -44,7 +44,7 @@ Definition fct1 (X:k1)(m: mon X) : Prop :=
 
 (** 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), 
+ 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
@@ -60,20 +60,20 @@ Definition pEFct (F:k2) : Type :=
   forall (X:k1), EFct X -> EFct (F X).
 
 
-(** we show some closure properties of pEFct, depending on such properties 
+(** 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.
+  intros 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.
+  intros ef1 ef2.
   apply (mkEFct(m:=moncomp (m ef1) (m ef2))); red; intros; unfold moncomp.
 (* prove ext *)
   apply (e ef1).
@@ -92,7 +92,7 @@ Proof.
   apply (f2 ef2).
 Defined.
 
-Corollary comppEFct (F G:k2): pEFct F -> pEFct G -> 
+Corollary comppEFct (F G:k2): pEFct F -> pEFct G ->
       pEFct (fun X A => F X (G X A)).
 Proof.
   red.
@@ -103,8 +103,8 @@ 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 
+  intros 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).
@@ -133,7 +133,7 @@ Proof.
   rewrite (f2 ef2); reflexivity.
 Defined.
 
-Corollary sumpEFct (F G:k2): pEFct F -> pEFct G -> 
+Corollary sumpEFct (F G:k2): pEFct F -> pEFct G ->
       pEFct (fun X A => F X A + G X A)%type.
 Proof.
   red.
@@ -144,8 +144,8 @@ 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 
+  intros 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 *)
@@ -168,7 +168,7 @@ Proof.
   apply (f2 ef2).
 Defined.
 
-Corollary prodpEFct (F G:k2): pEFct F -> pEFct G -> 
+Corollary prodpEFct (F G:k2): pEFct F -> pEFct G ->
       pEFct (fun X A => F X A * G X A)%type.
 Proof.
   red.
@@ -220,7 +220,6 @@ 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.
@@ -248,19 +247,19 @@ Module Type LNMIt_Type.
 
 Parameter F:k2.
 Parameter FpEFct: pEFct F.
-Parameter mu20: k1. 
+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), 
+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), 
+    (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)
@@ -327,8 +326,8 @@ Fixpoint Pow (X:k1)(k:nat){struct k}:k1:=
 
 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) 
+      with 0 => fun _ _ f  => f
+     |  S k' => fun _ _ f  => m _ _ (POW k' m f)
    end.
 
 Module Type BushkToList_Type.
diff --git a/test-suite/bugs/closed/shouldsucceed/1925.v b/test-suite/bugs/closed/shouldsucceed/1925.v
index 17eb721a..4caee1c3 100644
--- a/test-suite/bugs/closed/shouldsucceed/1925.v
+++ b/test-suite/bugs/closed/shouldsucceed/1925.v
@@ -3,14 +3,14 @@
 
 Require Import List.
 
-Definition compose (A B C : Type) (g : B -> C) (f : A -> B) : A -> C := 
+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 
+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 => 
+    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
diff --git a/test-suite/bugs/closed/shouldsucceed/1931.v b/test-suite/bugs/closed/shouldsucceed/1931.v
index bc8be78f..930ace1d 100644
--- a/test-suite/bugs/closed/shouldsucceed/1931.v
+++ b/test-suite/bugs/closed/shouldsucceed/1931.v
@@ -8,7 +8,7 @@ Inductive T (A:Set) : Set :=
 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. 
+ end.
 
 Fixpoint subst (A B:Set)(f:A -> T B)(t:T A) :T B :=
  match t with
@@ -19,7 +19,7 @@ Fixpoint subst (A B:Set)(f:A -> T B)(t:T A) :T B :=
 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): 
+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.
diff --git a/test-suite/bugs/closed/shouldsucceed/1935.v b/test-suite/bugs/closed/shouldsucceed/1935.v
index 641dcb7a..72396d49 100644
--- a/test-suite/bugs/closed/shouldsucceed/1935.v
+++ b/test-suite/bugs/closed/shouldsucceed/1935.v
@@ -1,14 +1,14 @@
 Definition f  (n:nat) := n = n.
 
 Lemma f_refl : forall n , f n.
-intros. reflexivity. 
+intros. reflexivity.
 Qed.
 
 Definition f'  (x:nat) (n:nat) := n = n.
 
 Lemma f_refl' : forall n , f' n n.
 Proof.
- intros. reflexivity. 
+ intros. reflexivity.
 Qed.
 
 Require Import ZArith.
diff --git a/test-suite/bugs/closed/shouldsucceed/1939.v b/test-suite/bugs/closed/shouldsucceed/1939.v
new file mode 100644
index 00000000..5e61529b
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1939.v
@@ -0,0 +1,19 @@
+Require Import Setoid Program.Basics.
+
+ Parameter P : nat -> Prop.
+ Parameter R : nat -> nat -> Prop.
+
+ Add Parametric Morphism : P
+   with signature R ++> impl as PM1.
+ Admitted.
+
+ Add Parametric Morphism : P
+   with signature R --> impl as PM2.
+ Admitted.
+
+ Goal forall x y, R x y -> P y -> P x.
+ Proof.
+   intros x y H1 H2.
+   rewrite H1.
+   auto.
+ Qed.
\ No newline at end of file
diff --git a/test-suite/bugs/closed/shouldsucceed/1944.v b/test-suite/bugs/closed/shouldsucceed/1944.v
new file mode 100644
index 00000000..ee2918c6
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1944.v
@@ -0,0 +1,9 @@
+(* Test some uses of ? in introduction patterns *)
+
+Inductive J : nat -> Prop :=
+  | K : forall p, J p -> (True /\ True)  -> J (S p).
+
+Lemma bug : forall n, J n -> J (S n).
+Proof.
+  intros ? H.
+  induction H as [? ? [? ?]].
diff --git a/test-suite/bugs/closed/shouldsucceed/1951.v b/test-suite/bugs/closed/shouldsucceed/1951.v
new file mode 100644
index 00000000..12c0ef9b
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1951.v
@@ -0,0 +1,63 @@
+
+(* First a simplification of the bug *)
+
+Set Printing Universes.
+
+Inductive enc (A:Type (*1*)) (* : Type.1 *) := C : A -> enc A.
+
+Definition id (X:Type(*5*)) (x:X) := x.
+
+Lemma test : let S := Type(*6 : 7*) in enc S -> S.
+simpl; intros.
+apply enc.
+apply id.
+apply Prop.
+Defined.
+
+(* Then the original bug *)
+
+Require Import List.
+
+Inductive a : Set := (* some dummy inductive *)
+b : (list a) -> a.   (* i don't know if this *)
+                     (* happens for smaller  *)
+                     (* ones                 *)
+
+Inductive sg : Type := Sg. (* single *)
+
+Definition ipl2 (P : a -> Type) :=   (* in Prop, that means P is true forall *)
+fold_right (fun x => prod (P x)) sg. (* the elements of a given list         *)
+
+Definition ind
+     : forall S : a -> Type,
+       (forall ls : list a, ipl2 S ls -> S (b ls)) -> forall s : a, S s :=
+fun (S : a -> Type)
+  (X : forall ls : list a, ipl2 S ls -> S (b ls)) =>
+fix ind2 (s : a) :=
+match s as a return (S a) with
+| b l =>
+    X l
+      (list_rect (fun l0 : list a => ipl2 S l0) Sg
+         (fun (a0 : a) (l0 : list a) (IHl : ipl2 S l0) =>
+          pair (ind2 a0) IHl) l)
+end. (* some induction principle *)
+
+Implicit Arguments ind [S].
+
+Lemma k : a -> Type. (* some ininteresting lemma *)
+intro;pattern H;apply ind;intros.
+  assert (K : Type).
+    induction ls.
+      exact sg.
+      exact sg.
+  exact (prod K sg).
+Defined.
+
+Lemma k' : a -> Type. (* same lemma but with our bug *)
+intro;pattern H;apply ind;intros.
+  apply prod.
+    induction ls.
+      exact sg.
+      exact sg.
+    exact sg. (* Proof complete *)
+Defined. (* bug *)
diff --git a/test-suite/bugs/closed/shouldsucceed/1981.v b/test-suite/bugs/closed/shouldsucceed/1981.v
index 0c3b96da..99952682 100644
--- a/test-suite/bugs/closed/shouldsucceed/1981.v
+++ b/test-suite/bugs/closed/shouldsucceed/1981.v
@@ -1,5 +1,5 @@
 Implicit Arguments ex_intro [A].
 
 Goal exists n : nat, True.
-  eapply ex_intro. exact 0. exact I. 
+  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
index 323021de..d0b3bf17 100644
--- a/test-suite/bugs/closed/shouldsucceed/2001.v
+++ b/test-suite/bugs/closed/shouldsucceed/2001.v
@@ -1,8 +1,10 @@
 (* Automatic computing of guard in "Theorem with"; check that guard is not
    computed when the user explicitly indicated it *)
 
+Unset Automatic Introduction.
+
 Inductive T : Set :=
-| v : T. 
+| v : T.
 
 Definition f (s:nat) (t:T) : nat.
 fix 2.
@@ -12,9 +14,9 @@ refine
   | v => s
   end.
 Defined.
-           
+
 Lemma test :
   forall s, f s v = s.
-Proof.    
+Proof.
 reflexivity.
-Qed.        
+Qed.
diff --git a/test-suite/bugs/closed/shouldsucceed/2017.v b/test-suite/bugs/closed/shouldsucceed/2017.v
index 948cea3e..df666148 100644
--- a/test-suite/bugs/closed/shouldsucceed/2017.v
+++ b/test-suite/bugs/closed/shouldsucceed/2017.v
@@ -8,8 +8,8 @@ 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 .      
+  Some _ => @choose _ H |_ => true
+end .
diff --git a/test-suite/bugs/closed/shouldsucceed/2083.v b/test-suite/bugs/closed/shouldsucceed/2083.v
new file mode 100644
index 00000000..a6ce4de0
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2083.v
@@ -0,0 +1,27 @@
+Require Import Program Arith.
+
+Program Fixpoint check_n  (n : nat) (P : { i | i < n } -> bool) (p : nat)
+  (H : forall (i : { i | i < n }), i < p -> P i = true)
+  {measure (n - p)} :
+  Exc (forall (p : { i | i < n}), P p = true) :=
+  match le_lt_dec n p with
+  | left _ => value _
+  | right cmp =>
+      if dec (P p) then
+        check_n n P (S p) _
+      else
+        error
+  end.
+
+Require Import Omega.
+
+Solve Obligations using program_simpl ; auto with *; try omega.
+
+Next Obligation.
+  apply H. simpl. omega.
+Defined.
+
+Next Obligation. 
+  case (le_lt_dec p i) ; intros. assert(i = p) by omega. subst.
+  revert H0. clear_subset_proofs. auto.
+  apply H. simpl. assumption. Defined.
diff --git a/test-suite/bugs/closed/shouldsucceed/2095.v b/test-suite/bugs/closed/shouldsucceed/2095.v
new file mode 100644
index 00000000..28ea99df
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2095.v
@@ -0,0 +1,19 @@
+(* Classes and sections *)
+
+Section OPT.
+  Variable A: Type.
+
+  Inductive MyOption: Type :=
+  | MyNone: MyOption
+  | MySome: A -> MyOption.
+
+  Class Opt: Type := {
+    f_opt: A -> MyOption
+  }.
+End OPT.
+
+Definition f_nat (n: nat):  MyOption nat := MySome _ n.
+
+Instance Nat_Opt: Opt nat := {
+  f_opt := f_nat
+}.
diff --git a/test-suite/bugs/closed/shouldsucceed/2108.v b/test-suite/bugs/closed/shouldsucceed/2108.v
new file mode 100644
index 00000000..cad8baa9
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2108.v
@@ -0,0 +1,22 @@
+(* Declare Module in Module Type *)
+Module Type A.
+Record t : Set := { something : unit }.
+End A.
+
+
+Module Type B.
+Declare Module BA : A.
+End B.
+
+
+Module Type C.
+Declare Module CA  : A.
+Declare Module CB : B with Module BA := CA.
+End C.
+
+
+Module Type D.
+Declare Module DA : A.
+(* Next line gives: "Anomaly: uncaught exception Not_found. Please report." *)
+Declare Module DC : C with Module CA := DA.
+End D.
diff --git a/test-suite/bugs/closed/shouldsucceed/2117.v b/test-suite/bugs/closed/shouldsucceed/2117.v
new file mode 100644
index 00000000..6377a8b7
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2117.v
@@ -0,0 +1,56 @@
+(* Check pattern-unification on evars in apply unification *)
+
+Axiom app : forall tau tau':Type, (tau -> tau') -> tau -> tau'.
+
+Axiom copy : forall tau:Type, tau -> tau -> Prop.
+Axiom copyr : forall tau:Type, tau -> tau -> Prop.
+Axiom copyf : forall tau:Type, tau -> tau -> Prop.
+Axiom eq : forall tau:Type, tau -> tau -> Prop.
+Axiom subst : forall tau tau':Type, (tau -> tau') -> tau -> tau' -> Prop.
+
+Axiom copy_atom : forall tau:Type, forall t t':tau, eq tau t t' -> copy tau t t'.
+Axiom copy_fun: forall tau tau':Type, forall t t':(tau->tau'),
+(forall x:tau, copyr tau x x->copy tau' (t x) (t' x))
+->copy (tau->tau') t t'.
+
+Axiom copyr_atom : forall tau:Type, forall t t':tau, copyr tau t t' -> eq tau t t'.
+Axiom copyr_fun: forall tau tau':Type, forall t t':(tau->tau'),
+copyr (tau->tau') t t'
+->(forall x y:tau, copy tau x y->copyr tau' (t x) (t' y)).
+
+Axiom copyf_atom : forall tau:Type, forall t t':tau, copyf tau t t' -> eq tau t t'.
+Axiom copyf_fun: forall tau tau':Type, forall t t':(tau->tau'),
+copyr (tau->tau') t t'
+->(forall x y:tau, forall z1 z2:tau',
+(copy tau x y)->
+(subst tau tau' t x z1)->
+(subst tau tau' t' y z2)->
+copyf tau' z1 z2).
+
+Axiom eqappg: forall tau tau':Type, forall t:tau->tau', forall q:tau, forall r:tau',forall t':tau',
+( ((subst tau tau' t q t') /\ (eq tau' t' r))
+->eq tau' (app tau tau' t q) r).
+
+Axiom eqappd: forall tau tau':Type, forall t:tau->tau', forall q:tau, forall r:tau',
+forall t':tau', ((subst tau tau' t q t') /\ (eq tau' r t'))
+->eq tau' r (app tau tau' t q).
+
+Axiom substcopy: forall tau tau':Type, forall t:tau->tau', forall q:tau, forall r:tau',
+(forall x:tau, (copyf tau x q) -> (copy tau' (t x) r))
+->subst tau tau' t q r.
+
+Ltac EtaLong := (apply copy_fun;intros;EtaLong)|| apply copy_atom.
+Ltac Subst := apply substcopy;intros;EtaLong.
+Ltac Rigid_aux := fun A => apply A|| Rigid_aux (copyr_fun _ _ _ _ A).
+Ltac Rigid := fun A => apply copyr_atom; Rigid_aux A.
+
+Theorem church0: forall i:Type, exists X:(i->i)->i->i,
+copy ((i->i)->i->i) (fun f:i->i => fun x:i=>f (X f x)) (fun f:i->i=>fun x:i=>app i i (X f) (f x)).
+intros.
+esplit.
+EtaLong.
+eapply eqappd;split.
+Subst.
+apply copyf_atom.
+Show Existentials.
+apply H1.
diff --git a/test-suite/bugs/closed/shouldsucceed/2123.v b/test-suite/bugs/closed/shouldsucceed/2123.v
new file mode 100644
index 00000000..422a2c12
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2123.v
@@ -0,0 +1,11 @@
+(* About the detection of non-dependent metas by the refine tactic *)
+
+(* The following is a simplification of bug #2123 *)
+
+Parameter fset : nat -> Set.
+Parameter widen : forall (n : nat) (s : fset n), { x : fset (S n) | s=s }.
+Goal forall i, fset (S i).
+intro.
+refine (proj1_sig (widen i _)).
+
+
diff --git a/test-suite/bugs/closed/shouldsucceed/2127.v b/test-suite/bugs/closed/shouldsucceed/2127.v
new file mode 100644
index 00000000..20ea4603
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2127.v
@@ -0,0 +1,11 @@
+(* Check that "apply refl_equal" is not exported as an interactive
+   tactic but as a statically globalized one *)
+
+(* (this is a simplification of the original bug report) *)
+
+Module A.
+Hint Rewrite sym_equal using apply refl_equal : foo.
+End A.
+
+
+
diff --git a/test-suite/bugs/closed/shouldsucceed/2135.v b/test-suite/bugs/closed/shouldsucceed/2135.v
new file mode 100644
index 00000000..61882176
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2135.v
@@ -0,0 +1,9 @@
+(* Check that metas are whd-normalized before trying 2nd-order unification *)
+Lemma test : 
+  forall (D:Type) (T : forall C, option C) (Q:forall D, option D -> Prop),
+  (forall (A : Type) (P : forall B:Type, option B -> Prop), P A (T A))
+  -> Q D (T D).
+Proof.
+  intros D T Q H.
+  pattern (T D). apply H.
+Qed.
diff --git a/test-suite/bugs/closed/shouldsucceed/2136.v b/test-suite/bugs/closed/shouldsucceed/2136.v
new file mode 100644
index 00000000..d2b926f3
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2136.v
@@ -0,0 +1,61 @@
+(* Bug #2136
+
+The fsetdec tactic seems to get confused by hypotheses like
+    HeqH1 : H1 = MkEquality s0 s1 b
+If I clear them then it is able to solve my goal; otherwise it is not.
+I would expect it to be able to solve the goal even without this hypothesis
+being cleared. A small, self-contained example is below.
+
+I have coq r12238.
+
+
+Thanks
+Ian
+*)
+
+
+Require Import FSets.
+Require Import Arith.
+Require Import FSetWeakList.
+
+Module DecidableNat.
+Definition t := nat.
+Definition eq := @eq nat.
+Definition eq_refl := @refl_equal nat.
+Definition eq_sym := @sym_eq nat.
+Definition eq_trans := @trans_eq nat.
+Definition eq_dec := eq_nat_dec.
+End DecidableNat.
+
+Module NatSet := Make(DecidableNat).
+
+Module Export Dec := WDecide (NatSet).
+Import FSetDecideAuxiliary.
+
+Parameter MkEquality : forall ( s0 s1 : NatSet.t )
+                              ( x : nat ),
+                       NatSet.Equal s1 (NatSet.add x s0).
+
+Lemma ThisLemmaWorks : forall ( s0 s1 : NatSet.t )
+                              ( a b : nat ),
+                       NatSet.In a s0
+                    -> NatSet.In a s1.
+Proof.
+intros.
+remember (MkEquality s0 s1 b) as H1.
+clear HeqH1.
+fsetdec.
+Qed.
+
+Lemma ThisLemmaWasFailing : forall ( s0 s1 : NatSet.t )
+                              ( a b : nat ),
+                       NatSet.In a s0
+                    -> NatSet.In a s1.
+Proof.
+intros.
+remember (MkEquality s0 s1 b) as H1.
+fsetdec.
+(*
+Error: Tactic failure: because the goal is beyond the scope of this tactic.
+*)
+Qed.
\ No newline at end of file
diff --git a/test-suite/bugs/closed/shouldsucceed/2137.v b/test-suite/bugs/closed/shouldsucceed/2137.v
new file mode 100644
index 00000000..6c2023ab
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2137.v
@@ -0,0 +1,52 @@
+(* Bug #2137
+
+The fsetdec tactic is sensitive to which way round the arguments to <> are.
+In the small, self-contained example below, it is able to solve the goal
+if it knows that "b <> a", but not if it knows that "a <> b". I would expect
+it to be able to solve hte goal in either case.
+
+I have coq r12238.
+
+
+Thanks
+Ian
+
+*)
+
+Require Import Arith FSets FSetWeakList.
+
+Module DecidableNat.
+Definition t := nat.
+Definition eq := @eq nat.
+Definition eq_refl := @refl_equal nat.
+Definition eq_sym := @sym_eq nat.
+Definition eq_trans := @trans_eq nat.
+Definition eq_dec := eq_nat_dec.
+End DecidableNat.
+
+Module NatSet := Make(DecidableNat).
+
+Module Export NameSetDec := WDecide (NatSet).
+
+Lemma ThisLemmaWorks : forall ( s0 : NatSet.t )
+                              ( a b : nat ),
+                       b <> a
+                    -> ~(NatSet.In a s0)
+                    -> ~(NatSet.In a (NatSet.add b s0)).
+Proof.
+intros.
+fsetdec.
+Qed.
+
+Lemma ThisLemmaWasFailing : forall ( s0 : NatSet.t )
+                              ( a b : nat ),
+                       a <> b
+                    -> ~(NatSet.In a s0)
+                    -> ~(NatSet.In a (NatSet.add b s0)).
+Proof.
+intros.
+fsetdec.
+(*
+Error: Tactic failure: because the goal is beyond the scope of this tactic.
+*)
+Qed.
\ No newline at end of file
diff --git a/test-suite/bugs/closed/shouldsucceed/2139.v b/test-suite/bugs/closed/shouldsucceed/2139.v
new file mode 100644
index 00000000..a7f35508
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2139.v
@@ -0,0 +1,24 @@
+(* Call of apply on <-> failed because of evars in elimination predicate *)
+Generalizable Variables patch.
+
+Class Patch (patch : Type) := {
+    commute : patch -> patch -> Prop
+}.
+
+Parameter flip : forall	`{patchInstance	: Patch	patch}
+                       	 {a b : patch},
+                 commute a b <-> commute b a.
+
+Lemma Foo : forall `{patchInstance : Patch patch}
+                    {a b : patch},
+            (commute a b)
+         -> True.
+Proof.
+intros.
+apply flip in H.
+
+(* failed in well-formed arity check because elimination predicate of
+   iff in (@flip _ _ _ _) had normalized evars while the ones in the
+   type of (@flip _ _ _ _) itself had non-normalized evars *)
+
+(* By the way, is the check necessary ? *)
diff --git a/test-suite/bugs/closed/shouldsucceed/2145.v b/test-suite/bugs/closed/shouldsucceed/2145.v
new file mode 100644
index 00000000..b6c5da65
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2145.v
@@ -0,0 +1,20 @@
+(* Test robustness of Groebner tactic in presence of disequalities *)
+
+Require Export Reals.
+Require Export NsatzR.
+
+Open Scope R_scope.
+
+Lemma essai :
+ forall yb xb m1 m2 xa ya,
+  xa <> xb ->
+ yb - 2 * m2 * xb = ya - m2 * xa -> 
+ yb - m1 * xb = ya - m1 * xa ->
+ yb - ya = (2 * xb - xa) * m2 -> 
+ yb - ya = (xb - xa) * m1.
+Proof.
+intros.
+(* clear H. groebner used not to work when H was not cleared *)
+nsatzR.
+Qed.
+
diff --git a/test-suite/bugs/closed/shouldsucceed/2193.v b/test-suite/bugs/closed/shouldsucceed/2193.v
new file mode 100644
index 00000000..fe258867
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2193.v
@@ -0,0 +1,31 @@
+(* Computation of dependencies in the "match" return predicate was incomplete *)
+(* Submitted by R. O'Connor, Nov 2009 *)
+
+Inductive Symbol : Set :=
+ | VAR : Symbol.
+
+Inductive SExpression :=
+ | atomic : Symbol -> SExpression.
+
+Inductive ProperExpr : SExpression -> SExpression -> Type :=
+ | pe_3 : forall (x : Symbol) (alpha : SExpression),
+    ProperExpr alpha (atomic VAR) ->
+    ProperExpr (atomic x) alpha.
+
+Definition A (P : forall s : SExpression, Type)
+ (x alpha alpha1 : SExpression)
+ (t : ProperExpr (x) alpha1) : option (x = atomic VAR) :=
+ match t as pe in ProperExpr a b return option (a = atomic VAR) with
+ | pe_3 x0 alpha3 tye' => 
+      (fun (x:Symbol) (alpha : SExpression) => @None (atomic x = atomic VAR))
+       x0 alpha3
+ end.
+
+Definition B (P : forall s : SExpression, Type)
+ (x alpha alpha1 : SExpression)
+ (t : ProperExpr (x) alpha1) : option (x = atomic VAR) :=
+ match t as pe in ProperExpr a b return option (a = atomic VAR) with
+ | pe_3 x0 alpha3 tye' => 
+      (fun (x:Symbol) (alpha : SExpression) (t:ProperExpr alpha (atomic VAR)) => @None (atomic x = atomic VAR))
+       x0 alpha3 tye'
+ end.
diff --git a/test-suite/bugs/closed/shouldsucceed/2231.v b/test-suite/bugs/closed/shouldsucceed/2231.v
new file mode 100644
index 00000000..03e2c9bb
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2231.v
@@ -0,0 +1,3 @@
+Inductive unit2 : Type := U : unit -> unit2.
+Inductive dummy (u: unit2) : unit -> Type :=
+          V: dummy u (let (tt) := u in tt).
diff --git a/test-suite/bugs/closed/shouldsucceed/2244.v b/test-suite/bugs/closed/shouldsucceed/2244.v
new file mode 100644
index 00000000..d499e515
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2244.v
@@ -0,0 +1,19 @@
+(* 1st-order unification did not work when in competition with pattern unif. *)
+
+Set Implicit Arguments.
+Lemma test : forall
+  (A : Type)
+  (B : Type)
+  (f : A -> B)
+  (S : B -> Prop)
+  (EV : forall y (f':A->B), (forall x', S (f' x')) -> S (f y))
+  (HS : forall x', S (f x'))
+  (x : A),
+  S (f x).
+Proof.
+  intros. eapply EV. intros. 
+  (* worked in v8.2 but not in v8.3beta, fixed in r12898 *)
+  apply HS.
+
+  (* still not compatible with 8.2 because an evar can be solved in
+     two different ways and is left open *)
diff --git a/test-suite/bugs/closed/shouldsucceed/2255.v b/test-suite/bugs/closed/shouldsucceed/2255.v
new file mode 100644
index 00000000..bf80ff66
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2255.v
@@ -0,0 +1,21 @@
+(* Check injection in presence of dependencies hidden in applicative terms *)
+
+Inductive TupleT : nat -> Type :=
+  nilT : TupleT 0
+| consT {n} A : (A -> TupleT n) -> TupleT (S n).
+
+Inductive Tuple : forall n, TupleT n -> Type :=
+  nil : Tuple _ nilT
+| cons {n} A (x : A) (F : A -> TupleT n) : Tuple _ (F x) -> Tuple _ (consT A F).
+
+Goal forall n A F x X n0 A0 x0 F0 H0 (H : existT (fun n0 : nat => {H0 : TupleT
+n0 & Tuple n0 H0}) 
+         (S n0)
+         (existT (fun H0 : TupleT (S n0) => Tuple (S n0) H0) 
+            (consT A0 F0) (cons A0 x0 F0 H0)) =
+       existT (fun n0 : nat => {H0 : TupleT n0 & Tuple n0 H0}) 
+         (S n)
+         (existT (fun H0 : TupleT (S n) => Tuple (S n) H0) 
+            (consT A F) (cons A x F X))), False.
+intros.
+injection H.
diff --git a/test-suite/bugs/closed/shouldsucceed/2281.v b/test-suite/bugs/closed/shouldsucceed/2281.v
new file mode 100644
index 00000000..40948d90
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2281.v
@@ -0,0 +1,50 @@
+(** Bug #2281
+
+In the code below, coq is confused by an equality unless it is first 'subst'ed
+away, yet http://coq.inria.fr/stdlib/Coq.FSets.FSetDecide.html says
+
+    fsetdec will first perform any necessary zeta and beta reductions and will
+invoke subst to eliminate any Coq equalities between finite sets or their
+elements.
+
+I have coq r12851.
+
+*)
+
+Require Import Arith.
+Require Import FSets.
+Require Import FSetWeakList.
+
+Module DecidableNat.
+Definition t := nat.
+Definition eq := @eq nat.
+Definition eq_refl := @refl_equal nat.
+Definition eq_sym := @sym_eq nat.
+Definition eq_trans := @trans_eq nat.
+Definition eq_dec := eq_nat_dec.
+End DecidableNat.
+
+Module NatSet := Make(DecidableNat).
+
+Module Export NameSetDec := WDecide (NatSet).
+
+Lemma ThisLemmaWorks : forall ( s1 s2 : NatSet.t )
+                              ( H : s1 = s2 ),
+                       NatSet.Equal s1 s2.
+Proof.
+intros.
+subst.
+fsetdec.
+Qed.
+
+Import FSetDecideAuxiliary.
+
+Lemma ThisLemmaWasFailing : forall ( s1 s2 : NatSet.t )
+                              ( H : s1 = s2 ),
+                       NatSet.Equal s1 s2.
+Proof.
+intros.
+fsetdec.
+(* Error: Tactic failure: because the goal is beyond the scope of this tactic.
+*)
+Qed.
\ No newline at end of file
diff --git a/test-suite/bugs/closed/shouldsucceed/2295.v b/test-suite/bugs/closed/shouldsucceed/2295.v
new file mode 100644
index 00000000..f5ca28dc
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2295.v
@@ -0,0 +1,11 @@
+(* Check if omission of "as" in return clause works w/ section variables too *)
+
+Section sec.
+
+Variable b: bool.
+
+Definition d' :=
+  (match b return b = true \/ b = false with
+  | true => or_introl _ (refl_equal true)
+  | false => or_intror _ (refl_equal false)
+  end).
diff --git a/test-suite/bugs/closed/shouldsucceed/2299.v b/test-suite/bugs/closed/shouldsucceed/2299.v
new file mode 100644
index 00000000..c0552ca7
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2299.v
@@ -0,0 +1,13 @@
+(* Check that destruct refreshes universes in what it generalizes *)
+
+Section test.
+
+Variable A: Type.
+
+Inductive T: unit -> Type := C: A -> unit -> T tt.
+
+Let unused := T tt.
+
+Goal T tt -> False.
+ intro X.
+ destruct X.
diff --git a/test-suite/bugs/closed/shouldsucceed/2300.v b/test-suite/bugs/closed/shouldsucceed/2300.v
new file mode 100644
index 00000000..4e587cbb
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2300.v
@@ -0,0 +1,15 @@
+(* Check some behavior of Ltac pattern-matching wrt universe levels *)
+
+Section contents.
+
+Variables (A: Type) (B: (unit -> Type) -> Type).
+
+Inductive C := c: A -> unit -> C.
+
+Let unused2 (x: unit) := C.
+
+Goal True.
+intuition.
+Qed.
+
+End contents.
diff --git a/test-suite/bugs/closed/shouldsucceed/335.v b/test-suite/bugs/closed/shouldsucceed/335.v
new file mode 100644
index 00000000..166fa7a9
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/335.v
@@ -0,0 +1,5 @@
+(* Compatibility of Require with backtracking at interactive module end *)
+
+Module A.
+Require List.
+End A.
diff --git a/test-suite/bugs/closed/shouldsucceed/38.v b/test-suite/bugs/closed/shouldsucceed/38.v
index 7bc04b1f..4fc8d7c9 100644
--- a/test-suite/bugs/closed/shouldsucceed/38.v
+++ b/test-suite/bugs/closed/shouldsucceed/38.v
@@ -6,7 +6,7 @@ Inductive liste : Set :=
 | vide : liste
 | c : A -> liste -> liste.
 
-Inductive e : A -> liste -> Prop := 
+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).
 
diff --git a/test-suite/bugs/closed/shouldsucceed/846.v b/test-suite/bugs/closed/shouldsucceed/846.v
index a963b225..ee5ec1fa 100644
--- a/test-suite/bugs/closed/shouldsucceed/846.v
+++ b/test-suite/bugs/closed/shouldsucceed/846.v
@@ -27,7 +27,7 @@ Definition index := list bool.
 
 Inductive L (A:Set) : index -> Set :=
   initL: A -> L A nil
-  | pluslL: forall l:index, One -> L A (false::l) 
+  | 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)
@@ -109,7 +109,7 @@ Proof.
   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). 
+       | inr t' => plusrL t' end)) r).
 Defined.
 
 Section minimal.
@@ -119,11 +119,11 @@ Hypothesis G: Set -> Set.
 Hypothesis step: sub1 (LamF' G) G.
 
 Fixpoint L'(A:Set)(i:index){struct i} : Set :=
-  match i with 
+  match i with
     nil => A
     | false::l => One + L' A l
     | true::l => G (L' A l)
-  end. 
+  end.
 
 Definition LinL': forall (A:Set)(i:index), L A i -> L' A i.
 Proof.
@@ -177,7 +177,7 @@ Proof.
   assumption.
   induction a.
   simpl L' in t.
-  apply (aczelapp (l1:=true::nil) (l2:=i)). 
+  apply (aczelapp (l1:=true::nil) (l2:=i)).
   exact (lam' IHi t).
   simpl L' in t.
   induction t.
-- 
cgit v1.2.3