mise a jour du nouveau ring et ajout du nouveau field, avant renommages

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

10 files changed, 41 insertions, 37 deletions

diff --git a/contrib/ring/ArithRing.v b/contrib/ring/ArithRing.v
index 0d42dabfd..959d66c74 100644
--- a/contrib/ring/ArithRing.v
+++ b/contrib/ring/ArithRing.v
@@ -10,7 +10,8 @@
 
 (* Instantiation of the Ring tactic for the naturals of Arith $*)
 
-Require Export Ring.
+Require Import Bool.
+Require Export LegacyRing.
 Require Export Arith.
 Require Import Eqdep_dec.
 
@@ -36,12 +37,12 @@ Hint Resolve nateq_prop: arithring.
 
 Definition NatTheory : Semi_Ring_Theory plus mult 1 0 nateq.
   split; intros; auto with arith arithring.
-  apply (fun n m p:nat => plus_reg_l m p n) with (n := n).
-  trivial.
+(*  apply (fun n m p:nat => plus_reg_l m p n) with (n := n).
+  trivial.*)
 Defined.
 
 
-Add Semi Ring nat plus mult 1 0 nateq NatTheory [ 0 S ].
+Add Legacy Semi Ring nat plus mult 1 0 nateq NatTheory [ 0 S ].
 
 Goal forall n:nat, S n = 1 + n.
 intro; reflexivity.
diff --git a/contrib/ring/Ring.v b/contrib/ring/LegacyRing.v
index d0c2b7da3..667e24d53 100644
--- a/contrib/ring/Ring.v
+++ b/contrib/ring/LegacyRing.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: Ring.v 5920 2004-07-16 20:01:26Z herbelin $ *)
 
 Require Export Bool.
 Require Export Ring_theory.
@@ -32,5 +32,5 @@ destruct n; destruct m; destruct p; reflexivity.
 destruct x; destruct y; reflexivity || simpl in |- *; tauto.
 Defined.
 
-Add Ring bool xorb andb true false (fun b:bool => b) eqb BoolTheory
- [ true false ].
\ No newline at end of file
+Add Legacy Ring bool xorb andb true false (fun b:bool => b) eqb BoolTheory
+ [ true false ].
diff --git a/contrib/ring/NArithRing.v b/contrib/ring/NArithRing.v
index 41e3a7d7b..ee9fb3761 100644
--- a/contrib/ring/NArithRing.v
+++ b/contrib/ring/NArithRing.v
@@ -10,7 +10,8 @@
 
 (* Instantiation of the Ring tactic for the binary natural numbers *)
 
-Require Export Ring.
+Require Import Bool.
+Require Export LegacyRing.
 Require Export ZArith_base.
 Require Import NArith.
 Require Import Eqdep_dec.
@@ -37,8 +38,9 @@ Definition NTheory : Semi_Ring_Theory Nplus Nmult 1%N 0%N Neq.
     apply Nmult_1_l.
     apply Nmult_0_l.
     apply Nmult_plus_distr_r.
-    apply Nplus_reg_l.
+(*    apply Nplus_reg_l.*)
     apply Neq_prop.
 Qed.
 
-Add Semi Ring N Nplus Nmult 1%N 0%N Neq NTheory [ Npos 0%N xO xI 1%positive ].
+Add Legacy Semi Ring
+  N Nplus Nmult 1%N 0%N Neq NTheory [ Npos 0%N xO xI 1%positive ].
diff --git a/contrib/ring/Ring_abstract.v b/contrib/ring/Ring_abstract.v
index 5d5046393..574c24421 100644
--- a/contrib/ring/Ring_abstract.v
+++ b/contrib/ring/Ring_abstract.v
@@ -129,7 +129,7 @@ Hint Resolve (SR_mult_zero_left T).
 Hint Resolve (SR_mult_zero_left2 T).
 Hint Resolve (SR_distr_left T).
 Hint Resolve (SR_distr_left2 T).
-Hint Resolve (SR_plus_reg_left T).
+(*Hint Resolve (SR_plus_reg_left T).*)
 Hint Resolve (SR_plus_permute T).
 Hint Resolve (SR_mult_permute T).
 Hint Resolve (SR_distr_right T).
@@ -140,7 +140,7 @@ Hint Resolve (SR_plus_zero_right T).
 Hint Resolve (SR_plus_zero_right2 T).
 Hint Resolve (SR_mult_one_right T).
 Hint Resolve (SR_mult_one_right2 T).
