- Déplacement des types paramétriques prod, sum, option, identity,

  sig, sig2, sumor, list et vector dans Type
- Branchement de prodT/listT vers les nouveaux prod/list
- Abandon sigS/sigS2 au profit de sigT et du nouveau sigT2
- Changements en conséquence dans les théories (notamment Field_Tactic),
  ainsi que dans les modules ML Coqlib/Equality/Hipattern/Field


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

4 files changed, 76 insertions, 95 deletions

diff --git a/contrib/field/Field_Compl.v b/contrib/field/Field_Compl.v
index 200d0f7e6..746e7c997 100644
--- a/contrib/field/Field_Compl.v
+++ b/contrib/field/Field_Compl.v
@@ -8,54 +8,31 @@
 
 (* $Id$ *)
 
-Inductive listT (A:Type) : Type :=
-  | nilT : listT A
-  | consT : A -> listT A -> listT A.
-
-Fixpoint appT (A:Type) (l m:listT A) {struct l} : listT A :=
-  match l with
-  | nilT => m
-  | consT a l1 => consT A a (appT A l1 m)
-  end.
-
-Inductive prodT (A B:Type) : Type :=
-    pairT : A -> B -> prodT A B.
+Require Import List.
 
 Definition assoc_2nd :=
   (fix assoc_2nd_rec (A:Type) (B:Set)
                      (eq_dec:forall e1 e2:B, {e1 = e2} + {e1 <> e2})
-                     (lst:listT (prodT A B)) {struct lst} : 
+                     (lst:list (prod A B)) {struct lst} : 
    B -> A -> A :=
      fun (key:B) (default:A) =>
        match lst with
-       | nilT => default
-       | consT (pairT v e) l =>
+       | nil => default
+       | (v,e) :: l =>
            match eq_dec e key with
            | left _ => v
            | right _ => assoc_2nd_rec A B eq_dec l key default
            end
        end).
 
-Definition fstT (A B:Type) (c:prodT A B) := match c with
-                                            | pairT a _ => a
-                                            end.
-
-Definition sndT (A B:Type) (c:prodT A B) := match c with
-                                            | pairT _ a => a
-                                            end.
-
 Definition mem :=
   (fix mem (A:Set) (eq_dec:forall e1 e2:A, {e1 = e2} + {e1 <> e2}) 
-           (a:A) (l:listT A) {struct l} : bool :=
+           (a:A) (l:list A) {struct l} : bool :=
      match l with
-     | nilT => false
-     | consT a1 l1 =>
+     | nil => false
+     | a1 :: l1 =>
          match eq_dec a a1 with
          | left _ => true
          | right _ => mem A eq_dec a l1
          end
      end).
-
-Inductive field_rel_option (A:Type) : Type :=
-  | Field_None : field_rel_option A
-  | Field_Some : (A -> A -> A) -> field_rel_option A.
\ No newline at end of file
diff --git a/contrib/field/Field_Tactic.v b/contrib/field/Field_Tactic.v
index 72306409c..fb6a31e99 100644
--- a/contrib/field/Field_Tactic.v
+++ b/contrib/field/Field_Tactic.v
@@ -8,6 +8,7 @@
 
 (* $Id$ *)
 
+Require Import List.
 Require Import Ring.
 Require Export Field_Compl.
 Require Export Field_Theory.
@@ -20,8 +21,8 @@ Ltac body_of s := eval cbv beta iota delta [s] in s.
 
 Ltac mem_assoc var lvar :=
   match constr:lvar with
-  | (nilT _) => constr:false
-  | (consT _ ?X1 ?X2) =>
+  | nil => constr:false
+  | ?X1 :: ?X2 =>
       match constr:(X1 = var) with
       | (?X1 = ?X1) => constr:true
       | _ => mem_assoc var X2
@@ -31,10 +32,10 @@ Ltac mem_assoc var lvar :=
 Ltac number lvar := 
   let rec number_aux lvar cpt :=
     match constr:lvar with
