From 97fefe1fcca363a1317e066e7f4b99b9c1e9987b Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Thu, 12 Jan 2012 16:02:20 +0100
Subject: Imported Upstream version 8.4~beta

---
 test-suite/bugs/closed/shouldsucceed/1416.v |   7 +-
 test-suite/bugs/closed/shouldsucceed/1507.v |   1 -
 test-suite/bugs/closed/shouldsucceed/1834.v | 174 ++++++++
 test-suite/bugs/closed/shouldsucceed/1912.v |   6 +
 test-suite/bugs/closed/shouldsucceed/1962.v |  55 +++
 test-suite/bugs/closed/shouldsucceed/2127.v |   3 -
 test-suite/bugs/closed/shouldsucceed/2141.v |  14 +
 test-suite/bugs/closed/shouldsucceed/2181.v |   3 +
 test-suite/bugs/closed/shouldsucceed/2304.v |   4 +
 test-suite/bugs/closed/shouldsucceed/2307.v |   3 +
 test-suite/bugs/closed/shouldsucceed/2320.v |  14 +
 test-suite/bugs/closed/shouldsucceed/2342.v |   8 +
 test-suite/bugs/closed/shouldsucceed/2362.v |  38 ++
 test-suite/bugs/closed/shouldsucceed/2378.v | 608 ++++++++++++++++++++++++++++
 test-suite/bugs/closed/shouldsucceed/2388.v |   6 +
 test-suite/bugs/closed/shouldsucceed/2393.v |  13 +
 test-suite/bugs/closed/shouldsucceed/2404.v |  46 +++
 test-suite/bugs/closed/shouldsucceed/2456.v |  53 +++
 test-suite/bugs/closed/shouldsucceed/2473.v |  39 ++
 test-suite/bugs/closed/shouldsucceed/2603.v |  18 +
 test-suite/bugs/closed/shouldsucceed/2613.v |  17 +
 test-suite/bugs/closed/shouldsucceed/2615.v |  14 +
 test-suite/bugs/closed/shouldsucceed/2616.v |   7 +
 test-suite/bugs/closed/shouldsucceed/2640.v |  17 +
 24 files changed, 1162 insertions(+), 6 deletions(-)
 create mode 100644 test-suite/bugs/closed/shouldsucceed/1834.v
 create mode 100644 test-suite/bugs/closed/shouldsucceed/1912.v
 create mode 100644 test-suite/bugs/closed/shouldsucceed/1962.v
 create mode 100644 test-suite/bugs/closed/shouldsucceed/2141.v
 create mode 100644 test-suite/bugs/closed/shouldsucceed/2181.v
 create mode 100644 test-suite/bugs/closed/shouldsucceed/2304.v
 create mode 100644 test-suite/bugs/closed/shouldsucceed/2307.v
 create mode 100644 test-suite/bugs/closed/shouldsucceed/2320.v
 create mode 100644 test-suite/bugs/closed/shouldsucceed/2342.v
 create mode 100644 test-suite/bugs/closed/shouldsucceed/2362.v
 create mode 100644 test-suite/bugs/closed/shouldsucceed/2378.v
 create mode 100644 test-suite/bugs/closed/shouldsucceed/2393.v
 create mode 100644 test-suite/bugs/closed/shouldsucceed/2404.v
 create mode 100644 test-suite/bugs/closed/shouldsucceed/2456.v
 create mode 100644 test-suite/bugs/closed/shouldsucceed/2473.v
 create mode 100644 test-suite/bugs/closed/shouldsucceed/2603.v
 create mode 100644 test-suite/bugs/closed/shouldsucceed/2613.v
 create mode 100644 test-suite/bugs/closed/shouldsucceed/2615.v
 create mode 100644 test-suite/bugs/closed/shouldsucceed/2616.v
 create mode 100644 test-suite/bugs/closed/shouldsucceed/2640.v

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

