- Added support for subterm matching in SearchAbout.

- Backtrack on precise unfolding of "iff" in "tauto": it has effects on
  the naming of hypotheses (especially when doing "case H" with H of
  type "{x|P<->Q}" since not unfolding will eventually introduce a name
  "i" while unfolding will eventually introduce a name "a" (deep sigh).
- Miscellaneous (error when a plugin is missing, doc hnf, standardization
  of names manipulating type constr_pattern, ...).



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

1 files changed, 0 insertions, 40 deletions

diff --git a/theories/ZArith/auxiliary.v b/theories/ZArith/auxiliary.v
index 18b49f4bb..5edf68013 100644
--- a/theories/ZArith/auxiliary.v
+++ b/theories/ZArith/auxiliary.v
@@ -91,46 +91,6 @@ Proof.
   rewrite Zplus_opp_r; trivial.
 Qed.
 
-(**********************************************************************)
-(** * Factorization lemmas *)
-
-Theorem Zred_factor0 : forall n:Z, n = n * 1.
-  intro x; rewrite (Zmult_1_r x); reflexivity.
-Qed.
-
-Theorem Zred_factor1 : forall n:Z, n + n = n * 2.
-Proof.
-  exact Zplus_diag_eq_mult_2.
-Qed.
-
-Theorem Zred_factor2 : forall n m:Z, n + n * m = n * (1 + m).
-Proof.
-  intros x y; pattern x at 1 in |- *; rewrite <- (Zmult_1_r x);
-    rewrite <- Zmult_plus_distr_r; trivial with arith.
-Qed.
-
-Theorem Zred_factor3 : forall n m:Z, n * m + n = n * (1 + m).
-Proof.
-  intros x y; pattern x at 2 in |- *; rewrite <- (Zmult_1_r x);
-    rewrite <- Zmult_plus_distr_r; rewrite Zplus_comm; 
-      trivial with arith.
-Qed.
-
-Theorem Zred_factor4 : forall n m p:Z, n * m + n * p = n * (m + p).
-Proof.
-  intros x y z; symmetry  in |- *; apply Zmult_plus_distr_r.
-Qed.
-
-Theorem Zred_factor5 : forall n m:Z, n * 0 + m = m.
-Proof.
-  intros x y; rewrite <- Zmult_0_r_reverse; auto with arith.
-Qed.
-
-Theorem Zred_factor6 : forall n:Z, n = n + 0.
-Proof.
-  intro; rewrite Zplus_0_r; trivial with arith.
-Qed.
-
 Theorem Zle_mult_approx :
   forall n m p:Z, n > 0 -> p > 0 -> 0 <= m -> 0 <= m * n + p.
 Proof.