From 38f147b8a5299a6bee27784cf9dc8401d29ee9f5 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 7 Aug 2001 11:10:26 +0000
Subject: Passage au nouveau Destruct

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1882 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/ring/Setoid_ring_theory.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/contrib/ring/Setoid_ring_theory.v b/contrib/ring/Setoid_ring_theory.v
index a0d587eb34..891a1bf89d 100644
--- a/contrib/ring/Setoid_ring_theory.v
+++ b/contrib/ring/Setoid_ring_theory.v
@@ -434,7 +434,7 @@ Implicit Arguments Off.
 
 Definition Semi_Setoid_Ring_Theory_of :
   Setoid_Ring_Theory -> Semi_Setoid_Ring_Theory.
-NewDestruct 1.
+Intros until 1; Case H.
 Split; Intros; Simpl; EAuto.
 Defined.
 
-- 
cgit v1.2.3