Imported Upstream version 8.5~beta1+dfsg

1 files changed, 0 insertions, 38 deletions

diff --git a/test-suite/bugs/closed/shouldsucceed/2362.v b/test-suite/bugs/closed/shouldsucceed/2362.v
deleted file mode 100644
index febb9c7b..00000000
--- a/test-suite/bugs/closed/shouldsucceed/2362.v
+++ /dev/null
@@ -1,38 +0,0 @@
-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.
-
-