-    | (nilT ?X1) => constr:(nilT (prodT X1 nat))
-    | (consT ?X1 ?X2 ?X3) =>
+    | (@nil ?X1) => constr:(@nil (prod X1 nat))
+    | ?X2 :: ?X3 =>
         let l2 := number_aux X3 (S cpt) in
-        constr:(consT (prodT X1 nat) (pairT X1 nat X2 cpt) l2) 
+        constr:((X2,cpt) :: l2) 
     end
   in number_aux lvar 0.
 
@@ -62,17 +63,17 @@ Ltac build_varlist FT trm :=
         let res := mem_assoc X1 lvar in
         match constr:res with
         | true => lvar
-        | false => constr:(consT AT X1 lvar)
+        | false => constr:(X1 :: lvar)
         end
     end in
   let AT := get_component A FT in
-  let lvar := seek_var (nilT AT) trm in
+  let lvar := seek_var (@nil AT) trm in
   number lvar.
 
 Ltac assoc elt lst :=
   match constr:lst with
-  | (nilT _) => fail
-  | (consT (prodT _ nat) (pairT _ nat ?X1 ?X2) ?X3) =>
+  | nil => fail
+  | (?X1,?X2) :: ?X3 =>
       match constr:(elt = X1) with
       | (?X1 = ?X1) => constr:X2
       | _ => assoc elt X3
@@ -113,32 +114,31 @@ Ltac interp_A FT lvar trm :=
 
 Ltac remove e l :=
   match constr:l with
-  | (nilT _) => l
-  | (consT ?X1 e ?X2) => constr:X2
-  | (consT ?X1 ?X2 ?X3) => let nl := remove e X3 in
-                           constr:(consT X1 X2 nl)
+  | nil => l
+  | e :: ?X2 => constr:X2
+  | ?X2 :: ?X3 => let nl := remove e X3 in constr:(X2 :: nl)
   end.
 
 Ltac union l1 l2 :=
   match constr:l1 with
-  | (nilT _) => l2
-  | (consT ?X1 ?X2 ?X3) =>
+  | nil => l2
+  | ?X2 :: ?X3 =>
       let nl2 := remove X2 l2 in
       let nl := union X3 nl2 in
-      constr:(consT X1 X2 nl)
+      constr:(X2 :: nl)
   end.
 
 Ltac raw_give_mult trm :=
   match constr:trm with
-  | (EAinv ?X1) => constr:(consT ExprA X1 (nilT ExprA))
+  | (EAinv ?X1) => constr:(X1 :: nil)
   | (EAopp ?X1) => raw_give_mult X1
   | (EAplus ?X1 ?X2) =>
       let l1 := raw_give_mult X1 with l2 := raw_give_mult X2 in
       union l1 l2
   | (EAmult ?X1 ?X2) =>
       let l1 := raw_give_mult X1 with l2 := raw_give_mult X2 in
-      eval compute in (appT ExprA l1 l2)
-  | _ => constr:(nilT ExprA)
+      eval compute in (app l1 l2)
+  | _ => constr:(@nil ExprA)
   end.
 
 Ltac give_mult trm :=
@@ -254,13 +254,13 @@ Ltac apply_simplif sfun :=
 
 Ltac unfolds FT :=
   match get_component Aminus FT with
-  | (Field_Some _ ?X1) => unfold X1 in |- *
+  | Some ?X1 => unfold X1 in |- *
   | _ => idtac
   end;
-   match get_component Adiv FT with
-   | (Field_Some _ ?X1) => unfold X1 in |- *
-   | _ => idtac
-   end.
+  match get_component Adiv FT with
+  | Some ?X1 => unfold X1 in |- *
+  | _ => idtac
+  end.
 
 Ltac reduce FT :=
   let AzeroT := get_component Azero FT
