Changement de list en listT, cons en consT et app en appT

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

3 files changed, 44 insertions, 44 deletions

diff --git a/contrib/field/Field_Compl.v b/contrib/field/Field_Compl.v
index bcf705fb6..75155be91 100644
--- a/contrib/field/Field_Compl.v
+++ b/contrib/field/Field_Compl.v
@@ -8,14 +8,14 @@
 
 (* $Id$ *)
 
-Inductive list [A:Type] : Type :=
-  nil : (list A) | cons : A->(list A)->(list A).
+Inductive listT [A:Type] : Type :=
+  nil : (listT A) | consT : A->(listT A)->(listT A).
 
-Fixpoint app [A:Type][l:(list A)] : (list A) -> (list A) :=
-  [m:(list A)]
+Fixpoint appT [A:Type][l:(listT A)] : (listT A) -> (listT A) :=
+  [m:(listT A)]
   Cases l of
   | nil => m 
-  | (cons a l1) => (cons A a (app A l1 m))
+  | (consT a l1) => (consT A a (appT A l1 m))
   end.
 
 Inductive Sprod [A:Type;B:Set] : Type :=
@@ -23,12 +23,12 @@ Inductive Sprod [A:Type;B:Set] : Type :=
 
 Definition assoc_2nd :=
 Fix assoc_2nd_rec {assoc_2nd_rec/4:
-  (A:Type)(B:Set)((e1,e2:B){e1=e2}+{~e1=e2})->(list (Sprod A B))->B->A->A:=
-    [A:Type;B:Set;eq_dec:(e1,e2:B){e1=e2}+{~e1=e2};lst:(list (Sprod A B));
+  (A:Type)(B:Set)((e1,e2:B){e1=e2}+{~e1=e2})->(listT (Sprod A B))->B->A->A:=
+    [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
-  | (cons (Spair v e) l) =>
+  | (consT (Spair v e) l) =>
     (Cases (eq_dec e key) of
     | (left _) => v
     | (right _) => (assoc_2nd_rec A B eq_dec l key default)
@@ -49,11 +49,11 @@ Definition sndT [A,B:Type;c:(prodT A B)] :=
   end.
 
 Definition mem :=
-Fix mem {mem/4:(A:Set)((e1,e2:A){e1=e2}+{~e1=e2})->(a:A)(list A)->bool :=
-  [A:Set;eq_dec:(e1,e2:A){e1=e2}+{~e1=e2};a:A;l:(list A)]
+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
-  | (cons a1 l1) =>
+  | (consT a1 l1) =>
     Cases (eq_dec a a1) of
     | (left _) => true
     | (right _) => (mem A eq_dec a l1)
diff --git a/contrib/field/Field_Tactic.v b/contrib/field/Field_Tactic.v
index 00f0cbe89..3fd8489b6 100644
--- a/contrib/field/Field_Tactic.v
+++ b/contrib/field/Field_Tactic.v
@@ -17,7 +17,7 @@ Require Export Field_Theory.
 Recursive Tactic Definition MemAssoc var lvar :=
   Match lvar With
   | [(nil ?)] -> false
-  | [(cons ? ?1 ?2)] ->
+  | [(consT ? ?1 ?2)] ->
     (Match ?1==var With
      | [?1== ?1] -> true
      | _ -> (MemAssoc var ?2)).
@@ -45,7 +45,7 @@ Recursive Tactic Definition SeekVarAux FT lvar trm :=
     Let res = (MemAssoc ?1 lvar) In
     Match res With
     | [(true)] -> lvar
-    | [(false)] -> '(cons AT ?1 lvar).
+    | [(false)] -> '(consT AT ?1 lvar).
 
 Tactic Definition SeekVar FT trm :=
   Let AT = Eval Compute in (A FT) In
@@ -54,9 +54,9 @@ Tactic Definition SeekVar FT trm :=
 Recursive Tactic Definition NumberAux lvar cpt :=
   Match lvar With
   | [(nil ?1)] -> '(nil (Sprod ?1 nat))
-  | [(cons ?1 ?2 ?3)] ->
+  | [(consT ?1 ?2 ?3)] ->
     Let l2 = (NumberAux ?3 '(S cpt)) In
-    '(cons (Sprod ?1 nat) (Spair ?1 nat ?2 cpt) l2).
+    '(consT (Sprod ?1 nat) (Spair ?1 nat ?2 cpt) l2).
 
 Tactic Definition Number lvar := (NumberAux lvar O).
 
@@ -67,7 +67,7 @@ Tactic Definition BuildVarList FT trm :=
 Recursive Tactic Definition Assoc elt lst :=
   Match lst With
   | [(nil ?)] -> Fail
-  | [(cons (Sprod ? nat) (Spair ? nat ?1 ?2) ?3)] ->
+  | [(consT (Sprod ? nat) (Spair ? nat ?1 ?2) ?3)] ->
     Match elt== ?1 With
     | [?1== ?1] -> ?2
     | _ -> (Assoc elt ?3).
@@ -110,22 +110,22 @@ Recursive Tactic Definition interp_A FT lvar trm :=
 Recursive Tactic Definition Remove e l :=
   Match l With
   | [(nil ?)] -> l
-  | [(cons ?1 e ?2)] -> ?2
-  | [(cons ?1 ?2 ?3)] ->
+  | [(consT ?1 e ?2)] -> ?2
+  | [(consT ?1 ?2 ?3)] ->
     Let nl = (Remove e ?3) In
-    '(cons ?1 ?2 nl).
+    '(consT ?1 ?2 nl).
 
 Recursive Tactic Definition Union l1 l2 :=
   Match l1 With
   | [(nil ?)] -> l2
-  | [(cons ?1 ?2 ?3)] ->
+  | [(consT ?1 ?2 ?3)] ->
     Let nl2 = (Remove ?2 l2) In
     Let nl = (Union ?3 nl2) In
-    '(cons ?1 ?2 nl).
+    '(consT ?1 ?2 nl).
 
 Recursive Tactic Definition RawGiveMult trm :=
   Match trm With
-  | [(EAinv ?1)] -> '(cons ExprA ?1 (nil ExprA))
+  | [(EAinv ?1)] -> '(consT ExprA ?1 (nil ExprA))
   | [(EAopp ?1)] -> (RawGiveMult ?1)
   | [(EAplus ?1 ?2)] ->
     Let l1 = (RawGiveMult ?1)
@@ -134,7 +134,7 @@ Recursive Tactic Definition RawGiveMult trm :=
   | [(EAmult ?1 ?2)] ->
     Let l1 = (RawGiveMult ?1)
     And l2 = (RawGiveMult ?2) In
-    Eval Compute in (app ExprA l1 l2)
+    Eval Compute in (appT ExprA l1 l2)
   | _ -> '(nil ExprA).
 
 Tactic Definition GiveMult trm :=
diff --git a/contrib/field/Field_Theory.v b/contrib/field/Field_Theory.v
index 9e5f95439..ee7cfd394 100644
--- a/contrib/field/Field_Theory.v
+++ b/contrib/field/Field_Theory.v
@@ -65,10 +65,10 @@ Definition eqExprA := Eval Compute in eqExprA_O.
 
 (**** Generation of the multiplier ****)
 
-Fixpoint mult_of_list [e:(list ExprA)]: ExprA :=
+Fixpoint mult_of_list [e:(listT ExprA)]: ExprA :=
   Cases e of
   | nil => EAone
-  | (cons e1 l1) => (EAmult e1 (mult_of_list l1))
+  | (consT e1 l1) => (EAmult e1 (mult_of_list l1))
   end.
 
 Section Theory_of_fields.
@@ -189,7 +189,7 @@ Save.
 
 (**** ExprA --> A ****)
 
-Fixpoint interp_ExprA [lvar:(list (Sprod AT nat));e:ExprA] : AT :=
+Fixpoint interp_ExprA [lvar:(listT (Sprod AT nat));e:ExprA] : AT :=
   Cases e of
   | EAzero         => AzeroT
   | EAone          => AoneT
@@ -254,7 +254,7 @@ Fixpoint assoc [e:ExprA] : ExprA :=
   end.
 
 Lemma merge_mult_correct1:
-  (e1,e2,e3:ExprA)(lvar:(list (Sprod AT nat)))
+  (e1,e2,e3:ExprA)(lvar:(listT (Sprod AT nat)))
   (interp_ExprA lvar (merge_mult (EAmult e1 e2) e3))==
   (interp_ExprA lvar (EAmult e1 (merge_mult e2 e3))).
 Proof.
@@ -268,7 +268,7 @@ Unfold 1 merge_mult;Fold merge_mult;
 Save.
 
 Lemma merge_mult_correct:
-  (e1,e2:ExprA)(lvar:(list (Sprod AT nat)))
+  (e1,e2:ExprA)(lvar:(listT (Sprod AT nat)))
     (interp_ExprA lvar (merge_mult e1 e2))==
     (interp_ExprA lvar (EAmult e1 e2)).
 Proof.
@@ -284,7 +284,7 @@ Intro H3;Rewrite H3;Rewrite <-H2;
 Ring.
 Save.
 
-Lemma assoc_mult_correct1:(e1,e2:ExprA)(lvar:(list (Sprod AT nat)))
+Lemma assoc_mult_correct1:(e1,e2:ExprA)(lvar:(listT (Sprod AT nat)))
   (AmultT (interp_ExprA lvar (assoc_mult e1)) 
          (interp_ExprA lvar (assoc_mult e2)))==
   (interp_ExprA lvar (assoc_mult (EAmult e1 e2))).
@@ -295,7 +295,7 @@ Rewrite <-(H e0 lvar);Simpl;Rewrite merge_mult_correct;Simpl;
 Save.
 
 Lemma assoc_mult_correct:
-  (e:ExprA)(lvar:(list (Sprod AT nat)))
+  (e:ExprA)(lvar:(listT (Sprod AT nat)))
     (interp_ExprA lvar (assoc_mult e))==(interp_ExprA lvar e).
 Proof.
 Induction e;Auto;Intros.
@@ -317,7 +317,7 @@ Simpl;Rewrite (H0 lvar);Auto.
 Save.
 
 Lemma merge_plus_correct1:
-  (e1,e2,e3:ExprA)(lvar:(list (Sprod AT nat)))
+  (e1,e2,e3:ExprA)(lvar:(listT (Sprod AT nat)))
   (interp_ExprA lvar (merge_plus (EAplus e1 e2) e3))==
   (interp_ExprA lvar (EAplus e1 (merge_plus e2 e3))).
 Proof.
@@ -331,7 +331,7 @@ Unfold 1 merge_plus;Fold merge_plus;
 Save.
 
 Lemma merge_plus_correct:
-  (e1,e2:ExprA)(lvar:(list (Sprod AT nat)))
+  (e1,e2:ExprA)(lvar:(listT (Sprod AT nat)))
     (interp_ExprA lvar (merge_plus e1 e2))==
     (interp_ExprA lvar (EAplus e1 e2)).
 Proof.
@@ -346,7 +346,7 @@ Intro H3;Rewrite H3;Rewrite <-H2;Rewrite merge_plus_correct1;Simpl;Ring.
 Ring.
 Save.
 
-Lemma assoc_plus_correct:(e1,e2:ExprA)(lvar:(list (Sprod AT nat)))
+Lemma assoc_plus_correct:(e1,e2:ExprA)(lvar:(listT (Sprod AT nat)))
   (AplusT (interp_ExprA lvar (assoc e1)) (interp_ExprA lvar (assoc e2)))==
   (interp_ExprA lvar (assoc (EAplus e1 e2))).
 Proof.
@@ -356,7 +356,7 @@ Rewrite <-(H e0 lvar);Simpl;Rewrite merge_plus_correct;Simpl;
 Save.
 
 Lemma assoc_correct:
-  (e:ExprA)(lvar:(list (Sprod AT nat)))
+  (e:ExprA)(lvar:(listT (Sprod AT nat)))
     (interp_ExprA lvar (assoc e))==(interp_ExprA lvar e).
 Proof.
 Induction e;Auto;Intros.
@@ -429,7 +429,7 @@ Fixpoint distrib_main [e:ExprA] : ExprA :=
 Definition distrib [e:ExprA] : ExprA := (distrib_main (distrib_EAopp e)).
 
 Lemma distrib_mult_right_correct:
-  (e1,e2:ExprA)(lvar:(list (Sprod AT nat)))
+  (e1,e2:ExprA)(lvar:(listT (Sprod AT nat)))
      (interp_ExprA lvar (distrib_mult_right e1 e2))==
      (AmultT (interp_ExprA lvar e1) (interp_ExprA lvar e2)).
 Proof.
@@ -439,7 +439,7 @@ Rewrite AmultT_sym;Rewrite AmultT_AplusT_distr;
 Save.
 
 Lemma distrib_mult_left_correct:
-  (e1,e2:ExprA)(lvar:(list (Sprod AT nat)))
+  (e1,e2:ExprA)(lvar:(listT (Sprod AT nat)))
      (interp_ExprA lvar (distrib_mult_left e1 e2))==
      (AmultT (interp_ExprA lvar e1)  (interp_ExprA lvar e2)).
 Proof.
@@ -460,7 +460,7 @@ Rewrite distrib_mult_right_correct;Simpl;Apply AmultT_sym.
 Save.
 
 Lemma distrib_correct:
-  (e:ExprA)(lvar:(list (Sprod AT nat)))
+  (e:ExprA)(lvar:(listT (Sprod AT nat)))
     (interp_ExprA lvar (distrib e))==(interp_ExprA lvar e).
 Proof.
 Induction e;Intros;Auto.
@@ -475,7 +475,7 @@ Save.
 (**** Multiplication by the inverse product ****)
 
 Lemma mult_eq:
-  (e1,e2,a:ExprA)(lvar:(list (Sprod AT nat)))
+  (e1,e2,a:ExprA)(lvar:(listT (Sprod AT nat)))
     ~((interp_ExprA lvar a)==AzeroT)->
       (interp_ExprA lvar (EAmult a e1))==(interp_ExprA lvar (EAmult a e2))->
         (interp_ExprA lvar e1)==(interp_ExprA lvar e2).
@@ -499,7 +499,7 @@ Definition multiply [e:ExprA] : ExprA :=
   end.
 
 Lemma multiply_aux_correct:
-  (a,e:ExprA)(lvar:(list (Sprod AT nat)))
+  (a,e:ExprA)(lvar:(listT (Sprod AT nat)))
     (interp_ExprA lvar (multiply_aux a e))==
     (AmultT (interp_ExprA lvar a) (interp_ExprA lvar e)).
 Proof.
@@ -508,7 +508,7 @@ Induction e;Simpl;Intros;Try (Rewrite merge_mult_correct);Auto.
 Save.
 
 Lemma multiply_correct:
-  (e:ExprA)(lvar:(list (Sprod AT nat)))
+  (e:ExprA)(lvar:(listT (Sprod AT nat)))
     (interp_ExprA lvar (multiply e))==(interp_ExprA lvar e).
 Proof.
   Induction e;Simpl;Auto.
@@ -556,7 +556,7 @@ Fixpoint inverse_simplif [a,e:ExprA] : ExprA :=
   end.
 
 Lemma monom_remove_correct:(e,a:ExprA)
-  (lvar:(list (Sprod AT nat)))~((interp_ExprA lvar a)==AzeroT)->
+  (lvar:(listT (Sprod AT nat)))~((interp_ExprA lvar a)==AzeroT)->
   (interp_ExprA lvar (monom_remove a e))==
   (AmultT (interp_ExprA lvar a) (interp_ExprA lvar e)).
 Proof.
@@ -583,7 +583,7 @@ Unfold monom_remove;Case (eqExprA (EAvar n) (EAinv a));Intros;
 Save.
 
 Lemma monom_simplif_rem_correct:(a,e:ExprA)
-  (lvar:(list (Sprod AT nat)))~((interp_ExprA lvar a)==AzeroT)->
+  (lvar:(listT (Sprod AT nat)))~((interp_ExprA lvar a)==AzeroT)->
   (interp_ExprA lvar (monom_simplif_rem a e))==
   (AmultT (interp_ExprA lvar a) (interp_ExprA lvar e)).
 Proof.
@@ -595,7 +595,7 @@ Ring.
 Save.
 
 Lemma monom_simplif_correct:(e,a:ExprA)
-  (lvar:(list (Sprod AT nat)))~((interp_ExprA lvar a)==AzeroT)->
+  (lvar:(listT (Sprod AT nat)))~((interp_ExprA lvar a)==AzeroT)->
   (interp_ExprA lvar (monom_simplif a e))==(interp_ExprA lvar e).
 Proof.
 Induction e;Intros;Auto.
@@ -605,7 +605,7 @@ Simpl;Trivial.
 Save.
 
 Lemma inverse_correct:
-  (e,a:ExprA)(lvar:(list (Sprod AT nat)))~((interp_ExprA lvar a)==AzeroT)->
+  (e,a:ExprA)(lvar:(listT (Sprod AT nat)))~((interp_ExprA lvar a)==AzeroT)->
     (interp_ExprA lvar (inverse_simplif a e))==(interp_ExprA lvar e).
 Proof.
 Induction e;Intros;Auto.