-Hint Resolve (SR_plus_reg_right T).
+(*Hint Resolve (SR_plus_reg_right T).*)
 Hint Resolve refl_equal sym_equal trans_equal.
 (*Hints Resolve refl_eqT sym_eqT trans_eqT.*)
 Hint Immediate T.
@@ -439,7 +439,7 @@ Hint Resolve (Th_mult_zero_left T).
 Hint Resolve (Th_mult_zero_left2 T).
 Hint Resolve (Th_distr_left T).
 Hint Resolve (Th_distr_left2 T).
-Hint Resolve (Th_plus_reg_left T).
+(*Hint Resolve (Th_plus_reg_left T).*)
 Hint Resolve (Th_plus_permute T).
 Hint Resolve (Th_mult_permute T).
 Hint Resolve (Th_distr_right T).
@@ -449,7 +449,7 @@ Hint Resolve (Th_plus_zero_right T).
 Hint Resolve (Th_plus_zero_right2 T).
 Hint Resolve (Th_mult_one_right T).
 Hint Resolve (Th_mult_one_right2 T).
-Hint Resolve (Th_plus_reg_right T).
+(*Hint Resolve (Th_plus_reg_right T).*)
 Hint Resolve refl_equal sym_equal trans_equal.
 (*Hints Resolve refl_eqT sym_eqT trans_eqT.*)
 Hint Immediate T.
diff --git a/contrib/ring/Ring_normalize.v b/contrib/ring/Ring_normalize.v
index bd22fa39a..6d0d05778 100644
--- a/contrib/ring/Ring_normalize.v
+++ b/contrib/ring/Ring_normalize.v
@@ -356,7 +356,7 @@ Hint Resolve (SR_mult_zero_left T).
 Hint Resolve (SR_mult_zero_left2 T).
 Hint Resolve (SR_distr_left T).
 Hint Resolve (SR_distr_left2 T).
-Hint Resolve (SR_plus_reg_left T).
+(*Hint Resolve (SR_plus_reg_left T).*)
 Hint Resolve (SR_plus_permute T).
 Hint Resolve (SR_mult_permute T).
 Hint Resolve (SR_distr_right T).
@@ -367,7 +367,7 @@ Hint Resolve (SR_plus_zero_right T).
 Hint Resolve (SR_plus_zero_right2 T).
 Hint Resolve (SR_mult_one_right T).
 Hint Resolve (SR_mult_one_right2 T).
-Hint Resolve (SR_plus_reg_right T).
+(*Hint Resolve (SR_plus_reg_right T).*)
 Hint Resolve refl_equal sym_equal trans_equal.
 (* Hints Resolve refl_eqT sym_eqT trans_eqT. *)
 Hint Immediate T.
@@ -785,7 +785,7 @@ Hint Resolve (Th_mult_zero_left T).
 Hint Resolve (Th_mult_zero_left2 T).
 Hint Resolve (Th_distr_left T).
 Hint Resolve (Th_distr_left2 T).
-Hint Resolve (Th_plus_reg_left T).
+(*Hint Resolve (Th_plus_reg_left T).*)
 Hint Resolve (Th_plus_permute T).
 Hint Resolve (Th_mult_permute T).
 Hint Resolve (Th_distr_right T).
@@ -796,7 +796,7 @@ Hint Resolve (Th_plus_zero_right T).
 Hint Resolve (Th_plus_zero_right2 T).
 Hint Resolve (Th_mult_one_right T).
 Hint Resolve (Th_mult_one_right2 T).
-Hint Resolve (Th_plus_reg_right T).
+(*Hint Resolve (Th_plus_reg_right T).*)
 Hint Resolve refl_equal sym_equal trans_equal.
 (*Hints Resolve refl_eqT sym_eqT trans_eqT.*)
 Hint Immediate T.
diff --git a/contrib/ring/Ring_theory.v b/contrib/ring/Ring_theory.v
index 31cc274b2..192ff1f57 100644
--- a/contrib/ring/Ring_theory.v
+++ b/contrib/ring/Ring_theory.v
@@ -39,7 +39,7 @@ Record Semi_Ring_Theory : Prop :=
    SR_mult_one_left : forall n:A, 1 * n = n;
    SR_mult_zero_left : forall n:A, 0 * n = 0;
    SR_distr_left : forall n m p:A, (n + m) * p = n * p + m * p;
