From 83c56744d7e232abeb5f23e6d0f23cd0abc14a9c Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 5 Aug 2001 19:04:16 +0000
Subject: Expérimentation de NewDestruct et parfois NewInduction

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1880 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/ring/Ring.v                  | 18 +++++++++---------
 contrib/ring/Ring_abstract.v         |  2 +-
 contrib/ring/Ring_normalize.v        |  2 +-
 contrib/ring/Ring_theory.v           |  2 +-
 contrib/ring/Setoid_ring_normalize.v |  2 +-
 contrib/ring/Setoid_ring_theory.v    |  2 +-
 6 files changed, 14 insertions(+), 14 deletions(-)

(limited to 'contrib/ring')

diff --git a/contrib/ring/Ring.v b/contrib/ring/Ring.v
index 88e609e3f8..93c6eaf539 100644
--- a/contrib/ring/Ring.v
+++ b/contrib/ring/Ring.v
@@ -69,15 +69,15 @@ Grammar vernac vernac : ast :=
 
 Definition BoolTheory : (Ring_Theory xorb andb true false [b:bool]b eqb).
 Split; Simpl.
-Destruct n; Destruct m; Reflexivity.
-Destruct n; Destruct m; Destruct p; Reflexivity.
-Destruct n; Destruct m; Reflexivity.
-Destruct n; Destruct m; Destruct p; Reflexivity.
-Destruct n; Reflexivity.
-Destruct n; Reflexivity.
-Destruct n; Reflexivity.
-Destruct n; Destruct m; Destruct p; Reflexivity.
-Destruct x; Destruct y; Reflexivity Orelse Simpl; Tauto.
+NewDestruct n; NewDestruct m; Reflexivity.
+NewDestruct n; NewDestruct m; NewDestruct p; Reflexivity.
+NewDestruct n; NewDestruct m; Reflexivity.
+NewDestruct n; NewDestruct m; NewDestruct p; Reflexivity.
+NewDestruct n; Reflexivity.
+NewDestruct n; Reflexivity.
+NewDestruct n; Reflexivity.
+NewDestruct n; NewDestruct m; NewDestruct p; Reflexivity.
+NewDestruct x; NewDestruct y; Reflexivity Orelse Simpl; Tauto.
 Defined.
 
 Add Ring bool xorb andb true false [b:bool]b eqb BoolTheory [ true false ].
diff --git a/contrib/ring/Ring_abstract.v b/contrib/ring/Ring_abstract.v
index 05a6f68507..80d27e630d 100644
--- a/contrib/ring/Ring_abstract.v
+++ b/contrib/ring/Ring_abstract.v
@@ -208,7 +208,7 @@ Proof.
   Induction x.
   Intros; Simpl; EAuto.
 
-  Destruct y; Intros.
+  NewDestruct y; Intros.
 
   Simpl; Rewrite H; EAuto.
 
diff --git a/contrib/ring/Ring_normalize.v b/contrib/ring/Ring_normalize.v
index f44f554e0e..ae72f4eb4c 100644
--- a/contrib/ring/Ring_normalize.v
+++ b/contrib/ring/Ring_normalize.v
@@ -427,7 +427,7 @@ Save.
 Remark interp_m_ok : (x:A)(l:varlist)
   (interp_m x l)==(Amult x (interp_vl l)).
 Proof.
-  Destruct l.
+  NewDestruct l.
   Simpl; Trivial.
   Reflexivity.
 Save.
diff --git a/contrib/ring/Ring_theory.v b/contrib/ring/Ring_theory.v
index 8b4a0f95d3..1b787f4239 100644
--- a/contrib/ring/Ring_theory.v
+++ b/contrib/ring/Ring_theory.v
@@ -386,7 +386,7 @@ Definition Semi_Ring_Theory_of :
   (Azero : A)(Aopp : A -> A)(Aeq : A -> A -> bool)
   (Ring_Theory Aplus Amult Aone Azero Aopp Aeq)
     ->(Semi_Ring_Theory Aplus Amult Aone Azero Aeq).
-Destruct 1.
+Intros until 1; Case H.
 Split; Intros; Simpl; EAuto.
 Defined.
 
diff --git a/contrib/ring/Setoid_ring_normalize.v b/contrib/ring/Setoid_ring_normalize.v
index 9b74e8952c..04e2aa16ab 100644
--- a/contrib/ring/Setoid_ring_normalize.v
+++ b/contrib/ring/Setoid_ring_normalize.v
@@ -453,7 +453,7 @@ Save.
 Remark interp_m_ok : (x:A)(l:varlist)
   (Aequiv (interp_m x l) (Amult x (interp_vl l))).
 Proof.
-  Destruct l;Trivial.
+  NewDestruct l;Trivial.
 Save.
 
 Lemma canonical_sum_merge_ok : (x,y:canonical_sum)
diff --git a/contrib/ring/Setoid_ring_theory.v b/contrib/ring/Setoid_ring_theory.v
index 6428947ec0..a0d587eb34 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.
-Destruct 1.
+NewDestruct 1.
 Split; Intros; Simpl; EAuto.
 Defined.
 
-- 
cgit v1.2.3