diff --git a/test-suite/bugs/closed/shouldsucceed/1416.v b/test-suite/bugs/closed/shouldsucceed/1416.v
index da67d9b0..ee092005 100644
--- a/test-suite/bugs/closed/shouldsucceed/1416.v
+++ b/test-suite/bugs/closed/shouldsucceed/1416.v
@@ -1,3 +1,8 @@
+(* In 8.1 autorewrite used to raised an anomaly here *)
+(* After resolution of the bug, autorewrite succeeded *)
+(* From forthcoming 8.4, autorewrite is forbidden to instantiate *)
+(* evars, so the new test just checks it is not an anomaly *)
+
 Set Implicit Arguments.
 
 Record Place (Env A: Type) : Type := {
@@ -22,6 +27,4 @@ Lemma autorewrite_raise_anomaly: forall (Env A:Type) (e: Env) (p:Place Env A),
 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/1507.v b/test-suite/bugs/closed/shouldsucceed/1507.v
index ea72ba89..f2ab9100 100644
--- a/test-suite/bugs/closed/shouldsucceed/1507.v
+++ b/test-suite/bugs/closed/shouldsucceed/1507.v
@@ -2,7 +2,6 @@
    Implementing reals a la Stolzenberg
 
    Danko Ilik, March 2007
-   svn revision: $Id: 1507.v 12337 2009-09-17 15:58:14Z glondu $
 
    XField.v -- (unfinished) axiomatisation of the theories of real and
                rational intervals.
diff --git a/test-suite/bugs/closed/shouldsucceed/1834.v b/test-suite/bugs/closed/shouldsucceed/1834.v
new file mode 100644
index 00000000..947d15f0
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1834.v
@@ -0,0 +1,174 @@
+(* This tests rather deep nesting of abstracted terms *)
+
+(* This used to fail before Nov 2011 because of a de Bruijn indice bug
+   in extract_predicate.
+
+   Note: use of eq_ok allows shorten notations but was not in the
+   original example
+*)
+
+Scheme eq_rec_dep := Induction for eq Sort Type.
+
+Section Teq.
+
+Variable P0:           Type.
+Variable P1: forall (y0:P0), Type.
+Variable P2: forall y0 (y1:P1 y0), Type.
+Variable P3: forall y0 y1 (y2:P2 y0 y1), Type.
+Variable P4: forall y0 y1 y2 (y3:P3 y0 y1 y2), Type.
+Variable P5: forall y0 y1 y2 y3 (y4:P4 y0 y1 y2 y3), Type.
+
+Variable x0:P0.
+
+Inductive eq0 : P0 -> Prop :=
+  refl0: eq0 x0.
+
+Definition eq_0 y0 := x0 = y0.
+
+Variable x1:P1 x0.
+
+Inductive eq1 : forall y0, P1 y0 -> Prop :=
+  refl1: eq1 x0 x1.
+
+Definition S0_0 y0 (e0:eq_0 y0) :=
+  eq_rec_dep P0 x0 (fun y0 e0 => P1 y0) x1 y0 e0.
+
+Definition eq_ok0 y0 y1 (E: eq_0 y0) := S0_0 y0 E = y1.
+
+Definition eq_1 y0 y1 :=
+  {E0:eq_0 y0 | eq_ok0 y0 y1 E0}.
+
+Variable x2:P2 x0 x1.
+
+Inductive eq2 :
+forall y0 y1, P2 y0 y1 -> Prop :=
+refl2: eq2 x0 x1 x2.
+
+Definition S1_0 y0 (e0:eq_0 y0) :=
+eq_rec_dep P0 x0 (fun y0 e0 => P2 y0 (S0_0 y0 e0)) x2 y0 e0.
+
+Definition S1_1 y0 y1 (e0:eq_0 y0) (e1:S0_0 y0 e0 = y1) :=
+  eq_rec_dep (P1 y0) (S0_0 y0 e0) (fun y1 e1 => P2 y0 y1)
+   (S1_0 y0 e0)
+   y1 e1.
+
+Definition eq_ok1 y0 y1 y2 (E: eq_1 y0 y1) :=
+  match E with exist e0 e1 => S1_1 y0 y1 e0 e1 = y2 end.
+
+Definition eq_2 y0 y1 y2 :=
+  {E1:eq_1 y0 y1 | eq_ok1 y0 y1 y2 E1}.
+
+Variable x3:P3 x0 x1 x2.
+
+Inductive eq3 :
+forall y0 y1 y2, P3 y0 y1 y2 -> Prop :=
+refl3: eq3 x0 x1 x2 x3.
+
+Definition S2_0 y0 (e0:eq_0 y0) :=
+eq_rec_dep P0 x0 (fun y0 e0 => P3 y0 (S0_0 y0 e0) (S1_0 y0 e0)) x3 y0 e0.
+
+Definition S2_1 y0 y1 (e0:eq_0 y0) (e1:S0_0 y0 e0 = y1) :=
+  eq_rec_dep (P1 y0) (S0_0 y0 e0)
+   (fun y1 e1 => P3 y0 y1 (S1_1 y0 y1 e0 e1))
+   (S2_0 y0 e0)
+   y1 e1.
+
+Definition S2_2 y0 y1 y2 (e0:eq_0 y0) (e1:S0_0 y0 e0 = y1)
+  (e2:S1_1 y0 y1 e0 e1 = y2) :=
+  eq_rec_dep (P2 y0 y1) (S1_1 y0 y1 e0 e1)
+   (fun y2 e2 => P3 y0 y1 y2)
+   (S2_1 y0 y1 e0 e1)
+   y2 e2.
+
+Definition eq_ok2 y0 y1 y2 y3 (E: eq_2 y0 y1 y2) : Prop :=
+  match E with exist (exist e0 e1) e2 =>
+     S2_2 y0 y1 y2 e0 e1 e2 = y3 end.
+
+Definition eq_3 y0 y1 y2 y3 :=
+  {E2: eq_2 y0 y1 y2 | eq_ok2 y0 y1 y2 y3 E2}.
+
+Variable x4:P4 x0 x1 x2 x3.
+
+Inductive eq4 :
+forall y0 y1 y2 y3, P4 y0 y1 y2 y3 -> Prop :=
+refl4: eq4 x0 x1 x2 x3 x4.
+
+Definition S3_0 y0 (e0:eq_0 y0) :=
+eq_rec_dep P0 x0 (fun y0 e0 => P4 y0 (S0_0 y0 e0) (S1_0 y0 e0) (S2_0 y0 e0))
+  x4 y0 e0.
+
+Definition S3_1 y0 y1 (e0:eq_0 y0) (e1:S0_0 y0 e0 = y1) :=
+  eq_rec_dep (P1 y0) (S0_0 y0 e0)
+   (fun y1 e1 => P4 y0 y1 (S1_1 y0 y1 e0 e1) (S2_1 y0 y1 e0 e1))
+   (S3_0 y0 e0)
+   y1 e1.
+
+Definition S3_2 y0 y1 y2 (e0:eq_0 y0) (e1:S0_0 y0 e0 = y1)
+  (e2:S1_1 y0 y1 e0 e1 = y2) :=
+  eq_rec_dep (P2 y0 y1) (S1_1 y0 y1 e0 e1)
+   (fun y2 e2 => P4 y0 y1 y2 (S2_2 y0 y1 y2 e0 e1 e2))
+   (S3_1 y0 y1 e0 e1)
+   y2 e2.
+
+Definition S3_3 y0 y1 y2 y3 (e0:eq_0 y0) (e1:S0_0 y0 e0 = y1)
+  (e2:S1_1 y0 y1 e0 e1 = y2) (e3:S2_2 y0 y1 y2 e0 e1 e2 = y3):=
+  eq_rec_dep (P3 y0 y1 y2) (S2_2 y0 y1 y2 e0 e1 e2)
+   (fun y3 e3 => P4 y0 y1 y2 y3)
+   (S3_2 y0 y1 y2 e0 e1 e2)
+   y3 e3.
+
+Definition eq_ok3 y0 y1 y2 y3 y4 (E: eq_3 y0 y1 y2 y3) : Prop :=
+  match E with exist (exist (exist e0 e1) e2) e3 =>
+     S3_3 y0 y1 y2 y3 e0 e1 e2 e3 = y4 end.
+
+Definition eq_4 y0 y1 y2 y3 y4 :=
+  {E3: eq_3 y0 y1 y2 y3 | eq_ok3 y0 y1 y2 y3 y4 E3}.
+
+Variable x5:P5 x0 x1 x2 x3 x4.
+
+Inductive eq5 :
+forall y0 y1 y2 y3 y4, P5 y0 y1 y2 y3 y4 -> Prop :=
+refl5: eq5 x0 x1 x2 x3 x4 x5.
+
+Definition S4_0 y0 (e0:eq_0 y0) :=
+eq_rec_dep P0 x0
+(fun y0 e0 => P5 y0 (S0_0 y0 e0) (S1_0 y0 e0) (S2_0 y0 e0) (S3_0 y0 e0))
+  x5 y0 e0.
+
+Definition S4_1 y0 y1 (e0:eq_0 y0) (e1:S0_0 y0 e0 = y1) :=
+  eq_rec_dep (P1 y0) (S0_0 y0 e0)
+   (fun y1 e1 => P5 y0 y1 (S1_1 y0 y1 e0 e1) (S2_1 y0 y1 e0 e1) (S3_1 y0 y1 e0
+e1))
+   (S4_0 y0 e0)
+   y1 e1.
+
+Definition S4_2 y0 y1 y2 (e0:eq_0 y0) (e1:S0_0 y0 e0 = y1)
+  (e2:S1_1 y0 y1 e0 e1 = y2) :=
+  eq_rec_dep (P2 y0 y1) (S1_1 y0 y1 e0 e1)
+   (fun y2 e2 => P5 y0 y1 y2 (S2_2 y0 y1 y2 e0 e1 e2) (S3_2 y0 y1 y2 e0 e1 e2))
+   (S4_1 y0 y1 e0 e1)
+   y2 e2.
+
+Definition S4_3 y0 y1 y2 y3 (e0:eq_0 y0) (e1:S0_0 y0 e0 = y1)
+  (e2:S1_1 y0 y1 e0 e1 = y2) (e3:S2_2 y0 y1 y2 e0 e1 e2 = y3):=
+  eq_rec_dep (P3 y0 y1 y2) (S2_2 y0 y1 y2 e0 e1 e2)
+   (fun y3 e3 => P5 y0 y1 y2 y3 (S3_3 y0 y1 y2 y3 e0 e1 e2 e3))
+   (S4_2 y0 y1 y2 e0 e1 e2)
+   y3 e3.
+
+Definition S4_4 y0 y1 y2 y3 y4 (e0:eq_0 y0) (e1:S0_0 y0 e0 = y1)
+  (e2:S1_1 y0 y1 e0 e1 = y2) (e3:S2_2 y0 y1 y2 e0 e1 e2 = y3)
+  (e4:S3_3 y0 y1 y2 y3 e0 e1 e2 e3 = y4) :=
+  eq_rec_dep (P4 y0 y1 y2 y3) (S3_3 y0 y1 y2 y3 e0 e1 e2 e3)
+   (fun y4 e4 => P5 y0 y1 y2 y3 y4)
+   (S4_3 y0 y1 y2 y3 e0 e1 e2 e3)
+   y4 e4.
+
+Definition eq_ok4 y0 y1 y2 y3 y4 y5 (E: eq_4 y0 y1 y2 y3 y4) : Prop :=
+  match E with exist (exist (exist (exist e0 e1) e2) e3) e4 =>
+     S4_4 y0 y1 y2 y3 y4 e0 e1 e2 e3 e4 = y5 end.
+
+Definition eq_5 y0 y1 y2 y3 y4 y5 :=
+  {E4: eq_4 y0 y1 y2 y3 y4 | eq_ok4 y0 y1 y2 y3 y4 y5 E4 }.
+
+End Teq.
diff --git a/test-suite/bugs/closed/shouldsucceed/1912.v b/test-suite/bugs/closed/shouldsucceed/1912.v
new file mode 100644
index 00000000..987a5417
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1912.v
@@ -0,0 +1,6 @@
+Require Import ZArith.
+
+Goal forall x, Z.succ (Z.pred x) = x.
+intros x.
+omega.
+Qed.
diff --git a/test-suite/bugs/closed/shouldsucceed/1962.v b/test-suite/bugs/closed/shouldsucceed/1962.v
new file mode 100644
index 00000000..a6b0fee5
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1962.v
@@ -0,0 +1,55 @@
+(* Bug 1962.v
+
+Bonjour,
+
+J'ai un exemple de lemme que j'arrivais à prouver avec fsetdec avec la 8.2beta3
+avec la beta4 et la version svn 11447 branche 8.2 çà diverge.
+
+Voici l'exemple en question, l'exmple test2 marche bien dans les deux version,
+test en revanche pose probleme:
+
+*)
+
+Require Export FSets.
+
+(** This module takes a decidable type and
+build finite sets of this type, tactics and defs *)
+
+Module BuildFSets (DecPoints: UsualDecidableType).
+
+Module Export FiniteSetsOfPoints := FSetWeakList.Make DecPoints.
+Module Export FiniteSetsOfPointsProperties :=
+ WProperties FiniteSetsOfPoints.
+Module Export Dec := WDecide FiniteSetsOfPoints.
+Module Export FM := Dec.F.
+
+Definition set_of_points := t.
+Definition Point := DecPoints.t.
+
+Definition couple(x y :Point) : set_of_points :=
+add x (add y empty).
+
+Definition triple(x y t :Point): set_of_points :=
+add x (add y (add t empty)).
+
+Lemma test : forall P A B C A' B' C',
+Equal
+(union (singleton P) (union (triple A B C) (triple A' B' C')))
+(union (triple P B B') (union (couple P A) (triple C A' C'))).
+Proof.
+intros.
+unfold triple, couple.
+Time fsetdec. (* works in 8.2 beta 3, not in beta 4 and final 8.2 *)
+              (* appears to works again in 8.3 and trunk, take 4-6 seconds *)
+Qed.
+
+Lemma test2 : forall A B C,
+Equal
+ (union (singleton C) (couple A B)) (triple A B C).
+Proof.
+intros.
+unfold triple, couple.
+Time fsetdec.
+Qed.
+
+End BuildFSets.
\ No newline at end of file
diff --git a/test-suite/bugs/closed/shouldsucceed/2127.v b/test-suite/bugs/closed/shouldsucceed/2127.v
index 20ea4603..0fc854b6 100644
--- a/test-suite/bugs/closed/shouldsucceed/2127.v
+++ b/test-suite/bugs/closed/shouldsucceed/2127.v
@@ -6,6 +6,3 @@
 Module A.
 Hint Rewrite sym_equal using apply refl_equal : foo.
 End A.
-
-
-
diff --git a/test-suite/bugs/closed/shouldsucceed/2141.v b/test-suite/bugs/closed/shouldsucceed/2141.v
new file mode 100644
index 00000000..941ae530
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2141.v
@@ -0,0 +1,14 @@
+Require Import FSetList.
+Require Import OrderedTypeEx.
+
+Module NatSet := FSetList.Make (Nat_as_OT).
+Recursive Extraction NatSet.fold.
+
+Module FSetHide (X : FSetInterface.S).
+  Include X.
+End FSetHide.
+
+Module NatSet' := FSetHide NatSet.
+Recursive Extraction NatSet'.fold.
+
+(* Extraction "test2141.ml" NatSet'.fold. *)
\ No newline at end of file
diff --git a/test-suite/bugs/closed/shouldsucceed/2181.v b/test-suite/bugs/closed/shouldsucceed/2181.v
new file mode 100644
index 00000000..62820d86
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2181.v
@@ -0,0 +1,3 @@
+Class C.
+Parameter P: C -> Prop.
+Fail Record R: Type := { _: C; u: P _ }.
diff --git a/test-suite/bugs/closed/shouldsucceed/2304.v b/test-suite/bugs/closed/shouldsucceed/2304.v
new file mode 100644
index 00000000..1ac2702b
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2304.v
@@ -0,0 +1,4 @@
+(* This used to fail with an anomaly NotASort at some time *)
+Class A (O: Type): Type := a: O -> Type.
+Fail Goal forall (x: a tt), @a x = @a x.
+
diff --git a/test-suite/bugs/closed/shouldsucceed/2307.v b/test-suite/bugs/closed/shouldsucceed/2307.v
new file mode 100644
index 00000000..7c049495
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2307.v
@@ -0,0 +1,3 @@
+Inductive V: nat -> Type := VS n: V (S n).
+Definition f (e: V 1): nat := match e with VS 0 => 3 end.
+
diff --git a/test-suite/bugs/closed/shouldsucceed/2320.v b/test-suite/bugs/closed/shouldsucceed/2320.v
new file mode 100644
index 00000000..facb9ecf
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2320.v
@@ -0,0 +1,14 @@
+(* Managing metavariables in the return clause of a match *)
+
+(* This was working in 8.1 but is failing in 8.2 and 8.3. It works in
+   trunk thanks to the new proof engine. It could probably made to work in
+   8.2 and 8.3 if a return predicate of the form "dummy 0" instead of
+   (or in addition to) a sophisticated predicate of the form 
+   "as x in dummy y return match y with 0 => ?P | _ => ID end" *)
+
+Inductive dummy : nat -> Prop := constr : dummy 0.
+
+Lemma failure : forall (x : dummy 0), x = constr.
+Proof.
+intros x.
+refine (match x with constr => _ end).
diff --git a/test-suite/bugs/closed/shouldsucceed/2342.v b/test-suite/bugs/closed/shouldsucceed/2342.v
new file mode 100644
index 00000000..094e5466
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2342.v
@@ -0,0 +1,8 @@
+(* Checking that the type inference algoithme does not commit to an
+   equality over sorts when only a subtyping constraint is around *)
+
+Parameter A : Set.
+Parameter B : A -> Set.
+Parameter F : Set -> Prop. 
+Check (F (forall x, B x)). 
+
diff --git a/test-suite/bugs/closed/shouldsucceed/2362.v b/test-suite/bugs/closed/shouldsucceed/2362.v
new file mode 100644
index 00000000..febb9c7b
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2362.v
@@ -0,0 +1,38 @@
+Set Implicit Arguments.
+
+Class Pointed (M:Type -> Type) := 
+{
+  creturn: forall {A: Type}, A -> M A
+}.
+
+Unset Implicit Arguments.
+Inductive FPair (A B:Type) (neutral: B) : Type:=
+ fpair : forall (a:A) (b:B), FPair A B neutral.
+Implicit Arguments fpair [[A] [B] [neutral]].
+
+Set Implicit Arguments.
+
+Notation "( x ,> y )" := (fpair x y) (at level 0).
+
+Instance Pointed_FPair B neutral:
+ Pointed (fun A => FPair A B neutral) :=
+ { creturn := fun A (a:A) => (a,> neutral) }.
+Definition blah_fail (x:bool) : FPair bool nat O :=
+  creturn x.
+Set Printing All. Print blah_fail.
+
+Definition blah_explicit (x:bool) : FPair bool nat O :=
+  @creturn _ (Pointed_FPair _ ) _ x.
+
+Print blah_explicit.
+
+
+Instance Pointed_FPair_mono:
+ Pointed (fun A => FPair A nat 0) :=
+ { creturn := fun A (a:A) => (a,> 0) }.
+
+
+Definition blah (x:bool) : FPair bool nat O :=
+  creturn x.
+
+
diff --git a/test-suite/bugs/closed/shouldsucceed/2378.v b/test-suite/bugs/closed/shouldsucceed/2378.v
new file mode 100644
index 00000000..7deec64d
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2378.v
@@ -0,0 +1,608 @@
+(* test with Coq 8.3rc1 *)
+
+Require Import Program.
+
+Inductive Unit: Set := unit: Unit.
+
+Definition eq_dec T := forall x y:T, {x=y}+{x<>y}.
+
+Section TTS_TASM.
+
+Variable Time: Set.
+Variable Zero: Time.
+Variable tle: Time -> Time -> Prop.
+Variable tlt: Time -> Time -> Prop.
+Variable tadd: Time -> Time -> Time.
+Variable tsub: Time -> Time -> Time.
+Variable tmin: Time -> Time -> Time.
+Notation "t1 @<= t2" := (tle t1 t2) (at level 70, no associativity).
+Notation "t1 @< t2" := (tlt t1 t2) (at level 70, no associativity).
+Notation "t1 @+ t2" := (tadd t1 t2) (at level 50, left associativity).
+Notation "t1 @- t2" := (tsub t1 t2) (at level 50, left associativity).
+Notation "t1 @<= t2 @<= t3" := ((tle t1 t2) /\ (tle t2 t3)) (at level 70, t2 at next level).
+Notation "t1 @<= t2 @< t3" := ((tle t1 t2) /\ (tlt t2 t3)) (at level 70, t2 at next level).
+
+Variable tzerop: forall n, (n = Zero) + {Zero @< n}.
+Variable tlt_eq_gt_dec: forall x y, {x @< y} + {x=y} + {y @< x}.
+Variable tle_plus_l: forall n m, n @<= n @+ m.
+Variable tle_lt_eq_dec: forall n m, n @<= m -> {n @< m} + {n = m}.
+
+Variable tzerop_zero: tzerop Zero = inleft (Zero @< Zero) (@eq_refl _ Zero).
+Variable tplus_n_O: forall n, n @+ Zero = n.
+Variable tlt_le_weak: forall n m, n @< m -> n @<= m.
+Variable tlt_irrefl: forall n, ~ n @< n.
+Variable tplus_nlt: forall n m, ~n @+ m @< n.
+Variable tle_n: forall n, n @<= n.
+Variable tplus_lt_compat_l: forall n m p, n @< m -> p @+ n @< p @+ m.
+Variable tlt_trans: forall n m p, n @< m -> m @< p -> n @< p.
+Variable tle_lt_trans: forall n m p, n @<= m -> m @< p -> n @< p.
+Variable tlt_le_trans: forall n m p, n @< m -> m @<= p -> n @< p.
+Variable tle_refl: forall n, n @<= n.
+Variable tplus_le_0: forall n m, n @+ m @<= n -> m = Zero.
+Variable Time_eq_dec: eq_dec Time.
+
+(*************************************************************)
+
+Section PropLogic.
+Variable Predicate: Type.
+
+Inductive LP: Type :=
+  LPPred: Predicate -> LP
+| LPAnd: LP -> LP -> LP
+| LPNot: LP -> LP.
+
+Variable State: Type.
+Variable Sat: State -> Predicate -> Prop.
+
+Fixpoint lpSat st f: Prop :=
+  match f with
+    LPPred p => Sat st p
+  | LPAnd f1 f2 => lpSat st f1 /\ lpSat st f2
+  | LPNot f1 => ~lpSat st f1
+  end.
+End PropLogic.
+
+Implicit Arguments lpSat.
+
+Fixpoint LPTransfo Pred1 Pred2 p2lp (f: LP Pred1): LP Pred2 :=
+  match f with
+    LPPred p => p2lp p
+  | LPAnd f1 f2 => LPAnd _ (LPTransfo Pred1 Pred2 p2lp f1) (LPTransfo Pred1 Pred2 p2lp f2)
+  | LPNot f1 => LPNot _ (LPTransfo Pred1 Pred2 p2lp f1)
+  end.
+Implicit Arguments LPTransfo.
+
+Definition addIndex (Ind:Type) (Pred: Ind -> Type) (i: Ind) f := 
+  LPTransfo (fun p => LPPred _ (existT (fun i => Pred i) i p)) f.
+
+Section TTS.
+
+Variable State: Type.
+
+Record TTS: Type := mkTTS {
+  Init: State -> Prop;
+  Delay: State -> Time -> State -> Prop;
+  Next: State -> State -> Prop;
+  Predicate: Type;
+  Satisfy: State -> Predicate -> Prop
+}.
+
+Definition TTSIndexedProduct Ind (tts: Ind -> TTS): TTS := mkTTS
+  (fun st => forall i, Init (tts i) st)
+  (fun st d st' => forall i, Delay (tts i) st d st')
+  (fun st st' => forall i, Next (tts i) st st')
+  { i: Ind & Predicate (tts i) }
+  (fun st p => Satisfy (tts (projT1 p)) st (projT2 p)).
+
+End TTS.
+
+Section SIMU_F.
+
+Variables StateA StateC: Type.
+
+Record mapping: Type := mkMapping {
+  mState: Type;
+  mInit: StateC -> mState;
+  mNext: mState -> StateC -> mState;
+  mDelay: mState -> StateC -> Time -> mState;
+  mabs: mState -> StateC -> StateA
+}.
+
+Variable m: mapping.
+
+Record simu (Pred: Type) (a: TTS StateA) (c: TTS StateC) (tra: Pred -> LP (Predicate _ a)) (trc: Pred -> LP (Predicate _ c)): Type := simuPrf {
+  inv: (mState m) -> StateC -> Prop;
+  invInit: forall st, Init _ c st -> inv (mInit m st) st;
+  invDelay: forall ex1 st1 st2 d, Delay _ c st1 d st2 -> inv ex1 st1 -> inv (mDelay m ex1 st1 d) st2;
+  invNext: forall ex1 st1 st2, Next _ c st1 st2 -> inv ex1 st1 -> inv (mNext m ex1 st1) st2;
+  simuInit: forall st, Init _ c st -> Init _ a (mabs m (mInit m st) st);
+  simuDelay: forall ex1 st1 st2 d, Delay _ c st1 d st2 -> inv ex1 st1 ->
+    Delay _ a (mabs m ex1 st1) d (mabs m (mDelay m ex1 st1 d) st2);
+  simuNext: forall ex1 st1 st2, Next _ c st1 st2 -> inv ex1 st1 ->
+    Next _ a (mabs m ex1 st1) (mabs m (mNext m ex1 st1) st2);
+  simuPred: forall ext st, inv ext st -> 
+    (forall p, lpSat (Satisfy _ c) st (trc p) <-> lpSat (Satisfy _ a) (mabs m ext st) (tra p)) 
+}.
+
+Theorem satProd: forall State Ind Pred (Sat: forall i, State -> Pred i -> Prop) (st:State) i (f: LP (Pred i)),
+  lpSat (Sat i) st f
+  <->
+  lpSat
+    (fun (st : State) (p : {i : Ind &  Pred i}) => Sat (projT1 p) st (projT2 p)) st
+     (addIndex Ind _ i f).
+Proof.
+  induction f; simpl; intros; split; intros; intuition.
+Qed.
+
+Definition trProd (State: Type) Ind (Pred: Ind -> Type) (tts: Ind -> TTS State) (tr: forall i, (Pred i) -> LP (Predicate _ (tts i))):
+  {i:Ind & Pred i} -> LP (Predicate _ (TTSIndexedProduct _ Ind tts)) :=
+  fun p => addIndex Ind _ (projS1 p) (tr (projS1 p) (projS2 p)).
+
+Implicit Arguments trProd.
+Require Import Setoid.
+
+Theorem satTrProd:
+  forall State Ind Pred (tts: Ind -> TTS State) 
+    (tr: forall i, (Pred  i) -> LP (Predicate _ (tts i))) (st:State) (p: {i:Ind & (Pred i)}),
+  lpSat (Satisfy _ (tts (projS1 p))) st (tr (projS1 p) (projS2 p))
+  <->
+  lpSat (Satisfy _ (TTSIndexedProduct _ _ tts)) st (trProd _ tts tr p).
+Proof.
+  unfold trProd, TTSIndexedProduct; simpl; intros.
+  rewrite (satProd State Ind (fun i => Predicate State (tts i))
+                      (fun i => Satisfy _ (tts i))); tauto.
+Qed.
+
+Theorem simuProd: 
+  forall Ind (Pred: Ind -> Type) (tta: Ind -> TTS StateA) (ttc: Ind -> TTS StateC) 
+    (tra: forall i, (Pred i) -> LP (Predicate _ (tta i)))
+    (trc: forall i, (Pred i) -> LP (Predicate _ (ttc i))),
+     (forall i, simu _ (tta i) (ttc i) (tra i) (trc i)) -> 
+       simu _ (TTSIndexedProduct _ Ind tta) (TTSIndexedProduct _ Ind ttc)
+                  (trProd Pred tta tra) (trProd Pred ttc trc).
+Proof.
+  intros.
+  apply simuPrf with (fun ex st => forall i, inv _ _ (ttc i) (tra i) (trc i) (X i) ex st); simpl; intros; auto.
+  eapply invInit; eauto.
+  eapply invDelay; eauto.
+  eapply invNext; eauto.
+  eapply simuInit; eauto.
+  eapply simuDelay; eauto.
+  eapply simuNext; eauto.
+  split; simpl; intros.
+  generalize (proj1 (simuPred _ _ _ _ _ (X (projS1 p)) ext st (H (projS1 p)) (projS2 p))); simpl; intro.
+  rewrite <- (satTrProd StateA Ind Pred tta tra); apply H1.
+  rewrite (satTrProd StateC Ind Pred ttc trc); apply H0.
+
+  generalize (proj2 (simuPred _ _ _ _ _ (X (projS1 p)) ext st (H (projS1 p)) (projS2 p))); simpl; intro.
+  rewrite <- (satTrProd StateC Ind Pred ttc trc); apply H1.
+  rewrite (satTrProd StateA Ind Pred tta tra); apply H0.
+Qed.
+
+End SIMU_F.
+
+Section TRANSFO.
+
+Record simu_equiv StateA StateC m1 m2 Pred (a: TTS StateA) (c: TTS StateC) (tra: Pred -> LP (Predicate _ a)) (trc: Pred -> LP (Predicate _ c)): Type := simuEquivPrf {
+  simuLR: simu StateA StateC m1 Pred a c tra trc;
+  simuRL: simu StateC StateA m2 Pred c a trc tra
+}.
+
+Theorem simu_equivProd: 
+  forall StateA StateC m1 m2 Ind (Pred: Ind -> Type) (tta: Ind -> TTS StateA) (ttc: Ind -> TTS StateC) 
+    (tra: forall i, (Pred i) -> LP (Predicate _ (tta i)))
+    (trc: forall i, (Pred i) -> LP (Predicate _ (ttc i))),
+     (forall i, simu_equiv StateA StateC m1 m2 _ (tta i) (ttc i) (tra i) (trc i)) -> 
+       simu_equiv StateA StateC m1 m2 _ (TTSIndexedProduct _ Ind tta) (TTSIndexedProduct _ Ind ttc)
+                  (trProd _ _ Pred tta tra) (trProd _ _ Pred ttc trc).
+Proof.
+  intros; split; intros.
+  apply simuProd; intro.
+  elim (X i); auto.
+  apply simuProd; intro.
+  elim (X i); auto.
+Qed.
+
+Record RTLanguage: Type := mkRTLanguage {
+   Syntax: Type;
+   DynamicState: Syntax -> Type;
+   Semantic: forall (mdl:Syntax), TTS (DynamicState mdl);
+   MdlPredicate: Syntax -> Type;
+   MdlPredicateDefinition: forall mdl, MdlPredicate mdl -> LP (Predicate _ (Semantic mdl))
+}.
+
+Record Transformation (l1 l2: RTLanguage): Type := mkTransformation {
+  Tmodel: Syntax l1 -> Syntax l2;
+  Tl1l2: forall mdl, mapping (DynamicState l1 mdl) (DynamicState l2 (Tmodel mdl));
+  Tl2l1: forall mdl, mapping (DynamicState l2 (Tmodel mdl)) (DynamicState l1 mdl);
+  Tpred: forall mdl, MdlPredicate l1 mdl -> LP (MdlPredicate l2 (Tmodel mdl));
+  Tsim: forall mdl, simu_equiv (DynamicState l1 mdl) (DynamicState l2 (Tmodel mdl)) (Tl1l2 mdl) (Tl2l1 mdl)
+    (MdlPredicate l1 mdl) (Semantic l1 mdl) (Semantic l2 (Tmodel mdl))
+    (MdlPredicateDefinition l1 mdl)
+    (fun p => LPTransfo (MdlPredicateDefinition l2 (Tmodel mdl)) (Tpred mdl p))
+}.
+
+Section Product.
+
+Record PSyntax (L: RTLanguage): Type := mkPSyntax {
+  pIndex: Type;
+  pIsEmpty: pIndex + {pIndex -> False};
+  pState: Type;
+  pComponents: pIndex -> Syntax L;
+  pIsShared: forall i, DynamicState L (pComponents i) = pState
+}.
+
+Definition pPredicate (L: RTLanguage) (sys: PSyntax L) := { i : pIndex L sys & MdlPredicate L (pComponents L sys i)}.
+
+(* product with shared state *)
+
+Definition PLanguage (L: RTLanguage): RTLanguage := 
+  mkRTLanguage
+    (PSyntax L)
+    (pState L)
+    (fun mdl => TTSIndexedProduct (pState L mdl) (pIndex L mdl)
+      (fun i => match pIsShared L mdl i in (_ = y) return TTS y with
+        eq_refl => Semantic L (pComponents L mdl i)
+       end))
+    (pPredicate L)
+    (fun mdl => trProd _ _ _ _ 
+      (fun i pi => match pIsShared L mdl i as e in (_ = y) return
+                     (LP (Predicate y
+                               match e in (_ = y0) return (TTS y0) with
+                               | eq_refl => Semantic L (pComponents L mdl i)
+                               end))
+     with
+     | eq_refl => MdlPredicateDefinition L (pComponents L mdl i) pi
+     end)).
+
+Inductive Empty: Type :=.
+
+Record isSharedTransfo l1 l2 tr: Prop := isSharedTransfoPrf {
+sameState:  forall mdl i j, 
+  DynamicState l2 (Tmodel l1 l2 tr (pComponents l1 mdl i)) =
+  DynamicState l2 (Tmodel l1 l2 tr (pComponents l1 mdl j));
+sameMState: forall mdl i j, 
+  mState _ _  (Tl1l2 _ _ tr (pComponents l1 mdl i)) =
+  mState _ _  (Tl1l2 _ _ tr (pComponents l1 mdl j));
+sameM12: forall mdl i j, 
+  Tl1l2 _ _ tr (pComponents l1 mdl i) =
+  match sym_eq (sameState mdl i j) in _=y return mapping _ y with
+    eq_refl => match sym_eq (pIsShared l1 mdl i) in _=x return mapping x _ with
+      eq_refl => match pIsShared l1 mdl j in _=x return mapping x _ with
+        eq_refl => Tl1l2 _ _ tr (pComponents l1 mdl j)
+      end
+    end         
+  end;
+sameM21: forall mdl i j, 
+  Tl2l1 l1 l2 tr (pComponents l1 mdl i) =
+  match
+    sym_eq (sameState mdl i j) in (_ = y)
+    return (mapping y (DynamicState l1 (pComponents l1 mdl i)))
+  with eq_refl =>
+    match
+      sym_eq (pIsShared l1 mdl i) in (_ = y)
+      return
+        (mapping (DynamicState l2 (Tmodel l1 l2 tr (pComponents l1 mdl j))) y)
+    with
+    | eq_refl =>
+        match
+          pIsShared l1 mdl j in (_ = y)
+          return
+            (mapping
+               (DynamicState l2 (Tmodel l1 l2 tr (pComponents l1 mdl j))) y)
+        with
+        | eq_refl => Tl2l1 l1 l2 tr (pComponents l1 mdl j)
+        end
+    end
+end
+}.
+
+Definition PTransfoSyntax l1 l2 tr (h: isSharedTransfo l1 l2 tr) mdl :=
+  mkPSyntax l2 (pIndex l1 mdl)
+    (pIsEmpty l1 mdl)
+    (match pIsEmpty l1 mdl return Type with 
+         inleft i => DynamicState l2 (Tmodel l1 l2 tr (pComponents l1 mdl i))
+        |inright h => pState l1 mdl
+       end)
+    (fun i => Tmodel l1 l2 tr (pComponents l1 mdl i))
+    (fun i => match pIsEmpty l1 mdl as y return
+        (DynamicState l2 (Tmodel l1 l2 tr (pComponents l1 mdl i)) =
+         match y with
+         | inleft i0 =>
+             DynamicState l2 (Tmodel l1 l2 tr (pComponents l1 mdl i0))
+         | inright _ => pState l1 mdl
+         end)
+      with
+         inleft j => sameState l1 l2 tr h mdl i j 
+      | inright h => match h i with end
+        end).
+
+Definition compSemantic l mdl i :=
+    match pIsShared l mdl i in (_=y) return TTS y with
+        eq_refl => Semantic l (pComponents l mdl i)
+    end.
+
+Definition compSemanticEq l mdl i s (e: DynamicState l (pComponents l mdl i) = s) :=
+    match e in (_=y) return TTS y with
+        eq_refl => Semantic l (pComponents l mdl i)
+    end.
+
+Definition Pmap12 l1 l2 tr (h: isSharedTransfo l1 l2 tr) (mdl : PSyntax l1) :=
+match
+  pIsEmpty l1 mdl as s
+  return
+    (mapping (pState l1 mdl)
+       match s with
+       | inleft i => DynamicState l2 (Tmodel l1 l2 tr (pComponents l1 mdl i))
+       | inright _ => pState l1 mdl
+       end)
+with
+| inleft p =>
+    match
+      pIsShared l1 mdl p in (_ = y)
+      return
+        (mapping y (DynamicState l2 (Tmodel l1 l2 tr (pComponents l1 mdl p))))
+    with
+    | eq_refl => Tl1l2 l1 l2 tr (pComponents l1 mdl p)
+    end
+| inright _ =>
+    mkMapping (pState l1 mdl) (pState l1 mdl) Unit
+      (fun _ : pState l1 mdl => unit)
+      (fun (_ : Unit) (_ : pState l1 mdl) => unit)
+      (fun (_ : Unit) (_ : pState l1 mdl) (_ : Time) => unit)
+      (fun (_ : Unit) (X : pState l1 mdl) => X)
+end.
+
+Definition Pmap21 l1 l2 tr (h : isSharedTransfo l1 l2 tr) mdl :=
+match
+  pIsEmpty l1 mdl as s
+  return
+    (mapping
+       match s with
+       | inleft i => DynamicState l2 (Tmodel l1 l2 tr (pComponents l1 mdl i))
+       | inright _ => pState l1 mdl
+       end (pState l1 mdl))
+with
+| inleft p =>
+    match
+      pIsShared l1 mdl p in (_ = y)
+      return
+        (mapping (DynamicState l2 (Tmodel l1 l2 tr (pComponents l1 mdl p))) y)
+    with
+    | eq_refl => Tl2l1 l1 l2 tr (pComponents l1 mdl p)
+    end
+| inright _ =>
+    mkMapping (pState l1 mdl) (pState l1 mdl) Unit
+      (fun _ : pState l1 mdl => unit)
+      (fun (_ : Unit) (_ : pState l1 mdl) => unit)
+      (fun (_ : Unit) (_ : pState l1 mdl) (_ : Time) => unit)
+      (fun (_ : Unit) (X : pState l1 mdl) => X)
+end.
+
+Definition PTpred l1 l2 tr (h : isSharedTransfo l1 l2 tr) mdl (pp : pPredicate l1 mdl):
+  LP (MdlPredicate (PLanguage l2) (PTransfoSyntax l1 l2 tr h mdl)) :=
+match pIsEmpty l1 mdl with
+| inleft _ =>
+      let (x, p) := pp in
+      addIndex (pIndex l1 mdl) (fun i => MdlPredicate l2 (Tmodel l1 l2 tr (pComponents l1 mdl i))) x
+        (LPTransfo (Tpred l1 l2 tr (pComponents l1 mdl x))
+          (LPPred (MdlPredicate l1 (pComponents l1 mdl x)) p))
+| inright f => match f (projS1 pp) with end
+end.
+
+Lemma simu_eqA: 
+  forall A1 A2 C m P sa sc tta ttc (h: A2=A1),
+  simu A1 C (match h in (_=y) return mapping _ C with eq_refl => m end) 
+  P (match h in (_=y) return TTS y with eq_refl => sa end)
+  sc (fun p => match h in (_=y) return LP (Predicate y _) with eq_refl => tta p end)
+  ttc ->
+  simu A2 C m P sa sc tta ttc.
+admit.
+Qed.
+
+Lemma simu_eqC: 
+  forall A C1 C2 m P sa sc tta ttc (h: C2=C1),
+  simu A C1 (match h in (_=y) return mapping A _ with eq_refl => m end) 
+  P sa (match h in (_=y) return TTS y with eq_refl => sc end)
+  tta (fun p => match h in (_=y) return LP (Predicate y _) with eq_refl => ttc p end)
+   ->
+  simu A C2 m P sa sc tta ttc.
+admit.
+Qed.
+
+Lemma simu_eqA1: 
+  forall A1 A2 C m P sa sc tta ttc (h: A1=A2),
+  simu A1 C m 
+  P 
+  (match (sym_eq h) in (_=y) return TTS y with eq_refl => sa end) sc
+  (fun p => match (sym_eq h) as e in (_=y) return LP (Predicate y (match e in (_=z) return TTS z with eq_refl => sa end)) with eq_refl => tta p end) ttc
+   ->
+  simu A2 C (match h in (_=y) return mapping _ C with eq_refl => m end) P sa sc tta ttc.
+admit.
+Qed.
+
+Lemma simu_eqA2: 
+  forall A1 A2 C m P sa sc tta ttc (h: A1=A2),
+  simu A1 C (match (sym_eq h) in (_=y) return mapping _ C with eq_refl => m end)
+  P 
+  sa sc tta ttc
+   ->
+  simu A2 C m P
+  (match h in (_=y) return TTS y with eq_refl => sa end) sc 
+  (fun p => match h as e in (_=y) return LP (Predicate y match e in (_=y0) return TTS y0 with eq_refl => sa end) with eq_refl => tta p end)
+ ttc.
+admit.
+Qed.
+
+Lemma simu_eqC2: 
+  forall A C1 C2 m P sa sc tta ttc (h: C1=C2),
+  simu A C1 (match (sym_eq h) in (_=y) return mapping A _ with eq_refl => m end)
+  P 
+  sa sc tta ttc
+   ->
+  simu A C2 m P
+  sa (match h in (_=y) return TTS y with eq_refl => sc end) 
+  tta (fun p => match h as e in (_=y) return LP (Predicate y match e in (_=y0) return TTS y0 with eq_refl => sc end) with eq_refl => ttc p end).
+admit.
+Qed.
+
+Lemma simu_eqM: 
+  forall A C m1 m2 P sa sc tta ttc (h: m1=m2),
+  simu A C m1 P sa sc tta ttc
+   ->
+  simu A C m2 P sa sc tta ttc.
+admit.
+Qed.
+
+Lemma LPTransfo_trans:
+  forall Pred1 Pred2 Pred3 (tr1: Pred1 -> LP Pred2) (tr2: Pred2 -> LP Pred3) f,
+    LPTransfo tr2 (LPTransfo tr1 f) = LPTransfo (fun x => LPTransfo tr2 (tr1 x)) f.
+Proof.
+  admit.
+Qed.
+
+Lemma LPTransfo_addIndex:
+  forall Ind Pred tr1 x (tr2: forall i, Pred i -> LP (tr1 i)) (p: LP (Pred x)),
+    addIndex Ind tr1 x (LPTransfo (tr2 x) p) =
+    LPTransfo
+      (fun p0 : {i : Ind & Pred i} =>
+        addIndex Ind tr1 (projT1 p0) (tr2 (projT1 p0) (projT2 p0)))
+      (addIndex Ind Pred x p).
+Proof.
+  unfold addIndex; intros. 
+  rewrite LPTransfo_trans.
+  rewrite LPTransfo_trans.
+  simpl.
+  auto.
+Qed.
+
+Record tr_compat I0 I1 tr := compatPrf {
+  and_compat: forall p1 p2, tr (LPAnd I0 p1 p2) = LPAnd I1 (tr p1) (tr p2);
+  not_compat: forall p, tr (LPNot I0 p) = LPNot I1 (tr p)
+}.
+
+Lemma LPTransfo_addIndex_tr:
+  forall Ind Pred tr0 tr1 x (tr2: forall i, Pred i -> LP (tr0 i))  (tr3: forall i, LP (tr0 i) -> LP (tr1 i)) (p: LP (Pred x)),
+    (forall x, tr_compat (tr0 x) (tr1 x) (tr3 x)) ->
+    addIndex Ind tr1 x (tr3 x (LPTransfo (tr2 x) p)) =
+    LPTransfo
+      (fun p0 : {i : Ind & Pred i} =>
+        addIndex Ind tr1 (projT1 p0) (tr3 (projT1 p0) (tr2 (projT1 p0) (projT2 p0))))
+      (addIndex Ind Pred x p).
+Proof.
+  unfold addIndex; simpl; intros. 
+  rewrite LPTransfo_trans; simpl.
+  rewrite <- LPTransfo_trans.
+  f_equal.
+  induction p; simpl; intros; auto.
+  rewrite (and_compat _ _ _ (H x)).
+  rewrite <- IHp1, <- IHp2; auto.
+  rewrite <- IHp.
+  rewrite (not_compat _ _ _ (H x)); auto.
+Qed.
+
+Require Export Coq.Logic.FunctionalExtensionality.
+Print PLanguage.
+Program Definition PTransfo l1 l2 (tr: Transformation l1 l2) (h: isSharedTransfo l1 l2 tr): 
+Transformation (PLanguage l1) (PLanguage l2) :=
+  mkTransformation (PLanguage l1) (PLanguage l2)
+    (PTransfoSyntax l1 l2 tr h)
+    (Pmap12 l1 l2 tr h)
+    (Pmap21 l1 l2 tr h)
+    (PTpred l1 l2 tr h)
+    (fun mdl => simu_equivProd 
+      (pState l1 mdl) 
+      (pState l2 (PTransfoSyntax l1 l2 tr h mdl)) 
+      (Pmap12 l1 l2 tr h mdl)
+      (Pmap21 l1 l2 tr h mdl)
+      (pIndex l1 mdl) 
+      (fun i => MdlPredicate l1 (pComponents l1 mdl i))
+      (compSemantic l1 mdl)
+      (compSemantic l2 (PTransfoSyntax l1 l2 tr h mdl))
+      _
+      _
+      _
+        ).
+
+Next Obligation.
+  unfold compSemantic, PTransfoSyntax; simpl.
+  case (pIsEmpty l1 mdl); simpl; intros.
+  unfold pPredicate; simpl.
+  unfold pPredicate in X; simpl in X.
+  case (sameState l1 l2 tr h mdl i p).
+  apply (LPTransfo (MdlPredicateDefinition l2 (Tmodel l1 l2 tr (pComponents l1 mdl i)))).
+  apply (LPTransfo (Tpred l1 l2 tr (pComponents l1 mdl i))).
+  apply (LPPred _ X).
+
+  apply False_rect; apply (f i).
+Defined.
+
+Next Obligation.
+  split; intros.
+  unfold Pmap12; simpl.
+  unfold PTransfo_obligation_1; simpl.
+  unfold compSemantic; simpl.
+  unfold eq_ind, eq_rect, f_equal; simpl.
+  case (pIsEmpty l1 mdl); intros.
+  apply simu_eqA2.
+  apply simu_eqC2.
+  apply simu_eqM with (Tl1l2 l1 l2 tr (pComponents l1 mdl i)).
+  apply sameM12.
+  apply (simuLR _ _ _ _ _ _ _ _ _ (Tsim l1 l2 tr (pComponents l1 mdl i))); intro.
+
+  apply False_rect; apply (f i).
+
+  unfold Pmap21; simpl.
+  unfold PTransfo_obligation_1; simpl.
+  unfold compSemantic; simpl.
+  unfold eq_ind, eq_rect, f_equal; simpl.
+  case (pIsEmpty l1 mdl); intros.
+  apply simu_eqC2.
+  apply simu_eqA2.
+  apply simu_eqM with (Tl2l1 l1 l2 tr (pComponents l1 mdl i)).
+  apply sameM21.
+  apply (simuRL _ _ _ _ _ _ _ _ _ (Tsim l1 l2 tr (pComponents l1 mdl i))); intro.
+
+  apply False_rect; apply (f i).
+Qed.
+
+Next Obligation.
+  unfold trProd; simpl.
+  unfold PTransfo_obligation_1; simpl.
+  unfold compSemantic; simpl.
+  unfold eq_ind, eq_rect, f_equal; simpl.
+  apply functional_extensionality; intro.
+  case x; clear x; intros.
+  unfold PTpred; simpl.
+  case (pIsEmpty l1 mdl); simpl; intros.
+  set (tr0 i :=
+   Predicate (DynamicState l2 (Tmodel l1 l2 tr (pComponents l1 mdl i)))
+     (Semantic l2 (Tmodel l1 l2 tr (pComponents l1 mdl i)))).
+  set (tr1 i :=
+   Predicate (DynamicState l2 (Tmodel l1 l2 tr (pComponents l1 mdl p)))
+     match sameState l1 l2 tr h mdl i p in (_ = y) return (TTS y) with
+     | eq_refl => Semantic l2 (Tmodel l1 l2 tr (pComponents l1 mdl i))
+     end).
+  set (tr2 x := MdlPredicateDefinition l2 (Tmodel l1 l2 tr (pComponents l1 mdl x))).
+  set (Pred x := MdlPredicate l2 (Tmodel l1 l2 tr (pComponents l1 mdl x))).
+  set (tr3 x f := match
+    sameState l1 l2 tr h mdl x p as e in (_ = y)
+    return
+      (LP
+         (Predicate y
+            match e in (_ = y0) return (TTS y0) with
+            | eq_refl => Semantic l2 (Tmodel l1 l2 tr (pComponents l1 mdl x))
+            end))
+  with
+  | eq_refl => f
+  end).
+  apply (LPTransfo_addIndex_tr _ Pred tr0 tr1 x tr2 tr3
+    (Tpred l1 l2 tr (pComponents l1 mdl x) m)).
+  unfold tr0, tr1, tr3; intros; split; simpl; intros; auto.
+  case (sameState l1 l2 tr h mdl x0 p); auto.
+  case (sameState l1 l2 tr h mdl x0 p); auto.
+
+  apply False_rect; apply (f x).
+Qed.
+
+End Product.
diff --git a/test-suite/bugs/closed/shouldsucceed/2388.v b/test-suite/bugs/closed/shouldsucceed/2388.v
index 8cc43ee6..c7926711 100644
--- a/test-suite/bugs/closed/shouldsucceed/2388.v
+++ b/test-suite/bugs/closed/shouldsucceed/2388.v
@@ -2,3 +2,9 @@
 
 Fail Parameters (A:Prop) (a:A A).
 
+(* This is a variant (reported as part of bug #2347) *)
+
+Require Import EquivDec.                                              
+Fail Program Instance bool_eq_eqdec : EqDec bool eq := 
+   {equiv_dec x y := (fix aux (x y : bool) {struct x}:= aux _ y) x y}.
+
diff --git a/test-suite/bugs/closed/shouldsucceed/2393.v b/test-suite/bugs/closed/shouldsucceed/2393.v
new file mode 100644
index 00000000..fb4f9261
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2393.v
@@ -0,0 +1,13 @@
+Require Import Program.
+
+Inductive T := MkT.
+
+Definition sizeOf (t : T) : nat
+    := match t with
+       | MkT => 1
+       end.
+Variable vect : nat -> Type.
+Program Fixpoint idType (t : T) (n := sizeOf t) (b : vect n) {measure n} : T
+    := match t with
+       | MkT => MkT
+       end.
diff --git a/test-suite/bugs/closed/shouldsucceed/2404.v b/test-suite/bugs/closed/shouldsucceed/2404.v
new file mode 100644
index 00000000..fe8eba54
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2404.v
@@ -0,0 +1,46 @@
+(* Check that dependencies in the indices of the type of the terms to
+   match are taken into account and correctly generalized *)
+
+Require Import Relations.Relation_Definitions.
+Require Import Basics.
+
+Record Base := mkBase
+ {(* Primitives *)
+    World : Set
+  (* Names are real, links are theoretical *)
+  ; Name : World -> Set
+
+  ; wweak : World -> World -> Prop
+
+  ; exportw : forall a b : World, (wweak a b) -> (Name b) -> option (Name a)
+}.
+
+Section Derived.
+  Variable base : Base.
+  Definition bWorld := World base.
+  Definition bName  := Name base.
+  Definition bexportw := exportw base.
+  Definition bwweak := wweak base.
+
+  Implicit Arguments bexportw [a b].
+
+Inductive RstarSetProof {I : Type} (T : I -> I -> Type) : I -> I -> Type :=
+  starReflS : forall a, RstarSetProof T a a
+| starTransS : forall i j k, T i j -> (RstarSetProof T j k) -> RstarSetProof T i k.
+
+Implicit Arguments starTransS [I T i j k].
+
+Definition RstarInv {A : Set} (rel : relation A) : A -> A -> Type :=  (flip (RstarSetProof (flip rel))).
+
+Definition bwweakFlip (b a : bWorld) : Prop := (bwweak a b).
+Definition Rweak : forall a b : bWorld, Type := RstarInv bwweak.
+
+Fixpoint exportRweak {a b} (aRWb : Rweak a b) (y : bName b) : option (bName a) :=
+  match aRWb,y with
+  | starReflS a, y' => Some y'
+  | starTransS i j k jWk jRWi, y' =>
+    match (bexportw jWk y) with
+    | Some x => exportRweak jRWi x
+    | None   => None
+    end
+  end.
diff --git a/test-suite/bugs/closed/shouldsucceed/2456.v b/test-suite/bugs/closed/shouldsucceed/2456.v
new file mode 100644
index 00000000..56f046c4
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2456.v
@@ -0,0 +1,53 @@
+
+Require Import Equality.
+
+Parameter Patch : nat -> nat -> Set.
+
+Inductive Catch (from to : nat) : Type
+    := MkCatch : forall (p : Patch from to),
+                 Catch from to.
+Implicit Arguments MkCatch [from to].
+
+Inductive CatchCommute5
+        : forall {from mid1 mid2 to : nat},
+          Catch from mid1
+       -> Catch mid1 to
+       -> Catch from mid2
+       -> Catch mid2 to
+       -> Prop
+     := MkCatchCommute5 :
+           forall {from mid1 mid2 to : nat}
+                  (p : Patch from mid1)
+                  (q : Patch mid1 to)
+                  (q' : Patch from mid2)
+                  (p' : Patch mid2 to),
+           CatchCommute5 (MkCatch p) (MkCatch q) (MkCatch q') (MkCatch p').
+
+Inductive CatchCommute {from mid1 mid2 to : nat}
+                       (p : Catch from mid1)
+                       (q : Catch mid1 to)
+                       (q' : Catch from mid2)
+                       (p' : Catch mid2 to)
+                     : Prop
+    := isCatchCommute5 : forall (catchCommuteDetails : CatchCommute5 p q q' p'),
+                         CatchCommute p q q' p'.
+Notation "<< p , q >> <~> << q' , p' >>"
+    := (CatchCommute p q q' p')
+    (at level 60, no associativity).
+
+Lemma CatchCommuteUnique2 :
+      forall {from mid mid' to : nat}
+             {p   : Catch from mid}  {q   : Catch mid  to}
+             {q'  : Catch from mid'} {p'  : Catch mid' to}
+             {q'' : Catch from mid'} {p'' : Catch mid' to}
+             (commute1 : <<p, q>> <~> <<q', p'>>)
+             (commute2 : <<p, q>> <~> <<q'', p''>>),
+      (p' = p'') /\ (q' = q'').
+Proof with auto.
+intros.
+set (X := commute2).
+dependent destruction commute1;
+dependent destruction catchCommuteDetails;
+dependent destruction commute2;
+dependent destruction catchCommuteDetails generalizing X.
+Admitted.
\ No newline at end of file
diff --git a/test-suite/bugs/closed/shouldsucceed/2473.v b/test-suite/bugs/closed/shouldsucceed/2473.v
new file mode 100644
index 00000000..4c302512
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2473.v
@@ -0,0 +1,39 @@
+
+Require Import Relations Program Setoid Morphisms.
+
+Section S1.
+  Variable R: nat -> relation bool.
+  Instance HR1: forall n, Transitive (R n). Admitted.
+  Instance HR2: forall n, Symmetric (R n).  Admitted.
+  Hypothesis H: forall n a, R n (andb a a) a.
+  Goal forall n a b, R n b a.
+   intros. 
+   (* rewrite <- H. *) (* Anomaly: Evar ?.. was not declared. Please report. *)
+   (* idem with setoid_rewrite *)
+(*    assert (HR2' := HR2 n). *)
+   rewrite <- H.                (* ok *)
+   admit.
+  Qed.
+End S1.
+
+Section S2.
+  Variable R: nat -> relation bool.
+  Instance HR: forall n, Equivalence (R n). Admitted.
+  Hypothesis H: forall n a, R n (andb a a) a.
+  Goal forall n a b, R n a b.
+   intros. rewrite <- H. admit.
+  Qed.
+End S2.
+
+(* the parametrised relation is required to get the problem *)
+Section S3.
+  Variable R: relation bool.
+  Instance HR1': Transitive R. Admitted.
+  Instance HR2': Symmetric R.  Admitted.
+  Hypothesis H: forall a, R (andb a a) a.
+  Goal forall a b, R b a.
+   intros. 
+   rewrite <- H.                (* ok *)
+   admit.
+  Qed.
+End S3.
\ No newline at end of file
diff --git a/test-suite/bugs/closed/shouldsucceed/2603.v b/test-suite/bugs/closed/shouldsucceed/2603.v
new file mode 100644
index 00000000..a556b9bf
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2603.v
@@ -0,0 +1,18 @@
+Module Type T.
+End T.
+
+Declare Module K : T.
+
+Module Type L.
+Declare Module E : T.
+End L.
+
+Module M1 : L with Module E:=K.
+Module E := K.
+Fail Inductive t := E. (* Used to be accepted, but End M1 below was failing *)
+End M1.
+
+Module M2 : L with Module E:=K.
+Inductive t := E.
+Fail Module E := K. (* Used to be accepted *)
+Fail End M2. (* Used to be accepted *)
diff --git a/test-suite/bugs/closed/shouldsucceed/2613.v b/test-suite/bugs/closed/shouldsucceed/2613.v
new file mode 100644
index 00000000..4f0470b1
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2613.v
@@ -0,0 +1,17 @@
+(* Check that eq_sym is still pointing to Logic.eq_sym after use of Function *)
+
+Require Import ZArith.
+Require Recdef.
+
+Axiom nat_eq_dec: forall x y : nat, {x=y}+{x<>y}.
+
+Locate eq_sym.  (* Constant Coq.Init.Logic.eq_sym  *)
+
+Function loop (n: nat) {measure (fun x => x) n} : bool :=
+  if nat_eq_dec n 0 then false else loop (pred n).
+Proof.
+   admit.
+Defined.
+
+Check eq_sym eq_refl : 0=0.
+
diff --git a/test-suite/bugs/closed/shouldsucceed/2615.v b/test-suite/bugs/closed/shouldsucceed/2615.v
new file mode 100644
index 00000000..54e1a07c
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2615.v
@@ -0,0 +1,14 @@
+(* This failed with an anomaly in pre-8.4 because of let-in not
+   properly taken into account in the test for unification pattern *)
+
+Inductive foo : forall A, A -> Prop :=
+| foo_intro : forall A x, foo A x.
+Lemma bar A B f : foo (A -> B) f -> forall x : A, foo B (f x).
+Fail induction 1.
+
+(* Whether these examples should succeed with a non-dependent return predicate 
+   or fail because there is well-typed return predicate dependent in f 
+   is questionable. As of 25 oct 2011, they succeed *)
+refine (fun p => match p with _ => _ end).
+Undo.
+refine (fun p => match p with foo_intro _ _ => _ end).
diff --git a/test-suite/bugs/closed/shouldsucceed/2616.v b/test-suite/bugs/closed/shouldsucceed/2616.v
new file mode 100644
index 00000000..8758e32d
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2616.v
@@ -0,0 +1,7 @@
+(* Testing ill-typed rewrite which used to succeed in 8.3 *)
+Goal 
+  forall (N : nat -> Prop) (g : nat -> sig N) (IN : forall a : sig N, a = g 0), 
+    N 0 -> False.
+Proof.
+intros.
+Fail rewrite IN in H.
diff --git a/test-suite/bugs/closed/shouldsucceed/2640.v b/test-suite/bugs/closed/shouldsucceed/2640.v
new file mode 100644
index 00000000..da0cc68a
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2640.v
@@ -0,0 +1,17 @@
+(* Testing consistency of globalization and interpretation in some
+   extreme cases *)
+
+Section sect.
+
+  (* Simplification of the initial example *)
+  Hypothesis Other: True.
+
+  Lemma C2 : True.
+  proof.
+  Fail have True using Other.
+  Abort.
+
+  (* Variant of the same problem *)
+  Lemma C2 : True.
+  Fail clear; Other.
+  Abort.
-- 
cgit v1.2.3