Implicit Variables Type

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

18 files changed, 48 insertions, 12 deletions

diff --git a/theories/Arith/Bool_nat.v b/theories/Arith/Bool_nat.v
index bbe1475f5..ff7f0ab5c 100644
--- a/theories/Arith/Bool_nat.v
+++ b/theories/Arith/Bool_nat.v
@@ -13,6 +13,8 @@ Require Export Peano_dec.
 Require Sumbool.
 Import nat_scope.
 
+Implicit Variables Type m,n,x,y:nat.
+
 (** The decidability of equality and order relations over
     type [nat] give some boolean functions with the adequate specification. *)
 
diff --git a/theories/Arith/Compare.v b/theories/Arith/Compare.v
index 5b12033dc..5d7f1e42c 100755
--- a/theories/Arith/Compare.v
+++ b/theories/Arith/Compare.v
@@ -11,9 +11,14 @@
 (** Equality is decidable on [nat] *)
 Import nat_scope.
 
+(*
 Lemma not_eq_sym : (A:Set)(p,q:A)(~p=q) -> ~(q=p).
 Proof sym_not_eq.
 Hints Immediate not_eq_sym : arith.
+*)
+Notation not_eq_sym := sym_not_eq.
+
+Implicit Variables Type m,n,p,q:nat.
 
 Require Arith.
 Require Peano_dec.
diff --git a/theories/Arith/Compare_dec.v b/theories/Arith/Compare_dec.v
index 735d267d6..c30b90fae 100755
--- a/theories/Arith/Compare_dec.v
+++ b/theories/Arith/Compare_dec.v
@@ -14,6 +14,8 @@ Require Gt.
 Require Decidable.
 Import nat_scope.
 
+Implicit Variables Type m,n,x,y:nat.
+
 Definition zerop : (n:nat){n=O}+{lt O n}.
 NewDestruct n; Auto with arith.
 Defined.
diff --git a/theories/Arith/Div.v b/theories/Arith/Div.v
index e4b0300dd..ed41c5a93 100755
--- a/theories/Arith/Div.v
+++ b/theories/Arith/Div.v
@@ -15,6 +15,8 @@ Require Le.
 Require Euclid_def.
 Require Compare_dec.
 
+Implicit Variables Type n,a,b,q,r:nat.
+
 Fixpoint inf_dec [n:nat] : nat->bool :=
       [m:nat] Cases n m of
                   O     _     => true
diff --git a/theories/Arith/Div2.v b/theories/Arith/Div2.v
index dd0cc8458..a6782c5f8 100644
--- a/theories/Arith/Div2.v
+++ b/theories/Arith/Div2.v
@@ -14,6 +14,8 @@ Require Compare_dec.
 Require Even.
 Import nat_scope.
 
+Implicit Variables Type n:nat.
+
 (** Here we define [n/2] and prove some of its properties *)
 
 Fixpoint div2 [n:nat] : nat :=
diff --git a/theories/Arith/EqNat.v b/theories/Arith/EqNat.v
index 88cca274b..c42deebd2 100755
--- a/theories/Arith/EqNat.v
+++ b/theories/Arith/EqNat.v
@@ -9,8 +9,11 @@
 (*i $Id$ i*)
 
 (** Equality on natural numbers *)
+
 Import nat_scope.
 
+Implicit Variables Type m,n,x,y:nat.
+
 Fixpoint  eq_nat [n:nat] : nat -> Prop :=
   [m:nat]Cases n m of 
                 O      O     => True
diff --git a/theories/Arith/Euclid.v b/theories/Arith/Euclid.v
index 173a90638..7f4e325be 100644
--- a/theories/Arith/Euclid.v
+++ b/theories/Arith/Euclid.v
@@ -13,6 +13,7 @@ Require Compare_dec.
 Require Wf_nat.
 Import nat_scope.
 
+Implicit Variables Type a,b,n,q,r:nat.
 
 Inductive diveucl [a,b:nat] : Set 
       := divex : (q,r:nat)(gt b r)->(a=(plus (mult q b) r))->(diveucl a b).
diff --git a/theories/Arith/Even.v b/theories/Arith/Even.v
index 034a60088..ca0637955 100644
--- a/theories/Arith/Even.v
+++ b/theories/Arith/Even.v
@@ -11,8 +11,11 @@
 (** Here we define the predicates [even] and [odd] by mutual induction
     and we prove the decidability and the exclusion of those predicates.
     The main results about parity are proved in the module Div2. *)
+
 Import nat_scope.
 
+Implicit Variables Type m,n:nat.
+
 Inductive even : nat->Prop :=
     even_O : (even O)
   | even_S : (n:nat)(odd n)->(even (S n))
diff --git a/theories/Arith/Gt.v b/theories/Arith/Gt.v
index 6b55c5bd3..d4bc8531d 100755
--- a/theories/Arith/Gt.v
+++ b/theories/Arith/Gt.v
@@ -13,6 +13,8 @@ Require Lt.
 Require Plus.
 Import nat_scope.
 
+Implicit Variables Type m,n,p:nat.
+
 Theorem gt_Sn_O : (n:nat)(gt (S n) O).
 Proof.
   Auto with arith.
diff --git a/theories/Arith/Le.v b/theories/Arith/Le.v
index 7765187cf..5321637be 100755
--- a/theories/Arith/Le.v
+++ b/theories/Arith/Le.v
@@ -12,6 +12,8 @@
 Import nat_scope.
 Open Scope nat_scope.
 
+Implicit Variables Type m,n,p:nat.
+
 Theorem le_n_S : (n,m:nat)(le n m)->(le (S n) (S m)).
 Proof.
   NewInduction 1; Auto.