@@ -304,11 +304,11 @@ Ltac field_gen FT := unfolds FT; (inverse_test FT; ring) || field_gen_aux FT.
 Ltac init_exp FT trm :=
   let e :=
    (match get_component Aminus FT with
-    | (Field_Some _ ?X1) => eval cbv beta delta [X1] in trm
+    | Some ?X1 => eval cbv beta delta [X1] in trm
     | _ => trm
     end) in
   match get_component Adiv FT with
-  | (Field_Some _ ?X1) => eval cbv beta delta [X1] in e
+  | Some ?X1 => eval cbv beta delta [X1] in e
   | _ => e
   end.
 
@@ -341,21 +341,21 @@ Ltac simpl_inv trm :=
 
 Ltac map_tactic fcn lst :=
   match constr:lst with
-  | (nilT _) => lst
-  | (consT ?X1 ?X2 ?X3) =>
+  | nil => lst
+  | ?X2 :: ?X3 =>
       let r := fcn X2 with t := map_tactic fcn X3 in
-      constr:(consT X1 r t)
+      constr:(r :: t)
   end.
 
 Ltac build_monom_aux lst trm :=
   match constr:lst with
-  | (nilT _) => eval compute in (assoc trm)
-  | (consT _ ?X1 ?X2) => build_monom_aux X2 (EAmult trm X1)
+  | nil => eval compute in (assoc trm)
+  | ?X1 :: ?X2 => build_monom_aux X2 (EAmult trm X1)
   end.
 
 Ltac build_monom lnum lden :=
   let ildn := map_tactic ltac:(fun e => constr:(EAinv e)) lden in
-  let ltot := eval compute in (appT ExprA lnum ildn) in
+  let ltot := eval compute in (app lnum ildn) in
   let trm := build_monom_aux ltot EAone in
   match constr:trm with
   | (EAmult _ ?X1) => constr:X1
@@ -370,7 +370,7 @@ Ltac simpl_monom_aux lnum lden trm :=
       | true =>
           let newlnum := remove X1 lnum in
           simpl_monom_aux newlnum lden X2
-      | false => simpl_monom_aux lnum (consT ExprA X1 lden) X2
+      | false => simpl_monom_aux lnum (X1 :: lden) X2
       end
   | (EAmult ?X1 ?X2) =>
       let mma := mem_assoc X1 lden in
@@ -378,7 +378,7 @@ Ltac simpl_monom_aux lnum lden trm :=
       | true =>
           let newlden := remove X1 lden in
           simpl_monom_aux lnum newlden X2
-      | false => simpl_monom_aux (consT ExprA X1 lnum) lden X2
+      | false => simpl_monom_aux (X1 :: lnum) lden X2
       end
   | (EAinv ?X1) =>
       let mma := mem_assoc X1 lnum in
@@ -386,7 +386,7 @@ Ltac simpl_monom_aux lnum lden trm :=
       | true =>
           let newlnum := remove X1 lnum in
           build_monom newlnum lden
-      | false => build_monom lnum (consT ExprA X1 lden)
+      | false => build_monom lnum (X1 :: lden)
       end
   | ?X1 =>
       let mma := mem_assoc X1 lden in
@@ -394,11 +394,11 @@ Ltac simpl_monom_aux lnum lden trm :=
       | true =>
           let newlden := remove X1 lden in
           build_monom lnum newlden
-      | false => build_monom (consT ExprA X1 lnum) lden
+      | false => build_monom (X1 :: lnum) lden
       end
   end.
 
-Ltac simpl_monom trm := simpl_monom_aux (nilT ExprA) (nilT ExprA) trm.
+Ltac simpl_monom trm := simpl_monom_aux (@nil ExprA) (@nil ExprA) trm.
 
 Ltac simpl_all_monomials trm :=
   match constr:trm with
diff --git a/contrib/field/Field_Theory.v b/contrib/field/Field_Theory.v
index 7fdf61bb4..5fe69ddca 100644
--- a/contrib/field/Field_Theory.v
+++ b/contrib/field/Field_Theory.v
@@ -8,6 +8,7 @@
 
 (* $Id$ *)
 
+Require Import List.
 Require Import Peano_dec.
 Require Import Ring.
 Require Import Field_Compl.