-   SR_plus_reg_left : forall n m p:A, n + m = n + p -> m = p;
+(*   SR_plus_reg_left : forall n m p:A, n + m = n + p -> m = p;*)
    SR_eq_prop : forall x y:A, Is_true (Aeq x y) -> x = y}.
 
 Variable T : Semi_Ring_Theory.
@@ -52,10 +52,10 @@ Let plus_zero_left := SR_plus_zero_left T.
 Let mult_one_left := SR_mult_one_left T. 
 Let mult_zero_left := SR_mult_zero_left T.
 Let distr_left := SR_distr_left T.
-Let plus_reg_left := SR_plus_reg_left T.
+(*Let plus_reg_left := SR_plus_reg_left T.*)
 
 Hint Resolve plus_comm plus_assoc mult_comm mult_assoc plus_zero_left
-  mult_one_left mult_zero_left distr_left plus_reg_left.
+  mult_one_left mult_zero_left distr_left (*plus_reg_left*).
 
 (* Lemmas whose form is x=y are also provided in form y=x because Auto does
   not symmetry *) 
@@ -126,11 +126,11 @@ Qed.
 Lemma SR_mult_one_right2 : forall n:A, n = n * 1.
 intro; elim mult_comm; auto.
 Qed.
-
+(*
 Lemma SR_plus_reg_right : forall n m p:A, m + n = p + n -> m = p.
 intros n m p; rewrite (plus_comm m n); rewrite (plus_comm p n); eauto.
 Qed.
-
+*)
 End Theory_of_semi_rings.
 
 Section Theory_of_rings.
@@ -320,7 +320,7 @@ symmetry  in |- *; apply Th_mult_opp_opp. Qed.
 Lemma Th_opp_zero : - 0 = 0.
 rewrite <- (plus_zero_left (- 0)).
 auto. Qed.
-
+(*
 Lemma Th_plus_reg_left : forall n m p:A, n + m = n + p -> m = p.
 intros; generalize (f_equal (fun z => - n + z) H).
 repeat rewrite plus_assoc.
@@ -336,7 +336,7 @@ rewrite (plus_comm n m).
 rewrite (plus_comm n p).
 auto.
 Qed.
-
+*)
 Lemma Th_distr_right : forall n m p:A, n * (m + p) = n * m + n * p.
 intros.
 repeat rewrite (mult_comm n).
@@ -349,7 +349,7 @@ Qed.
 
 End Theory_of_rings.
 
-Hint Resolve Th_mult_zero_left Th_plus_reg_left: core.
+Hint Resolve Th_mult_zero_left (*Th_plus_reg_left*): core.
 
 Unset Implicit Arguments.
 
@@ -373,4 +373,4 @@ End product_ring.
 
 Section power_ring.
 
-End power_ring.
\ No newline at end of file
+End power_ring.
diff --git a/contrib/ring/ZArithRing.v b/contrib/ring/ZArithRing.v
index 9324fb602..075431827 100644
--- a/contrib/ring/ZArithRing.v
+++ b/contrib/ring/ZArithRing.v
@@ -32,5 +32,5 @@ Definition ZTheory : Ring_Theory Zplus Zmult 1%Z 0%Z Zopp Zeq.
 Qed.
 
 (* NatConstants and NatTheory are defined in Ring_theory.v *)
-Add Ring Z Zplus Zmult 1%Z 0%Z Zopp Zeq ZTheory
+Add Legacy Ring Z Zplus Zmult 1%Z 0%Z Zopp Zeq ZTheory
  [ Zpos Zneg 0%Z xO xI 1%positive ].
diff --git a/contrib/ring/g_ring.ml4 b/contrib/ring/g_ring.ml4
index 0cb86dfdd..5ca1bfced 100644
--- a/contrib/ring/g_ring.ml4
+++ b/contrib/ring/g_ring.ml4
@@ -12,9 +12,10 @@
 
 open Quote
 open Ring
+open Tacticals
 
 TACTIC EXTEND ring
-  [ "ring" constr_list(l) ] -> [ polynom l ]
+| [ "legacy" "ring" constr_list(l) ] -> [ polynom l ]
 END
 
 (* The vernac commands "Add Ring" and co *)
