From 0b78edbafedf87f150840228f7d3b7938c809c14 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 26 Jun 2014 13:54:16 +0200
Subject: Duplicate

---
 test-suite/bugs/opened/3385.v | 22 ----------------------
 1 file changed, 22 deletions(-)
 delete mode 100644 test-suite/bugs/opened/3385.v

diff --git a/test-suite/bugs/opened/3385.v b/test-suite/bugs/opened/3385.v
deleted file mode 100644
index b4da9cf675..0000000000
--- a/test-suite/bugs/opened/3385.v
+++ /dev/null
@@ -1,22 +0,0 @@
-Set Primitive Projections.
-Set Implicit Arguments.
-Set Universe Polymorphism.
-
-Record category := { ob : Type }.
-
-Goal forall C, ob C -> ob C.
-intros C X.
-
-let y := (eval compute in (ob C)) in constr_eq y (ob C). (* success *)
-let y := (eval compute in (@ob C)) in constr_eq y (ob C). (* success *)
-(* should be [Fail let y := (eval compute in (@ob C)) in constr_eq y (@ob C).] (really [let y := (eval compute in (@ob C)) in constr_eq y (@ob C)] should succeed, but so long as the [Fail] succeeds, this bug is open), but "not equal" escapes [Fail]. *)
-try (let y := (eval compute in (@ob C)) in constr_eq y (@ob C); fail 1). (* failure *)
-try (constr_eq (@ob C) (ob C); fail 1). (* failure *)
-let y := constr:(@ob C) in
-match y with
-  | ?f C => idtac
-end. (* success *)
-try (let y := constr:(@ob C) in
-match eval compute in y with
-  | ?f C => idtac
-end; fail 1). (* failure: no matching clauses for match *)
-- 
cgit v1.2.3