diff options
| author | herbelin | 2003-10-10 19:19:53 +0000 |
|---|---|---|
| committer | herbelin | 2003-10-10 19:19:53 +0000 |
| commit | 5b8a67e43421fb3cf574af403df6ac4dc7fc4a57 (patch) | |
| tree | c58940e15f8387a2bce0ec134b3d04ab1d1e0391 | |
| parent | 49898a533578846598c7d8a62e8de2f1fcca84c0 (diff) | |
Plus d'Eval Compute
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4584 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | theories/ZArith/fast_integer.v | 6 |
1 files 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)))))))))))) |