@@ -23,7 +24,7 @@ let cset_of_constrarg_list l =
   List.fold_right ConstrSet.add (List.map constr_of l) ConstrSet.empty
 
 VERNAC COMMAND EXTEND AddRing
-  [ "Add" "Ring" 
+  [ "Add" "Legacy" "Ring" 
           constr(a) constr(aplus) constr(amult) constr(aone) constr(azero)
           constr(aopp) constr(aeq) constr(t) "[" ne_constr_list(l) "]" ] 
   -> [ add_theory true false false
@@ -40,7 +41,7 @@ VERNAC COMMAND EXTEND AddRing
 			 (constr_of t)
 			 (cset_of_constrarg_list l) ]
 
-| [ "Add" "Semi" "Ring" 
+| [ "Add" "Legacy" "Semi" "Ring" 
       	  constr(a) constr(aplus) constr(amult) constr(aone) constr(azero)
           constr(aeq) constr(t) "[" ne_constr_list(l) "]" ] 
   -> [ add_theory false false false
@@ -57,7 +58,7 @@ VERNAC COMMAND EXTEND AddRing
 			 (constr_of t)
 			 (cset_of_constrarg_list l) ]
 
-| [ "Add" "Abstract" "Ring" 
+| [ "Add" "Legacy" "Abstract" "Ring" 
     	  constr(a) constr(aplus) constr(amult) constr(aone)
           constr(azero) constr(aopp) constr(aeq) constr(t) ] 
   -> [ add_theory true true false
@@ -74,7 +75,7 @@ VERNAC COMMAND EXTEND AddRing
 			 (constr_of t)
 			 ConstrSet.empty ]
 
-| [ "Add" "Abstract" "Semi" "Ring" 
+| [ "Add" "Legacy" "Abstract" "Semi" "Ring" 
           constr(a) constr(aplus) constr(amult) constr(aone)
           constr(azero) constr(aeq) constr(t) ] 
   -> [ add_theory false true false
@@ -91,7 +92,7 @@ VERNAC COMMAND EXTEND AddRing
 			 (constr_of t)
 			 ConstrSet.empty ]
 
-| [ "Add" "Setoid" "Ring"
+| [ "Add" "Legacy" "Setoid" "Ring"
       	  constr(a) constr(aequiv) constr(asetth) constr(aplus) constr(amult) 
 	  constr(aone) constr(azero) constr(aopp) constr(aeq) constr(pm)
 	  constr(mm) constr(om) constr(t) "[" ne_constr_list(l) "]" ] 
@@ -112,7 +113,7 @@ VERNAC COMMAND EXTEND AddRing
 			 (constr_of t)
 			 (cset_of_constrarg_list l) ]
 
-| [ "Add" "Semi" "Setoid" "Ring" 
+| [ "Add" "Legacy" "Semi" "Setoid" "Ring" 
           constr(a) constr(aequiv) constr(asetth) constr(aplus)
 	  constr(amult) constr(aone) constr(azero) constr(aeq) 
           constr(pm) constr(mm) constr(t) "[" ne_constr_list(l) "]" ] 
diff --git a/contrib/ring/quote.ml b/contrib/ring/quote.ml
index 3b937c7a6..3c1645d47 100644
--- a/contrib/ring/quote.ml
+++ b/contrib/ring/quote.ml
@@ -298,7 +298,7 @@ let rec closed_under cset t =
   (ConstrSet.mem t cset) or
   (match (kind_of_term t) with
      | Cast(c,_,_) -> closed_under cset c  
-     | App(f,l) -> closed_under cset f & array_for_all (closed_under cset) l
+     | App(f,l) -> closed_under cset f && array_for_all (closed_under cset) l
      | _ -> false)
     
 (*s [btree_of_array [| c1; c2; c3; c4; c5 |]] builds the complete
diff --git a/contrib/ring/ring.ml b/contrib/ring/ring.ml
index 48e8763d5..1c5121ef6 100644
--- a/contrib/ring/ring.ml
+++ b/contrib/ring/ring.ml
@@ -885,7 +885,7 @@ let match_with_equiv c = match (kind_of_term c) with
   | _ -> None
 
 let polynom lc gl =
-  Coqlib.check_required_library ["Coq";"ring";"Ring"];
+  Coqlib.check_required_library ["Coq";"ring";"LegacyRing"];
   match lc with 
    (* If no argument is given, try to recognize either an equality or
       a declared relation with arguments c1 ... cn,