@@ -21,8 +22,8 @@ Record Field_Theory : Type :=
    Aopp : A -> A;
    Aeq : A -> A -> bool;
    Ainv : A -> A;
-   Aminus : field_rel_option A;
-   Adiv : field_rel_option A;
+   Aminus : option (A -> A -> A);
+   Adiv : option (A -> A -> A);
    RT : Ring_Theory Aplus Amult Aone Azero Aopp Aeq;
    Th_inv_def : forall n:A, n <> Azero -> Amult (Ainv n) n = Aone}.
 
@@ -66,10 +67,10 @@ Definition eqExprA := Eval compute in eqExprA_O.
 
 (**** Generation of the multiplier ****)
 
-Fixpoint mult_of_list (e:listT ExprA) : ExprA :=
+Fixpoint mult_of_list (e:list ExprA) : ExprA :=
   match e with
-  | nilT => EAone
-  | consT e1 l1 => EAmult e1 (mult_of_list l1)
+  | nil => EAone
+  | e1 :: l1 => EAmult e1 (mult_of_list l1)
   end.
 
 Section Theory_of_fields.
@@ -191,7 +192,7 @@ Qed.
 
 (**** ExprA --> A ****)
 
-Fixpoint interp_ExprA (lvar:listT (prodT AT nat)) (e:ExprA) {struct e} :
+Fixpoint interp_ExprA (lvar:list (AT * nat)) (e:ExprA) {struct e} :
  AT :=
   match e with
   | EAzero => AzeroT
@@ -257,7 +258,7 @@ Fixpoint assoc (e:ExprA) : ExprA :=
   end.
 
 Lemma merge_mult_correct1 :
- forall (e1 e2 e3:ExprA) (lvar:listT (prodT AT nat)),
+ forall (e1 e2 e3:ExprA) (lvar:list (AT * nat)),
    interp_ExprA lvar (merge_mult (EAmult e1 e2) e3) =
    interp_ExprA lvar (EAmult e1 (merge_mult e2 e3)).
 Proof.
@@ -271,7 +272,7 @@ unfold merge_mult at 1 in |- *; fold merge_mult in |- *;
 Qed.
 
 Lemma merge_mult_correct :
- forall (e1 e2:ExprA) (lvar:listT (prodT AT nat)),
+ forall (e1 e2:ExprA) (lvar:list (AT * nat)),
    interp_ExprA lvar (merge_mult e1 e2) = interp_ExprA lvar (EAmult e1 e2).
 Proof.
 simple induction e1; auto; intros.
@@ -290,7 +291,7 @@ ring.
 Qed.
 
 Lemma assoc_mult_correct1 :
- forall (e1 e2:ExprA) (lvar:listT (prodT AT nat)),
+ forall (e1 e2:ExprA) (lvar:list (AT * nat)),
    AmultT (interp_ExprA lvar (assoc_mult e1))
      (interp_ExprA lvar (assoc_mult e2)) =
    interp_ExprA lvar (assoc_mult (EAmult e1 e2)).
@@ -302,7 +303,7 @@ rewrite <- (H e0 lvar); simpl in |- *; rewrite merge_mult_correct;
 Qed.
 
 Lemma assoc_mult_correct :
- forall (e:ExprA) (lvar:listT (prodT AT nat)),
+ forall (e:ExprA) (lvar:list (AT * nat)),
    interp_ExprA lvar (assoc_mult e) = interp_ExprA lvar e.
 Proof.
 simple induction e; auto; intros.
@@ -325,7 +326,7 @@ simpl in |- *; rewrite (H0 lvar); auto.
 Qed.
 
 Lemma merge_plus_correct1 :
- forall (e1 e2 e3:ExprA) (lvar:listT (prodT AT nat)),
+ forall (e1 e2 e3:ExprA) (lvar:list (AT * nat)),
    interp_ExprA lvar (merge_plus (EAplus e1 e2) e3) =
    interp_ExprA lvar (EAplus e1 (merge_plus e2 e3)).
 Proof.