diff --git a/theories/Arith/Lt.v b/theories/Arith/Lt.v
index 96541cb9f..94bb00c8f 100755
--- a/theories/Arith/Lt.v
+++ b/theories/Arith/Lt.v
@@ -11,6 +11,8 @@
 Require Le.
 Import nat_scope.
 
+Implicit Variables Type m,n,p:nat.
+
 Theorem lt_n_Sn : (n:nat)(lt n (S n)).
 Proof.
 Auto with arith.
diff --git a/theories/Arith/Max.v b/theories/Arith/Max.v
index 8a599ed7e..8b4c86cd5 100755
--- a/theories/Arith/Max.v
+++ b/theories/Arith/Max.v
@@ -9,8 +9,11 @@
 (*i $Id$ i*)
 
 Require Arith.
+
 Import nat_scope.
 
+Implicit Variables Type m,n:nat.
+
 (** maximum of two natural numbers *)
 
 Fixpoint max [n:nat] : nat -> nat :=  
diff --git a/theories/Arith/Min.v b/theories/Arith/Min.v
index 650b95380..a762a06d5 100755
--- a/theories/Arith/Min.v
+++ b/theories/Arith/Min.v
@@ -9,8 +9,11 @@
 (*i $Id$ i*)
 
 Require Arith.
+
 Import nat_scope.
 
+Implicit Variables Type m,n:nat.
+
 (** minimum of two natural numbers *)
 
 Fixpoint min [n:nat] : nat -> nat :=  
diff --git a/theories/Arith/Minus.v b/theories/Arith/Minus.v
index 42f44083a..de06c097a 100755
--- a/theories/Arith/Minus.v
+++ b/theories/Arith/Minus.v
@@ -14,12 +14,7 @@ Require Lt.
 Require Le.
 Import nat_scope.
 
-Fixpoint minus [n:nat] : nat -> nat := 
-  [m:nat]Cases n m of
-            O    _     =>  O
-         | (S k) O     => (S k)
-         | (S k) (S l) => (minus k l)
-        end. 
+Implicit Variables Type m,n,p:nat.
 
 Lemma minus_plus_simpl : 
 	(n,m,p:nat)((minus n m)=(minus (plus p n) (plus p m))).
diff --git a/theories/Arith/Mult.v b/theories/Arith/Mult.v
index 1daf8567c..7c2ea25cd 100755
--- a/theories/Arith/Mult.v
+++ b/theories/Arith/Mult.v
@@ -13,6 +13,8 @@ Require Export Minus.
 Require Export Lt.
 Import nat_scope.
 
+Implicit Variables Type m,n,p:nat.
+
 (** Multiplication *)
 
 Lemma mult_plus_distr : 
diff --git a/theories/Arith/Peano_dec.v b/theories/Arith/Peano_dec.v
index e998e0b7c..c5f0ecdcc 100755
--- a/theories/Arith/Peano_dec.v
+++ b/theories/Arith/Peano_dec.v
@@ -9,8 +9,11 @@
 (*i $Id$ i*)
 
 Require Decidable.
+
 Import nat_scope.
 
+Implicit Variables Type m,n,x,y:nat.
+
 Theorem O_or_S : (n:nat)({m:nat|(S m)=n})+{O=n}.
 Proof.
 NewInduction n.
diff --git a/theories/Arith/Plus.v b/theories/Arith/Plus.v
index 3ad37d13a..debad4ca7 100755
--- a/theories/Arith/Plus.v
+++ b/theories/Arith/Plus.v
@@ -15,6 +15,8 @@ Require Lt.
 
 Import nat_scope.
 
+Implicit Variables Type m,n,p,q:nat.
+
 Lemma plus_sym : (n,m:nat)(n+m)=(m+n).
 Proof.
 Intros n m ; Elim n ; Simpl ; Auto with arith.
@@ -150,11 +152,11 @@ Proof.
   Simpl in H. Discriminate H.
 Defined.
 
-Lemma plus_permute_2_in_4 : (a,b,c,d:nat) ((a+b)+(c+d))=((a+c)+(b+d)).
+Lemma plus_permute_2_in_4 : (m,n,p,q:nat) ((m+n)+(p+q))=((m+p)+(n+q)).
 Proof.
   Intros. 
-  Rewrite <- (plus_assoc_l a b (c+d)). Rewrite (plus_assoc_l b c d).
-  Rewrite (plus_sym b c). Rewrite <- (plus_assoc_l c b d). Apply plus_assoc_l.
+  Rewrite <- (plus_assoc_l m n (p+q)). Rewrite (plus_assoc_l n p q).
+  Rewrite (plus_sym n p). Rewrite <- (plus_assoc_l p n q). Apply plus_assoc_l.
 Qed.
 
 
@@ -164,10 +166,10 @@ Qed.
     tail-recursive, whereas [plus] is not. This can be useful
     when extracting programs. *)
 
-Fixpoint plus_acc [s,n:nat] : nat := 
+Fixpoint plus_acc [q,n:nat] : nat := 
    Cases n of 
-      O => s
-      | (S p) => (plus_acc (S s) p)
+      O => q
+      | (S p) => (plus_acc (S q) p)
     end.
 
 Definition tail_plus := [n,m:nat](plus_acc m n).
diff --git a/theories/Arith/Wf_nat.v b/theories/Arith/Wf_nat.v
index b0c715c8b..0c299bd37 100755
--- a/theories/Arith/Wf_nat.v
+++ b/theories/Arith/Wf_nat.v
@@ -14,6 +14,8 @@ Require Lt.
 
 Import nat_scope.
 
+Implicit Variables Type m,n,p:nat.
+
 Chapter  Well_founded_Nat.
 
 Variable A : Set.