aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2002-01-09 17:08:58 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2002-01-09 17:08:58 +0000
commit5719b93a439912b0fa1f32f4bb1d0369186e50ed (patch)
tree0133a8f477350e3bd41fc5c24e9955d1a5b5bea0 /theories
parent7cfe7d097e6f47bde2ef2dc7fbcaef340944bbd4 (diff)
MAJ des Id pour coqweb
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2384 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories')
-rwxr-xr-xtheories/Init/Datatypes.v2
-rw-r--r--theories/Init/DatatypesSyntax.v2
-rwxr-xr-xtheories/Init/Logic.v2
-rw-r--r--theories/Init/LogicSyntax.v2
-rwxr-xr-xtheories/Init/Logic_Type.v2
-rw-r--r--theories/Init/Logic_TypeSyntax.v2
-rwxr-xr-xtheories/Init/Peano.v6
-rwxr-xr-xtheories/Init/Prelude.v2
-rwxr-xr-xtheories/Init/Specif.v2
-rw-r--r--theories/Init/SpecifSyntax.v2
-rwxr-xr-xtheories/Init/Wf.v2
-rw-r--r--theories/Setoids/Setoid.v2
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.