@@ -339,7 +340,7 @@ unfold merge_plus at 1 in |- *; fold merge_plus in |- *;
 Qed.
 
 Lemma merge_plus_correct :
- forall (e1 e2:ExprA) (lvar:listT (prodT AT nat)),
+ forall (e1 e2:ExprA) (lvar:list (AT * nat)),
    interp_ExprA lvar (merge_plus e1 e2) = interp_ExprA lvar (EAplus e1 e2).
 Proof.
 simple induction e1; auto; intros.
@@ -358,7 +359,7 @@ ring.
 Qed.
 
 Lemma assoc_plus_correct :
- forall (e1 e2:ExprA) (lvar:listT (prodT AT nat)),
+ forall (e1 e2:ExprA) (lvar:list (AT * nat)),
    AplusT (interp_ExprA lvar (assoc e1)) (interp_ExprA lvar (assoc e2)) =
    interp_ExprA lvar (assoc (EAplus e1 e2)).
 Proof.
@@ -369,7 +370,7 @@ rewrite <- (H e0 lvar); simpl in |- *; rewrite merge_plus_correct;
 Qed.
 
 Lemma assoc_correct :
- forall (e:ExprA) (lvar:listT (prodT AT nat)),
+ forall (e:ExprA) (lvar:list (AT * nat)),
    interp_ExprA lvar (assoc e) = interp_ExprA lvar e.
 Proof.
 simple induction e; auto; intros.
@@ -448,7 +449,7 @@ Fixpoint distrib_main (e:ExprA) : ExprA :=
 Definition distrib (e:ExprA) : ExprA := distrib_main (distrib_EAopp e).
 
 Lemma distrib_mult_right_correct :
- forall (e1 e2:ExprA) (lvar:listT (prodT AT nat)),
+ forall (e1 e2:ExprA) (lvar:list (AT * nat)),
    interp_ExprA lvar (distrib_mult_right e1 e2) =
    AmultT (interp_ExprA lvar e1) (interp_ExprA lvar e2).
 Proof.
@@ -458,7 +459,7 @@ rewrite AmultT_sym; rewrite AmultT_AplusT_distr; rewrite (H e2 lvar);
 Qed.
 
 Lemma distrib_mult_left_correct :
- forall (e1 e2:ExprA) (lvar:listT (prodT AT nat)),
+ forall (e1 e2:ExprA) (lvar:list (AT * nat)),
    interp_ExprA lvar (distrib_mult_left e1 e2) =
    AmultT (interp_ExprA lvar e1) (interp_ExprA lvar e2).
 Proof.
@@ -480,7 +481,7 @@ rewrite distrib_mult_right_correct; simpl in |- *; apply AmultT_sym.
 Qed.
 
 Lemma distrib_correct :
- forall (e:ExprA) (lvar:listT (prodT AT nat)),
+ forall (e:ExprA) (lvar:list (AT * nat)),
    interp_ExprA lvar (distrib e) = interp_ExprA lvar e.
 Proof.
 simple induction e; intros; auto.
@@ -496,7 +497,7 @@ Qed.
 (**** Multiplication by the inverse product ****)
 
 Lemma mult_eq :
