- Extension de "generalize" en "generalize c as id at occs".

- Ajout clause "in" à "remember" (et passage du code en ML).
- Ajout clause "in" à "induction"/"destruct" qui, en ce cas, ajoute
  aussi une égalité pour se souvenir du terme sur lequel l'induction
  ou l'analyse de cas s'applique.
- Ajout "pose t as id" en standard (Matthieu: j'ai enlevé celui de
  Programs qui avait la sémantique de "pose proof" tandis que le nouveau
  a la même sémantique que "pose (id:=t)").
- Un peu de réorganisation, uniformisation de noms dans Arith, et
  ajout EqNat dans Arith.
- Documentation tactiques et notations de tactiques.



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11072 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 1 insertions, 14 deletions

diff --git a/theories/ZArith/Zmisc.v b/theories/ZArith/Zmisc.v
index b05acd730..c99582a25 100644
--- a/theories/ZArith/Zmisc.v
+++ b/theories/ZArith/Zmisc.v
@@ -8,6 +8,7 @@
 
 (*i $Id$ i*)
 
+Require Import Wf_nat.
 Require Import BinInt.
 Require Import Zcompare.
 Require Import Zorder.
@@ -18,11 +19,6 @@ Open Local Scope Z_scope.
 (** Iterators *)
 
 (** [n]th iteration of the function [f] *)
-Fixpoint iter_nat (n:nat) (A:Type) (f:A -> A) (x:A) {struct n} : A :=
-  match n with
-    | O => x
-    | S n' => f (iter_nat n' A f x)
-  end.
 
 Fixpoint iter_pos (n:positive) (A:Type) (f:A -> A) (x:A) {struct n} : A :=
   match n with
@@ -38,15 +34,6 @@ Definition iter (n:Z) (A:Type) (f:A -> A) (x:A) :=
     | Zneg p => x
   end.
 
-Theorem iter_nat_plus :
-  forall (n m:nat) (A:Type) (f:A -> A) (x:A),
-    iter_nat (n + m) A f x = iter_nat n A f (iter_nat m A f x).
-Proof.    
-  simple induction n;
-    [ simpl in |- *; auto with arith
-      | intros; simpl in |- *; apply f_equal with (f := f); apply H ].  
-Qed.
-
 Theorem iter_nat_of_P :
   forall (p:positive) (A:Type) (f:A -> A) (x:A),
     iter_pos p A f x = iter_nat (nat_of_P p) A f x.