From e04ce4144522b71c0d6bf3df868b2f3586eb5d5f Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Sun, 15 Jun 2014 13:29:23 +0200
Subject: Remove HoTT bug #33, as the stdlib won't become polymorphic in the
 next version.

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

diff --git a/test-suite/bugs/opened/HoTT_coq_033.v b/test-suite/bugs/opened/HoTT_coq_033.v
deleted file mode 100644
index e357fce324..0000000000
--- a/test-suite/bugs/opened/HoTT_coq_033.v
+++ /dev/null
@@ -1,14 +0,0 @@
-(** JMeq should be polymorphic *)
-Require Import JMeq.
-
-Set Implicit Arguments.
-
-Monomorphic Inductive JMeq' (A : Type) (x : A)
-: forall B : Type, B -> Prop :=
-  JMeq'_refl : JMeq' x x.
-
-(* Note: This should fail (the [Fail] should be present in the final file, even when in bugs/closed) *)
-Fail Monomorphic Definition foo := @JMeq' _ (@JMeq').
-
-(* Note: This should not fail *)
-Fail Monomorphic Definition bar := @JMeq _ (@JMeq).
-- 
cgit v1.2.3