From 8f08fe35f2b236dce27a3b0439810b736b8e559a Mon Sep 17 00:00:00 2001
From: letouzey
Date: Tue, 12 Jan 2010 13:35:26 +0000
Subject: revert commit 12650 for the moment, since it breaks MSetAVL

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12651 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 test-suite/success/apply.v | 17 -----------------
 1 file changed, 17 deletions(-)

(limited to 'test-suite')

diff --git a/test-suite/success/apply.v b/test-suite/success/apply.v
index cb55432fb7..3fc8a97922 100644
--- a/test-suite/success/apply.v
+++ b/test-suite/success/apply.v
@@ -348,20 +348,3 @@ Goal True.
 eapply (fun (A:Prop) (x:A) => conj I x).
 exact I.
 Qed.
-
-(* The following was not accepted from r12612 to r12649 *)
-
-Record sig0 := { p1 : nat; p2 : p1 = 0 }.
-
-Goal forall x : sig0, p1 x = 0.
-intro x;
-apply x.
-Qed.
-
-(* The following was accepted before r12612 but is still not accepted in r12650
-
-Goal forall x : { x:nat | x = 0}, proj1_sig x = 0.
-intro x;
-apply x.
-
-*)
-- 
cgit v1.2.3