MAJ des Id pour coqweb

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

12 files changed, 14 insertions, 14 deletions

diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v
index 0d2e03bf2..f952f194e 100755
--- a/theories/Init/Datatypes.v
+++ b/theories/Init/Datatypes.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 (* [unit] is a singleton datatype with sole inhabitant [tt] *)
 
diff --git a/theories/Init/DatatypesSyntax.v b/theories/Init/DatatypesSyntax.v
index 2f0eb5cf2..fab21c52e 100644
--- a/theories/Init/DatatypesSyntax.v
+++ b/theories/Init/DatatypesSyntax.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 Require Export Datatypes.
 
diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v
index 0bf52ee2e..35b326d17 100755
--- a/theories/Init/Logic.v
+++ b/theories/Init/Logic.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 Require Datatypes.
 
diff --git a/theories/Init/LogicSyntax.v b/theories/Init/LogicSyntax.v
index fd394c1aa..872c19ae2 100644
--- a/theories/Init/LogicSyntax.v
+++ b/theories/Init/LogicSyntax.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 Require Export Logic.
 
diff --git a/theories/Init/Logic_Type.v b/theories/Init/Logic_Type.v
index b6a1fca71..eabcb3721 100755
--- a/theories/Init/Logic_Type.v
+++ b/theories/Init/Logic_Type.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 (* This module defines quantification on the world [Type] *)
 (* [Logic.v] was defining it on the world [Set] *)
diff --git a/theories/Init/Logic_TypeSyntax.v b/theories/Init/Logic_TypeSyntax.v
index 1c3f23dac..0b911c8b1 100644
--- a/theories/Init/Logic_TypeSyntax.v
+++ b/theories/Init/Logic_TypeSyntax.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 Require Logic_Type.
 
diff --git a/theories/Init/Peano.v b/theories/Init/Peano.v
index 9134127be..724c3db2e 100755
--- a/theories/Init/Peano.v
+++ b/theories/Init/Peano.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 (* Natural numbers [nat] built from [O] and [S] are defined in Datatypes.v *)
 (* This module defines the following operations on natural numbers :
@@ -113,8 +113,8 @@ Hints Resolve mult_n_O : core v62.
 
 Lemma mult_n_Sm : (n,m:nat) (plus (mult n m) n)=(mult n (S m)).
 Proof.
-  Intros; Elim n; Simpl; Auto.
-  Intros p H; Case H; Elim plus_n_Sm; Apply (f_equal nat nat S).
+  Intros n m; NewInduction n; Simpl; Auto.
+  Rewrite <- IHn; Rewrite -> plus_n_Sm.
   Pattern 1 3 m; Elim m; Simpl; Auto.
 Qed.
 Hints Resolve mult_n_Sm : core v62.
diff --git a/theories/Init/Prelude.v b/theories/Init/Prelude.v
index 8f8fa294e..5f647f373 100755
--- a/theories/Init/Prelude.v
+++ b/theories/Init/Prelude.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 Require Export Datatypes.
 Require Export DatatypesSyntax.
diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v
index 135f0f727..389b532f3 100755
--- a/theories/Init/Specif.v
+++ b/theories/Init/Specif.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 (**************************************************************)
 (* Basic specifications : Sets containing logical information *)
diff --git a/theories/Init/SpecifSyntax.v b/theories/Init/SpecifSyntax.v
index f732ced89..431f44fb7 100644
--- a/theories/Init/SpecifSyntax.v
+++ b/theories/Init/SpecifSyntax.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 Require LogicSyntax.
 Require Specif.
diff --git a/theories/Init/Wf.v b/theories/Init/Wf.v
index 87d5c720d..752dfbccd 100755
--- a/theories/Init/Wf.v
+++ b/theories/Init/Wf.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 (* This module proves the validity of
     - well-founded recursion (also called course of values)
diff --git a/theories/Setoids/Setoid.v b/theories/Setoids/Setoid.v
index 80dfe2d63..4e33e4728 100644
--- a/theories/Setoids/Setoid.v
+++ b/theories/Setoids/Setoid.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-(* $Id$: *)
+(*i $Id$: i*)
 
 Require Export Setoid_replace.