- 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

9 files changed, 40 insertions, 34 deletions

diff --git a/theories/Arith/Arith_base.v b/theories/Arith/Arith_base.v
index b076de2aff..2d54f0e8d9 100644
--- a/theories/Arith/Arith_base.v
+++ b/theories/Arith/Arith_base.v
@@ -18,3 +18,5 @@ Require Export Between.
 Require Export Peano_dec.
 Require Export Compare_dec.
 Require Export Factorial.
+Require Export EqNat.
+Require Export Wf_nat.
diff --git a/theories/Arith/Minus.v b/theories/Arith/Minus.v
index f5c3260de5..1bf6102e94 100644
--- a/theories/Arith/Minus.v
+++ b/theories/Arith/Minus.v
@@ -51,11 +51,18 @@ Qed.
 
 (** * Diagonal *)
 
-Lemma minus_n_n : forall n, 0 = n - n.
+Lemma minus_diag : forall n, n - n = 0.
 Proof.
   induction n; simpl in |- *; auto with arith.
 Qed.
-Hint Resolve minus_n_n: arith v62.
+
+Lemma minus_diag_reverse : forall n, 0 = n - n.
+Proof.
+  auto using minus_diag.
+Qed.
+Hint Resolve minus_diag_reverse: arith v62.
+
+Notation minus_n_n := minus_diag_reverse.
 
 (** * Simplification *)
 
diff --git a/theories/Arith/Wf_nat.v b/theories/Arith/Wf_nat.v
index 5e7ee41536..e87901080c 100644
--- a/theories/Arith/Wf_nat.v
+++ b/theories/Arith/Wf_nat.v
@@ -257,3 +257,22 @@ Proof.
     repeat split;
       assumption || intros n' (HPn',Hminn'); apply le_antisym; auto.
 Qed.
+
+Unset Implicit Arguments.
+
+(** [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.
+
+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.
diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v
index 25316c2782..17a645c8fa 100644
--- a/theories/Classes/RelationClasses.v
+++ b/theories/Classes/RelationClasses.v
@@ -388,7 +388,7 @@ Class [ equ : Equivalence A eqA, PreOrder A R ] => PartialOrder :=
 
 Instance partial_order_antisym [ PartialOrder A eqA R ] : ! Antisymmetric A eqA R.
 Proof with auto.
-  reduce_goal. pose partial_order_equivalence as poe. do 3 red in poe. 
+  reduce_goal. pose proof partial_order_equivalence as poe. do 3 red in poe. 
   apply <- poe. firstorder.
 Qed.
 
diff --git a/theories/Init/Tactics.v b/theories/Init/Tactics.v
index 602b119007..705fb3bdf5 100644
--- a/theories/Init/Tactics.v
+++ b/theories/Init/Tactics.v
@@ -77,15 +77,6 @@ Ltac case_eq x := generalize (refl_equal x); pattern x at -1; case x.
 Tactic Notation "rewrite_all" constr(eq) := repeat rewrite eq in *.
 Tactic Notation "rewrite_all" "<-" constr(eq) := repeat rewrite <- eq in *.
 
-(* Keeping a copy of an expression *)
-
-Ltac remembertac x a :=
-  let x := fresh x in
-  let H := fresh "Heq" x in
-  (set (x:=a) in *; assert (H: x=a) by reflexivity; clearbody x).
-
-Tactic Notation "remember" constr(c) "as" ident(x) := remembertac x c.
-
 (** Tactics for applying equivalences.
 
 The following code provides tactics "apply -> t", "apply <- t",
diff --git a/theories/Numbers/Cyclic/Int31/Int31.v b/theories/Numbers/Cyclic/Int31/Int31.v
index 59c2029a37..12c0cc2642 100644
--- a/theories/Numbers/Cyclic/Int31/Int31.v
+++ b/theories/Numbers/Cyclic/Int31/Int31.v
@@ -11,6 +11,7 @@
 (*i $Id$ i*)
 
 Require Import NaryFunctions.
+Require Import Wf_nat.
 Require Export ZArith.
 Require Export DoubleType.
 
diff --git a/theories/Program/Tactics.v b/theories/Program/Tactics.v
index c8c0c8b169..946fdf6185 100644
--- a/theories/Program/Tactics.v
+++ b/theories/Program/Tactics.v
@@ -26,8 +26,8 @@ Ltac destruct_pairs := repeat (destruct_one_pair).
 (** Destruct one existential package, keeping the name of the hypothesis for the first component. *)
 
 Ltac destruct_one_ex :=
-  let tac H := let ph := fresh "H" in destruct H as [H ph] in
-  let tacT H := let ph := fresh "X" in destruct H as [H ph] in
+  let tac H := let ph := fresh "H" in (destruct H as [H ph]) in
+  let tacT H := let ph := fresh "X" in (destruct H as [H ph]) in
     match goal with
       | [H : (ex _) |- _] => tac H
       | [H : (sig ?P) |- _ ] => tac H
@@ -120,20 +120,20 @@ Ltac on_call f tac :=
 (* Destructs calls to f in hypothesis or conclusion, useful if f creates a subset object. *)
 
 Ltac destruct_call f :=
-  let tac t := destruct t in on_call f tac.
+  let tac t := (destruct t) in on_call f tac.
 
 Ltac destruct_calls f := repeat destruct_call f.
 
 Ltac destruct_call_in f H :=
-  let tac t := destruct t in
+  let tac t := (destruct t) in
   let T := type of H in
     on_application f tac T.
 
 Ltac destruct_call_as f l :=
-  let tac t := destruct t as l in on_call f tac.
+  let tac t := (destruct t as l) in on_call f tac.
 
 Ltac destruct_call_as_in f l H :=
-  let tac t := destruct t as l in
+  let tac t := (destruct t as l) in
   let T := type of H in
     on_application f tac T.
 
@@ -200,8 +200,6 @@ Ltac add_hypothesis H' p :=
     end
   end.
 
-Tactic Notation "pose" constr(c) "as" ident(H) := assert(H:=c).
-
 (** A tactic to replace an hypothesis by another term. *)
 
 Ltac replace_hyp H c :=
diff --git a/theories/ZArith/Zmisc.v b/theories/ZArith/Zmisc.v
index b05acd7306..c99582a25f 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.
diff --git a/theories/ZArith/Zpower.v b/theories/ZArith/Zpower.v
index f3f357de11..7ee8b97667 100644
--- a/theories/ZArith/Zpower.v
+++ b/theories/ZArith/Zpower.v
@@ -8,6 +8,7 @@
 
 (*i $Id$ i*)
 
+Require Import Wf_nat.
 Require Import ZArith_base.
 Require Export Zpow_def.
 Require Import Omega.