- forall (e1 e2 a:ExprA) (lvar:listT (prodT AT nat)),
+ forall (e1 e2 a:ExprA) (lvar:list (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.
@@ -520,7 +521,7 @@ Definition multiply (e:ExprA) : ExprA :=
   end.
 
 Lemma multiply_aux_correct :
- forall (a e:ExprA) (lvar:listT (prodT AT nat)),
+ forall (a e:ExprA) (lvar:list (AT * nat)),
    interp_ExprA lvar (multiply_aux a e) =
    AmultT (interp_ExprA lvar a) (interp_ExprA lvar e).
 Proof.
@@ -530,7 +531,7 @@ simple induction e; simpl in |- *; intros; try rewrite merge_mult_correct;
 Qed.
 
 Lemma multiply_correct :
- forall (e:ExprA) (lvar:listT (prodT AT nat)),
+ forall (e:ExprA) (lvar:list (AT * nat)),
    interp_ExprA lvar (multiply e) = interp_ExprA lvar e.
 Proof.
   simple induction e; simpl in |- *; auto.
@@ -578,7 +579,7 @@ Fixpoint inverse_simplif (a e:ExprA) {struct e} : ExprA :=
   end.
 
 Lemma monom_remove_correct :
- forall (e a:ExprA) (lvar:listT (prodT AT nat)),
+ forall (e a:ExprA) (lvar:list (AT * nat)),
    interp_ExprA lvar a <> AzeroT ->
    interp_ExprA lvar (monom_remove a e) =
    AmultT (interp_ExprA lvar a) (interp_ExprA lvar e).
@@ -608,7 +609,7 @@ unfold monom_remove in |- *; case (eqExprA (EAvar n) (EAinv a)); intros;
 Qed.
 
 Lemma monom_simplif_rem_correct :
- forall (a e:ExprA) (lvar:listT (prodT AT nat)),
+ forall (a e:ExprA) (lvar:list (AT * nat)),
    interp_ExprA lvar a <> AzeroT ->
    interp_ExprA lvar (monom_simplif_rem a e) =
    AmultT (interp_ExprA lvar a) (interp_ExprA lvar e).
@@ -622,7 +623,7 @@ ring.
 Qed.
 
 Lemma monom_simplif_correct :
- forall (e a:ExprA) (lvar:listT (prodT AT nat)),
+ forall (e a:ExprA) (lvar:list (AT * nat)),
    interp_ExprA lvar a <> AzeroT ->
    interp_ExprA lvar (monom_simplif a e) = interp_ExprA lvar e.
 Proof.
@@ -633,7 +634,7 @@ simpl in |- *; trivial.
 Qed.
 
 Lemma inverse_correct :
- forall (e a:ExprA) (lvar:listT (prodT AT nat)),
+ forall (e a:ExprA) (lvar:list (AT * nat)),
    interp_ExprA lvar a <> AzeroT ->
    interp_ExprA lvar (inverse_simplif a e) = interp_ExprA lvar e.
 Proof.
@@ -642,4 +643,4 @@ simpl in |- *; rewrite (H0 a lvar H1); rewrite monom_simplif_correct; auto.
 unfold inverse_simplif in |- *; rewrite monom_simplif_correct; auto.
 Qed.
 
-End Theory_of_fields.
\ No newline at end of file
+End Theory_of_fields.
diff --git a/contrib/field/field.ml4 b/contrib/field/field.ml4
index 90a986385..8e33f6292 100644
--- a/contrib/field/field.ml4
+++ b/contrib/field/field.ml4
@@ -22,19 +22,22 @@ open Vernacinterp
 open Vernacexpr
 open Tacexpr
 open Mod_subst
+open Coqlib
 
 (* Interpretation of constr's *)
 let constr_of c = Constrintern.interp_constr Evd.empty (Global.env()) c
 
 (* Construction of constants *)
-let constant dir s = Coqlib.gen_constant "Field" ("field"::dir) s
+let constant dir s = gen_constant "Field" ("field"::dir) s
+let init_constant s = gen_constant_in_modules "Field" init_modules s
 
 (* To deal with the optional arguments *)
 let constr_of_opt a opt =
   let ac = constr_of a in
+  let ac3 = mkArrow ac (mkArrow ac ac) in
   match opt with
-  | None -> mkApp ((constant ["Field_Compl"] "Field_None"),[|ac|])
-  | Some f -> mkApp ((constant ["Field_Compl"] "Field_Some"),[|ac;constr_of f|])
+  | None -> mkApp (init_constant "None",[|ac3|])
+  | Some f -> mkApp (init_constant "Some",[|ac3;constr_of f|])
 
 (* Table of theories *)
 let th_tab = ref (Gmap.empty : (constr,constr) Gmap.t)