Removing test for bug #3956.

It breaks test-suite of trunk since Matthieu's fixes for the soundness of
polymorphic universes, and I am unsure of the expected semantics. We should
reintroduce it later on when we understand better the issue of simply fix it
once and for all.

1 files changed, 0 insertions, 141 deletions

diff --git a/test-suite/bugs/opened/3956.v b/test-suite/bugs/opened/3956.v
deleted file mode 100644
index 94c0c6744..000000000
--- a/test-suite/bugs/opened/3956.v
+++ /dev/null
@@ -1,141 +0,0 @@
-(* -*- mode: coq; mode: visual-line -*- *)
-Set Universe Polymorphism.
-Set Primitive Projections.
-Close Scope nat_scope.
-
-Record prod (A B : Type) := pair { fst : A ; snd : B }.
-Arguments pair {A B} _ _.
-Arguments fst {A B} _ / .
-Arguments snd {A B} _ / .
-Notation "x * y" := (prod x y) : type_scope.
-Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z) : core_scope.
-
-Definition Type1 := Eval hnf in let gt := (Set : Type@{i}) in Type@{i}.
-Definition Type2 := Eval hnf in let gt := (Type1 : Type@{i}) in Type@{i}.
-
-Inductive paths {A : Type} (a : A) : A -> Type :=
-  idpath : paths a a.
-Arguments idpath {A a} , [A] a.
-Notation "x = y" := (@paths _ x y) : type_scope.
-Definition concat {A} {x y z : A} (p : x = y) (q : y = z) : x = z
-  := match p, q with idpath, idpath => idpath end.
-
-Definition path_prod {A B : Type} (z z' : A * B)
-: (fst z = fst z') -> (snd z = snd z') -> (z = z').
-Proof.
-  destruct z, z'; simpl; intros [] []; reflexivity.
-Defined.  
-
-Module Type TypeM.
-  Parameter m : Type2.
-End TypeM.
-
-Module ProdM (XM : TypeM) (YM : TypeM) <: TypeM.
-  Definition m := XM.m * YM.m.
-End ProdM.
-
-Module Type FunctionM (XM YM : TypeM).
-  Parameter m : XM.m -> YM.m.
-End FunctionM.
-
-Module IdmapM (XM : TypeM) <: FunctionM XM XM.
-  Definition m := (fun x => x) : XM.m -> XM.m.
-End IdmapM.
-
-Module Type HomotopyM (XM YM : TypeM) (fM gM : FunctionM XM YM).
-  Parameter m : forall x, fM.m x = gM.m x.
-End HomotopyM.
-
-Module ComposeM (XM YM ZM : TypeM)
-       (gM : FunctionM YM ZM) (fM : FunctionM XM YM)
-       <: FunctionM XM ZM.
-  Definition m := (fun x => gM.m (fM.m x)).
-End ComposeM.
-
-Module Type CorecM (YM ZM : TypeM) (fM : FunctionM YM ZM)
-       (XM : TypeM) (gM : FunctionM XM ZM).
-  Parameter m : XM.m -> YM.m.
-  Parameter m_beta : forall x, fM.m (m x) = gM.m x.
-End CorecM.
-
-Module Type CoindpathsM (YM ZM : TypeM) (fM : FunctionM YM ZM)
-       (XM : TypeM) (hM kM : FunctionM XM YM).
-  Module fhM := ComposeM XM YM ZM fM hM.
-  Module fkM := ComposeM XM YM ZM fM kM.
-  Declare Module mM (pM : HomotopyM XM ZM fhM fkM)
-    : HomotopyM XM YM hM kM.
-End CoindpathsM.
-
-Module Type Comodality (XM : TypeM).
-  Parameter m : Type2.
-  Module mM <: TypeM.
-    Definition m := m.
-  End mM.
-  Parameter from : m -> XM.m.
-  Module fromM <: FunctionM mM XM.
-    Definition m := from.
-  End fromM.
-  Declare Module corecM : CorecM mM XM fromM.
-  Declare Module coindpathsM : CoindpathsM mM XM fromM.
-End Comodality.
-
-Module Comodality_Theory (F : Comodality).
-
-  Module F_functor_M (XM YM : TypeM) (fM : FunctionM XM YM)
-         (FXM : Comodality XM) (FYM : Comodality YM).
-    Module f_o_from_M <: FunctionM FXM.mM YM.
-      Definition m := fun x => fM.m (FXM.from x).
-    End f_o_from_M.
-    Module mM := FYM.corecM FXM.mM f_o_from_M.
-    Definition m := mM.m.
-  End F_functor_M.
-
-  Module F_prod_cmp_M (XM YM : TypeM)
-         (FXM : Comodality XM) (FYM : Comodality YM).
-    Module PM := ProdM XM YM.
-    Module PFM := ProdM FXM FYM.
-    Module fstM <: FunctionM PM XM.
-      Definition m := @fst XM.m YM.m.
-    End fstM.
-    Module sndM <: FunctionM PM YM.
-      Definition m := @snd XM.m YM.m.
-    End sndM.
-    Module FPM := F PM.
-    Module FfstM := F_functor_M PM XM fstM FPM FXM.
-    Module FsndM := F_functor_M PM YM sndM FPM FYM.
-    Definition m : FPM.m -> PFM.m
-      := fun z => (FfstM.m z , FsndM.m z).
-  End F_prod_cmp_M.
-
-  Module isequiv_F_prod_cmp_M
-         (XM YM : TypeM)
-         (FXM : Comodality XM) (FYM : Comodality YM).
-    (** The comparison map *)
-    Module cmpM := F_prod_cmp_M XM YM FXM FYM.
-    Module FPM := cmpM.FPM.
-    (** We construct an inverse to it using corecursion. *)
-    Module prod_from_M <: FunctionM cmpM.PFM cmpM.PM.
-      Definition m : cmpM.PFM.m -> cmpM.PM.m
-        := fun z => ( FXM.from (fst z) , FYM.from (snd z) ).
-    End prod_from_M.
-    Module cmpinvM <: FunctionM cmpM.PFM FPM
-      := FPM.corecM cmpM.PFM prod_from_M.
-    (** We prove the first homotopy *)
-    Module cmpinv_o_cmp_M <: FunctionM FPM FPM
-      := ComposeM FPM cmpM.PFM FPM cmpinvM cmpM.
-    Module idmap_FPM <: FunctionM FPM FPM
-      := IdmapM FPM.
-    Module cip_FPM := FPM.coindpathsM FPM cmpinv_o_cmp_M idmap_FPM.
-    Module cip_FPHM <: HomotopyM FPM cmpM.PM cip_FPM.fhM cip_FPM.fkM.
-      Definition m : forall x, cip_FPM.fhM.m@{i j} x = cip_FPM.fkM.m@{i j} x.
-      Proof.
-        intros x.
-        refine (concat (cmpinvM.m_beta@{i j} (cmpM.m@{i j} x)) _).
-        apply path_prod@{i i i}; simpl.
-        - exact (cmpM.FfstM.mM.m_beta@{i j} x).
-        - exact (cmpM.FsndM.mM.m_beta@{i j} x).
-      Defined.
-    Fail End cip_FPHM.
-(*  End isequiv_F_prod_cmp_M.
-
-End Comodality_Theory.*)