From 5b8a67e43421fb3cf574af403df6ac4dc7fc4a57 Mon Sep 17 00:00:00 2001 From: herbelin Date: Fri, 10 Oct 2003 19:19:53 +0000 Subject: Plus d'Eval Compute git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4584 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/ZArith/fast_integer.v | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/theories/ZArith/fast_integer.v b/theories/ZArith/fast_integer.v index 4ecc1b984e..180ab9fd2b 100644 --- a/theories/ZArith/fast_integer.v +++ b/theories/ZArith/fast_integer.v @@ -813,9 +813,9 @@ Qed. Lemma convert_xI : (p:positive) (convert (xI p))=(S (mult (2) (convert p))). Proof. Induction p. Unfold convert. Simpl. Intro p0. Intro. Rewrite positive_to_nat_2. - Rewrite positive_to_nat_4. Inversion H. Rewrite H1. Rewrite <- plus_Snm_nSm. Reflexivity. + Rewrite positive_to_nat_4; Injection H; Intro H1; Rewrite H1; Rewrite <- plus_Snm_nSm; Reflexivity. Unfold convert. Simpl. Intros. Rewrite positive_to_nat_2. Rewrite positive_to_nat_4. - Inversion H. Rewrite H1. Reflexivity. + Injection H; Intro H1; Rewrite H1; Reflexivity. Reflexivity. Qed. @@ -1305,7 +1305,7 @@ Definition Prec : (A:Set)A->(positive->A->A)->positive->A := (** Test *) -Eval Compute in +Check let fact = (Prec positive xH [p;r](times (add_un p) r)) in let seven = (xI (xI xH)) in let five_thousand_forty= (xO(xO(xO(xO(xI(xI(xO(xI(xI(xI(xO(xO xH)))))))))))) -- cgit v1.2.3