From e0d682ec25282a348d35c5b169abafec48555690 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Mon, 20 Aug 2012 18:27:01 +0200
Subject: Imported Upstream version 8.4dfsg

---
 theories/Arith/Mult.v | 24 ++++++++++++------------
 1 file changed, 12 insertions(+), 12 deletions(-)

(limited to 'theories/Arith/Mult.v')

diff --git a/theories/Arith/Mult.v b/theories/Arith/Mult.v
index 479138a9..cbb9b376 100644
--- a/theories/Arith/Mult.v
+++ b/theories/Arith/Mult.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -11,7 +11,7 @@ Require Export Minus.
 Require Export Lt.
 Require Export Le.
 
-Open Local Scope nat_scope.
+Local Open Scope nat_scope.
 
 Implicit Types m n p : nat.
 
@@ -23,7 +23,7 @@ Implicit Types m n p : nat.
 
 Lemma mult_0_r : forall n, n * 0 = 0.
 Proof.
-  intro; symmetry  in |- *; apply mult_n_O.
+  intro; symmetry ; apply mult_n_O.
 Qed.
 
 Lemma mult_0_l : forall n, 0 * n = 0.
@@ -35,7 +35,7 @@ Qed.
 
 Lemma mult_1_l : forall n, 1 * n = n.
 Proof.
-  simpl in |- *; auto with arith.
+  simpl; auto with arith.
 Qed.
 Hint Resolve mult_1_l: arith v62.
 
@@ -68,12 +68,12 @@ Hint Resolve mult_plus_distr_r: arith v62.
 Lemma mult_plus_distr_l : forall n m p, n * (m + p) = n * m + n * p.
 Proof.
   induction n. trivial.
-  intros. simpl in |- *. rewrite IHn. symmetry. apply plus_permute_2_in_4.
+  intros. simpl. rewrite IHn. symmetry. apply plus_permute_2_in_4.
 Qed.
 
 Lemma mult_minus_distr_r : forall n m p, (n - m) * p = n * p - m * p.
 Proof.
-  intros; induction n m using nat_double_ind; simpl; auto with arith.
+  intros; induction n, m using nat_double_ind; simpl; auto with arith.
   rewrite <- minus_plus_simpl_l_reverse; auto with arith.
 Qed.
 Hint Resolve mult_minus_distr_r: arith v62.
@@ -137,13 +137,13 @@ Qed.
 
 Lemma mult_O_le : forall n m, m = 0 \/ n <= m * n.
 Proof.
-  induction m; simpl in |- *; auto with arith.
+  induction m; simpl; auto with arith.
 Qed.
 Hint Resolve mult_O_le: arith v62.
 
 Lemma mult_le_compat_l : forall n m p, n <= m -> p * n <= p * m.
 Proof.
-  induction p as [| p IHp]; intros; simpl in |- *.
+  induction p as [| p IHp]; intros; simpl.
   apply le_n.
   auto using plus_le_compat.
 Qed.
@@ -167,7 +167,7 @@ Proof.
   assumption.
   apply le_plus_l.
   (* m*p<=m0*q -> m*p<=(S m0)*q *)
-  simpl in |- *; apply le_trans with (m0 * q).
+  simpl; apply le_trans with (m0 * q).
   assumption.
   apply le_plus_r.
 Qed.
@@ -232,7 +232,7 @@ Fixpoint mult_acc (s:nat) m n : nat :=
 
 Lemma mult_acc_aux : forall n m p, m + n * p = mult_acc m p n.
 Proof.
-  induction n as [| p IHp]; simpl in |- *; auto.
+  induction n as [| p IHp]; simpl; auto.
   intros s m; rewrite <- plus_tail_plus; rewrite <- IHp.
   rewrite <- plus_assoc_reverse; apply f_equal2; auto.
   rewrite plus_comm; auto.
@@ -242,7 +242,7 @@ Definition tail_mult n m := mult_acc 0 m n.
 
 Lemma mult_tail_mult : forall n m, n * m = tail_mult n m.
 Proof.
-  intros; unfold tail_mult in |- *; rewrite <- mult_acc_aux; auto.
+  intros; unfold tail_mult; rewrite <- mult_acc_aux; auto.
 Qed.
 
 (** [TailSimpl] transforms any [tail_plus] and [tail_mult] into [plus]
@@ -250,4 +250,4 @@ Qed.
 
 Ltac tail_simpl :=
   repeat rewrite <- plus_tail_plus; repeat rewrite <- mult_tail_mult;
-    simpl in |- *.
+    simpl.
-- 
cgit v1.2.3