From 3a91cd07b9399ed66b3b554b0aa173a541b4a87a Mon Sep 17 00:00:00 2001 From: herbelin Date: Mon, 22 May 2000 17:12:57 +0000 Subject: Changement nommage des hypothèses; parenthèses pour les tactiques MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@462 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Arith/Div2.v | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/theories/Arith/Div2.v b/theories/Arith/Div2.v index 2040c00c4..5520e179d 100644 --- a/theories/Arith/Div2.v +++ b/theories/Arith/Div2.v @@ -60,8 +60,8 @@ Intro H. Absurd (div2 (S O))=(div2 (S (S O))). Simpl. Discriminate. Assumption. Split; Auto with arith. (* n = (S (S n')) *) -Intros. Decompose [and] H. Unfold iff in H1 H2. -Decompose [and] H1. Decompose [and] H2. Clear H H1 H2. +Intros. Decompose [and] H. Unfold iff in H0 H1. +Decompose [and] H0. Decompose [and] H1. Clear H H0 H1. Split; Split; Auto with arith. Intro H. Inversion H. Inversion H1. Change (S (div2 n0))=(S (div2 (S n0))). Auto with arith. @@ -109,8 +109,8 @@ Intro H. Inversion H. Split; Split; Auto with arith. Intro H. Inversion H. Inversion H1. (* n = (S (S n')) *) -Intros. Decompose [and] H. Unfold iff in H1 H2. -Decompose [and] H1. Decompose [and] H2. Clear H H1 H2. +Intros. Decompose [and] H. Unfold iff in H0 H1. +Decompose [and] H0. Decompose [and] H1. Clear H H0 H1. Split; Split. Intro H. Inversion H. Inversion H1. Simpl. Rewrite (double_S (div2 n0)). Auto with arith. -- cgit v1.2.3