oubli: changement de nil en nilT

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

3 files changed, 13 insertions, 13 deletions

diff --git a/contrib/field/Field_Compl.v b/contrib/field/Field_Compl.v
index 75155be91..514edf39c 100644
--- a/contrib/field/Field_Compl.v
+++ b/contrib/field/Field_Compl.v
@@ -9,12 +9,12 @@
 (* $Id$ *)
 
 Inductive listT [A:Type] : Type :=
-  nil : (listT A) | consT : A->(listT A)->(listT A).
+  nilT : (listT A) | consT : A->(listT A)->(listT A).
 
 Fixpoint appT [A:Type][l:(listT A)] : (listT A) -> (listT A) :=
   [m:(listT A)]
   Cases l of
-  | nil => m 
+  | nilT => m 
   | (consT a l1) => (consT A a (appT A l1 m))
   end.
 
@@ -27,7 +27,7 @@ Fix assoc_2nd_rec {assoc_2nd_rec/4:
     [A:Type;B:Set;eq_dec:(e1,e2:B){e1=e2}+{~e1=e2};lst:(listT (Sprod A B));
       key:B;default:A]
   Cases lst of
-  | nil => default
+  | nilT => default
   | (consT (Spair v e) l) =>
     (Cases (eq_dec e key) of
     | (left _) => v
@@ -52,7 +52,7 @@ Definition mem :=
 Fix mem {mem/4:(A:Set)((e1,e2:A){e1=e2}+{~e1=e2})->(a:A)(listT A)->bool :=
   [A:Set;eq_dec:(e1,e2:A){e1=e2}+{~e1=e2};a:A;l:(listT A)]
   Cases l of
-  | nil => false
+  | nilT => false
   | (consT a1 l1) =>
     Cases (eq_dec a a1) of
     | (left _) => true
diff --git a/contrib/field/Field_Tactic.v b/contrib/field/Field_Tactic.v
index 3fd8489b6..c3002a552 100644
--- a/contrib/field/Field_Tactic.v
+++ b/contrib/field/Field_Tactic.v
@@ -16,7 +16,7 @@ Require Export Field_Theory.
 
 Recursive Tactic Definition MemAssoc var lvar :=
   Match lvar With
-  | [(nil ?)] -> false
+  | [(nilT ?)] -> false
   | [(consT ? ?1 ?2)] ->
     (Match ?1==var With
      | [?1== ?1] -> true
@@ -49,11 +49,11 @@ Recursive Tactic Definition SeekVarAux FT lvar trm :=
 
 Tactic Definition SeekVar FT trm :=
   Let AT = Eval Compute in (A FT) In
-  (SeekVarAux FT '(nil AT) trm).
+  (SeekVarAux FT '(nilT AT) trm).
 
 Recursive Tactic Definition NumberAux lvar cpt :=
   Match lvar With
-  | [(nil ?1)] -> '(nil (Sprod ?1 nat))
+  | [(nilT ?1)] -> '(nilT (Sprod ?1 nat))
   | [(consT ?1 ?2 ?3)] ->
     Let l2 = (NumberAux ?3 '(S cpt)) In
     '(consT (Sprod ?1 nat) (Spair ?1 nat ?2 cpt) l2).
@@ -66,7 +66,7 @@ Tactic Definition BuildVarList FT trm :=
 
 Recursive Tactic Definition Assoc elt lst :=
   Match lst With
-  | [(nil ?)] -> Fail
+  | [(nilT ?)] -> Fail
   | [(consT (Sprod ? nat) (Spair ? nat ?1 ?2) ?3)] ->
     Match elt== ?1 With
     | [?1== ?1] -> ?2
@@ -109,7 +109,7 @@ Recursive Tactic Definition interp_A FT lvar trm :=
 
 Recursive Tactic Definition Remove e l :=
   Match l With
-  | [(nil ?)] -> l
+  | [(nilT ?)] -> l
   | [(consT ?1 e ?2)] -> ?2
   | [(consT ?1 ?2 ?3)] ->
     Let nl = (Remove e ?3) In
@@ -117,7 +117,7 @@ Recursive Tactic Definition Remove e l :=
 
 Recursive Tactic Definition Union l1 l2 :=
   Match l1 With
-  | [(nil ?)] -> l2
+  | [(nilT ?)] -> l2
   | [(consT ?1 ?2 ?3)] ->
     Let nl2 = (Remove ?2 l2) In
     Let nl = (Union ?3 nl2) In
@@ -125,7 +125,7 @@ Recursive Tactic Definition Union l1 l2 :=
 
 Recursive Tactic Definition RawGiveMult trm :=
   Match trm With
-  | [(EAinv ?1)] -> '(consT ExprA ?1 (nil ExprA))
+  | [(EAinv ?1)] -> '(consT ExprA ?1 (nilT ExprA))
   | [(EAopp ?1)] -> (RawGiveMult ?1)
   | [(EAplus ?1 ?2)] ->
     Let l1 = (RawGiveMult ?1)
@@ -135,7 +135,7 @@ Recursive Tactic Definition RawGiveMult trm :=
     Let l1 = (RawGiveMult ?1)
     And l2 = (RawGiveMult ?2) In
     Eval Compute in (appT ExprA l1 l2)
-  | _ -> '(nil ExprA).
+  | _ -> '(nilT ExprA).
 
 Tactic Definition GiveMult trm :=
   Let ltrm = (RawGiveMult trm) In
diff --git a/contrib/field/Field_Theory.v b/contrib/field/Field_Theory.v
index ee7cfd394..54cc9609e 100644
--- a/contrib/field/Field_Theory.v
+++ b/contrib/field/Field_Theory.v
@@ -67,7 +67,7 @@ Definition eqExprA := Eval Compute in eqExprA_O.
 
 Fixpoint mult_of_list [e:(listT ExprA)]: ExprA :=
   Cases e of
-  | nil => EAone
+  | nilT => EAone
   | (consT e1 l1) => (EAmult e1 (mult_of_list l1))
   end.