Imported Upstream version 8.0pl3+8.1alphaupstream/8.0pl3+8.1alpha

15 files changed, 180 insertions, 127 deletions

diff --git a/contrib/ring/ArithRing.v b/contrib/ring/ArithRing.v
index 1a6e0ba6..68464c10 100644
--- a/contrib/ring/ArithRing.v
+++ b/contrib/ring/ArithRing.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: ArithRing.v,v 1.9.2.1 2004/07/16 19:30:13 herbelin Exp $ *)
+(* $Id: ArithRing.v 6295 2004-11-12 16:40:39Z gregoire $ *)
 
 (* Instantiation of the Ring tactic for the naturals of Arith $*)
 
@@ -16,7 +16,7 @@ Require Import Eqdep_dec.
 
 Open Local Scope nat_scope.
 
-Fixpoint nateq (n m:nat) {struct m} : bool :=
+Unboxed Fixpoint nateq (n m:nat) {struct m} : bool :=
   match n, m with
   | O, O => true
   | S n', S m' => nateq n' m'
@@ -32,12 +32,12 @@ Proof.
   trivial.
 Qed.
 
-Hint Resolve nateq_prop eq2eqT: arithring.
+Hint Resolve nateq_prop: arithring.
 
 Definition NatTheory : Semi_Ring_Theory plus mult 1 0 nateq.
   split; intros; auto with arith arithring.
-  apply eq2eqT; apply (fun n m p:nat => plus_reg_l m p n) with (n := n).
-  apply eqT2eq; trivial.
+  apply (fun n m p:nat => plus_reg_l m p n) with (n := n).
+  trivial.
 Defined.
 
 
@@ -86,4 +86,4 @@ Ltac rewrite_S_to_plus :=
        change (t1 = t2) in |- *
   end.
 
-Ltac ring_nat := rewrite_S_to_plus; ring.
\ No newline at end of file
+Ltac ring_nat := rewrite_S_to_plus; ring.
diff --git a/contrib/ring/NArithRing.v b/contrib/ring/NArithRing.v
index cfec29ce..878346ba 100644
--- a/contrib/ring/NArithRing.v
+++ b/contrib/ring/NArithRing.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: NArithRing.v,v 1.5.2.1 2004/07/16 19:30:13 herbelin Exp $ *)
+(* $Id: NArithRing.v 6295 2004-11-12 16:40:39Z gregoire $ *)
 
 (* Instantiation of the Ring tactic for the binary natural numbers *)
 
@@ -15,7 +15,7 @@ Require Export ZArith_base.
 Require Import NArith.
 Require Import Eqdep_dec.
 
-Definition Neq (n m:N) :=
+Unboxed Definition Neq (n m:N) :=
   match (n ?= m)%N with
   | Datatypes.Eq => true
   | _ => false
@@ -41,4 +41,4 @@ Definition NTheory : Semi_Ring_Theory Nplus Nmult 1%N 0%N Neq.
     apply Neq_prop.
 Qed.
 
-Add Semi Ring N Nplus Nmult 1%N 0%N Neq NTheory [ Npos 0%N xO xI 1%positive ].
\ No newline at end of file
+Add Semi Ring N Nplus Nmult 1%N 0%N Neq NTheory [ Npos 0%N xO xI 1%positive ].
diff --git a/contrib/ring/Quote.v b/contrib/ring/Quote.v
index b4ac5745..6f7414a3 100644
--- a/contrib/ring/Quote.v
+++ b/contrib/ring/Quote.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: Quote.v,v 1.7.2.1 2004/07/16 19:30:13 herbelin Exp $ *)
+(* $Id: Quote.v 6295 2004-11-12 16:40:39Z gregoire $ *)
 
 (***********************************************************************
   The "abstract" type index is defined to represent variables.
@@ -26,6 +26,7 @@
 ***********************************************************************)
 
 Set Implicit Arguments.
+Unset Boxed Definitions.
 
 Section variables_map.
 
@@ -81,4 +82,4 @@ Qed.
 
 End variables_map.
 
-Unset Implicit Arguments.
\ No newline at end of file
+Unset Implicit Arguments.
diff --git a/contrib/ring/Ring.v b/contrib/ring/Ring.v
index 81497533..6572e79a 100644
--- a/contrib/ring/Ring.v
+++ b/contrib/ring/Ring.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: Ring.v,v 1.9.2.1 2004/07/16 19:30:13 herbelin Exp $ *)
+(* $Id: Ring.v 5920 2004-07-16 20:01:26Z herbelin $ *)
 
 Require Export Bool.
 Require Export Ring_theory.
diff --git a/contrib/ring/Ring_abstract.v b/contrib/ring/Ring_abstract.v
index de42e8c3..c0818da8 100644
--- a/contrib/ring/Ring_abstract.v
+++ b/contrib/ring/Ring_abstract.v
@@ -6,12 +6,14 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: Ring_abstract.v,v 1.13.2.1 2004/07/16 19:30:13 herbelin Exp $ *)
+(* $Id: Ring_abstract.v 6295 2004-11-12 16:40:39Z gregoire $ *)
 
 Require Import Ring_theory.
 Require Import Quote.
 Require Import Ring_normalize.
 
+Unset Boxed Definitions.
+
 Section abstract_semi_rings.
 
 Inductive aspolynomial : Type :=
@@ -701,4 +703,4 @@ Proof.
     rewrite H; reflexivity.
 Qed.  
 
-End abstract_rings.
\ No newline at end of file
+End abstract_rings.
diff --git a/contrib/ring/Ring_normalize.v b/contrib/ring/Ring_normalize.v
index 8c0fd5fb..7b40328a 100644
--- a/contrib/ring/Ring_normalize.v
+++ b/contrib/ring/Ring_normalize.v
@@ -6,12 +6,13 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: Ring_normalize.v,v 1.16.2.1 2004/07/16 19:30:13 herbelin Exp $ *)
+(* $Id: Ring_normalize.v 6295 2004-11-12 16:40:39Z gregoire $ *)
 
 Require Import Ring_theory.
 Require Import Quote.
 
 Set Implicit Arguments.
+Unset Boxed Definitions.
 
 Lemma index_eq_prop : forall n m:index, Is_true (index_eq n m) -> n = m.
 Proof.
@@ -898,4 +899,4 @@ Infix "*" := Pmult : ring_scope.
 Notation "- x" := (Popp x) : ring_scope.
 Notation "[ x ]" := (Pvar x) (at level 1) : ring_scope.
 
-Delimit Scope ring_scope with ring.
\ No newline at end of file
+Delimit Scope ring_scope with ring.
diff --git a/contrib/ring/Ring_theory.v b/contrib/ring/Ring_theory.v
index dfdfdf66..5536294e 100644
--- a/contrib/ring/Ring_theory.v
+++ b/contrib/ring/Ring_theory.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: Ring_theory.v,v 1.21.2.1 2004/07/16 19:30:13 herbelin Exp $ *)
+(* $Id: Ring_theory.v 5920 2004-07-16 20:01:26Z herbelin $ *)
 
 Require Export Bool.
 
diff --git a/contrib/ring/Setoid_ring.v b/contrib/ring/Setoid_ring.v
index c4537fe3..7bf33b17 100644
--- a/contrib/ring/Setoid_ring.v
+++ b/contrib/ring/Setoid_ring.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: Setoid_ring.v,v 1.4.2.1 2004/07/16 19:30:13 herbelin Exp $ *)
+(* $Id: Setoid_ring.v 5920 2004-07-16 20:01:26Z herbelin $ *)
 
 Require Export Setoid_ring_theory.
 Require Export Quote.
diff --git a/contrib/ring/Setoid_ring_normalize.v b/contrib/ring/Setoid_ring_normalize.v
index 0c9c1e6a..56329ade 100644
--- a/contrib/ring/Setoid_ring_normalize.v
+++ b/contrib/ring/Setoid_ring_normalize.v
@@ -6,13 +6,14 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: Setoid_ring_normalize.v,v 1.11.2.1 2004/07/16 19:30:13 herbelin Exp $ *)
+(* $Id: Setoid_ring_normalize.v 6662 2005-02-02 21:33:14Z sacerdot $ *)
 
 Require Import Setoid_ring_theory.
 Require Import Quote.
 
 Set Implicit Arguments.
-
+Unset Boxed Definitions.
+ 
 Lemma index_eq_prop : forall n m:index, Is_true (index_eq n m) -> n = m.
 Proof.
   simple induction n; simple induction m; simpl in |- *;
@@ -34,24 +35,24 @@ Variable Aeq : A -> A -> bool.
 
 Variable S : Setoid_Theory A Aequiv.
 
-Add Setoid A Aequiv S.
+Add Setoid A Aequiv S as Asetoid.
 
-Variable
-  plus_morph :
-    forall a a0 a1 a2:A,
-      Aequiv a a0 -> Aequiv a1 a2 -> Aequiv (Aplus a a1) (Aplus a0 a2).
-Variable
-  mult_morph :
-    forall a a0 a1 a2:A,
-      Aequiv a a0 -> Aequiv a1 a2 -> Aequiv (Amult a a1) (Amult a0 a2).
+Variable plus_morph :
+ forall a a0:A, Aequiv a a0 ->
+   forall a1 a2:A, Aequiv a1 a2 ->
+     Aequiv (Aplus a a1)  (Aplus a0 a2).
+Variable mult_morph :
+ forall a a0:A, Aequiv a a0 ->
+   forall a1 a2:A, Aequiv a1 a2 ->
+     Aequiv (Amult a a1) (Amult a0 a2).
 Variable opp_morph : forall a a0:A, Aequiv a a0 -> Aequiv (Aopp a) (Aopp a0).
 
 Add Morphism Aplus : Aplus_ext.
-exact plus_morph.
+intros; apply plus_morph; assumption.
 Qed.
 
 Add Morphism Amult : Amult_ext.
-exact mult_morph.
+intros; apply mult_morph; assumption.
 Qed.
 
 Add Morphism Aopp : Aopp_ext.
@@ -488,19 +489,22 @@ rewrite (interp_m_ok (Aplus a a0) v0).
 rewrite (interp_m_ok a v0).
 rewrite (interp_m_ok a0 v0).
 setoid_replace (Amult (Aplus a a0) (interp_vl v0)) with
- (Aplus (Amult a (interp_vl v0)) (Amult a0 (interp_vl v0))).
+ (Aplus (Amult a (interp_vl v0)) (Amult a0 (interp_vl v0)));
+ [ idtac | trivial ].
 setoid_replace
  (Aplus (Aplus (Amult a (interp_vl v0)) (Amult a0 (interp_vl v0)))
     (Aplus (interp_setcs c) (interp_setcs c0))) with
  (Aplus (Amult a (interp_vl v0))
     (Aplus (Amult a0 (interp_vl v0))
-       (Aplus (interp_setcs c) (interp_setcs c0)))).
+       (Aplus (interp_setcs c) (interp_setcs c0))));
+ [ idtac | trivial ].
 setoid_replace
  (Aplus (Aplus (Amult a (interp_vl v0)) (interp_setcs c))
     (Aplus (Amult a0 (interp_vl v0)) (interp_setcs c0))) with
  (Aplus (Amult a (interp_vl v0))
     (Aplus (interp_setcs c)
-       (Aplus (Amult a0 (interp_vl v0)) (interp_setcs c0)))).
+       (Aplus (Amult a0 (interp_vl v0)) (interp_setcs c0))));
+ [ idtac | trivial ].
 auto.
 
 elim (varlist_lt v v0); simpl in |- *.
@@ -550,19 +554,23 @@ rewrite (H c0).
 rewrite (interp_m_ok (Aplus a Aone) v0).
 rewrite (interp_m_ok a v0).
 setoid_replace (Amult (Aplus a Aone) (interp_vl v0)) with
- (Aplus (Amult a (interp_vl v0)) (Amult Aone (interp_vl v0))).
+ (Aplus (Amult a (interp_vl v0)) (Amult Aone (interp_vl v0)));
+ [ idtac | trivial ].
 setoid_replace
  (Aplus (Aplus (Amult a (interp_vl v0)) (Amult Aone (interp_vl v0)))
     (Aplus (interp_setcs c) (interp_setcs c0))) with
  (Aplus (Amult a (interp_vl v0))
     (Aplus (Amult Aone (interp_vl v0))
-       (Aplus (interp_setcs c) (interp_setcs c0)))).
+       (Aplus (interp_setcs c) (interp_setcs c0))));
+ [ idtac | trivial ].
 setoid_replace
  (Aplus (Aplus (Amult a (interp_vl v0)) (interp_setcs c))
     (Aplus (interp_vl v0) (interp_setcs c0))) with
  (Aplus (Amult a (interp_vl v0))
-    (Aplus (interp_setcs c) (Aplus (interp_vl v0) (interp_setcs c0)))).
-setoid_replace (Amult Aone (interp_vl v0)) with (interp_vl v0).
+    (Aplus (interp_setcs c) (Aplus (interp_vl v0) (interp_setcs c0))));
+ [ idtac | trivial ].
+setoid_replace (Amult Aone (interp_vl v0)) with (interp_vl v0);
+ [ idtac | trivial ].
 auto.
 
 elim (varlist_lt v v0); simpl in |- *.
@@ -613,18 +621,21 @@ rewrite (ics_aux_ok (interp_m (Aplus Aone a) v0) (canonical_sum_merge c c0));
 rewrite (interp_m_ok (Aplus Aone a) v0); rewrite (interp_m_ok a v0).
 setoid_replace (Amult (Aplus Aone a) (interp_vl v0)) with
  (Aplus (Amult Aone (interp_vl v0)) (Amult a (interp_vl v0)));
- setoid_replace
-  (Aplus (Aplus (Amult Aone (interp_vl v0)) (Amult a (interp_vl v0)))
-     (Aplus (interp_setcs c) (interp_setcs c0))) with
-  (Aplus (Amult Aone (interp_vl v0))
-     (Aplus (Amult a (interp_vl v0))
-        (Aplus (interp_setcs c) (interp_setcs c0))));
- setoid_replace
-  (Aplus (Aplus (interp_vl v0) (interp_setcs c))
-     (Aplus (Amult a (interp_vl v0)) (interp_setcs c0))) with
-  (Aplus (interp_vl v0)
-     (Aplus (interp_setcs c)
-        (Aplus (Amult a (interp_vl v0)) (interp_setcs c0)))).
+ [ idtac | trivial ].
+setoid_replace
+ (Aplus (Aplus (Amult Aone (interp_vl v0)) (Amult a (interp_vl v0)))
+    (Aplus (interp_setcs c) (interp_setcs c0))) with
+ (Aplus (Amult Aone (interp_vl v0))
+    (Aplus (Amult a (interp_vl v0))
+       (Aplus (interp_setcs c) (interp_setcs c0))));
+ [ idtac | trivial ].
+setoid_replace
+ (Aplus (Aplus (interp_vl v0) (interp_setcs c))
+    (Aplus (Amult a (interp_vl v0)) (interp_setcs c0))) with
+ (Aplus (interp_vl v0)
+    (Aplus (interp_setcs c)
+       (Aplus (Amult a (interp_vl v0)) (interp_setcs c0))));
+ [ idtac | trivial ].
 auto.
 
 elim (varlist_lt v v0); simpl in |- *; intros.
@@ -668,17 +679,20 @@ rewrite
 rewrite (interp_m_ok (Aplus Aone Aone) v0).
 setoid_replace (Amult (Aplus Aone Aone) (interp_vl v0)) with
  (Aplus (Amult Aone (interp_vl v0)) (Amult Aone (interp_vl v0)));
- setoid_replace
-  (Aplus (Aplus (Amult Aone (interp_vl v0)) (Amult Aone (interp_vl v0)))
-     (Aplus (interp_setcs c) (interp_setcs c0))) with
-  (Aplus (Amult Aone (interp_vl v0))
-     (Aplus (Amult Aone (interp_vl v0))
-        (Aplus (interp_setcs c) (interp_setcs c0))));
- setoid_replace
-  (Aplus (Aplus (interp_vl v0) (interp_setcs c))
-     (Aplus (interp_vl v0) (interp_setcs c0))) with
-  (Aplus (interp_vl v0)
-     (Aplus (interp_setcs c) (Aplus (interp_vl v0) (interp_setcs c0)))).
+ [ idtac | trivial ].
+setoid_replace
+ (Aplus (Aplus (Amult Aone (interp_vl v0)) (Amult Aone (interp_vl v0)))
+    (Aplus (interp_setcs c) (interp_setcs c0))) with
+ (Aplus (Amult Aone (interp_vl v0))
+    (Aplus (Amult Aone (interp_vl v0))
+       (Aplus (interp_setcs c) (interp_setcs c0))));
+ [ idtac | trivial ].
+setoid_replace
+ (Aplus (Aplus (interp_vl v0) (interp_setcs c))
+    (Aplus (interp_vl v0) (interp_setcs c0))) with
+ (Aplus (interp_vl v0)
+    (Aplus (interp_setcs c) (Aplus (interp_vl v0) (interp_setcs c0))));
+[ idtac | trivial ].
 setoid_replace (Amult Aone (interp_vl v0)) with (interp_vl v0); auto.
 
 elim (varlist_lt v v0); simpl in |- *.
@@ -727,7 +741,8 @@ rewrite (ics_aux_ok (interp_m (Aplus a a0) v) c);
  rewrite (ics_aux_ok (interp_m a0 v) c).
 rewrite (interp_m_ok (Aplus a a0) v); rewrite (interp_m_ok a0 v).
 setoid_replace (Amult (Aplus a a0) (interp_vl v)) with
- (Aplus (Amult a (interp_vl v)) (Amult a0 (interp_vl v))).
+ (Aplus (Amult a (interp_vl v)) (Amult a0 (interp_vl v)));
+ [ idtac | trivial ].
 auto.
 
 elim (varlist_lt l v); simpl in |- *; intros.
@@ -746,8 +761,10 @@ rewrite (ics_aux_ok (interp_m (Aplus a Aone) v) c);
  rewrite (ics_aux_ok (interp_vl v) c).
 rewrite (interp_m_ok (Aplus a Aone) v).
 setoid_replace (Amult (Aplus a Aone) (interp_vl v)) with
- (Aplus (Amult a (interp_vl v)) (Amult Aone (interp_vl v))).
-setoid_replace (Amult Aone (interp_vl v)) with (interp_vl v).
+ (Aplus (Amult a (interp_vl v)) (Amult Aone (interp_vl v)));
+ [ idtac | trivial ].
+setoid_replace (Amult Aone (interp_vl v)) with (interp_vl v);
+ [ idtac | trivial ].
 auto.
 
 elim (varlist_lt l v); simpl in |- *; intros; auto.
@@ -769,7 +786,8 @@ rewrite (ics_aux_ok (interp_m (Aplus Aone a) v) c);
  rewrite (ics_aux_ok (interp_m a v) c).
 rewrite (interp_m_ok (Aplus Aone a) v); rewrite (interp_m_ok a v).
 setoid_replace (Amult (Aplus Aone a) (interp_vl v)) with
- (Aplus (Amult Aone (interp_vl v)) (Amult a (interp_vl v))).
+ (Aplus (Amult Aone (interp_vl v)) (Amult a (interp_vl v)));
+ [ idtac | trivial ].
 setoid_replace (Amult Aone (interp_vl v)) with (interp_vl v); auto.
 
 elim (varlist_lt l v); simpl in |- *; intros; auto.
@@ -784,7 +802,8 @@ rewrite (ics_aux_ok (interp_m (Aplus Aone Aone) v) c);
  rewrite (ics_aux_ok (interp_vl v) c).
 rewrite (interp_m_ok (Aplus Aone Aone) v).
 setoid_replace (Amult (Aplus Aone Aone) (interp_vl v)) with
- (Aplus (Amult Aone (interp_vl v)) (Amult Aone (interp_vl v))).
+ (Aplus (Amult Aone (interp_vl v)) (Amult Aone (interp_vl v)));
+ [ idtac | trivial ].
 setoid_replace (Amult Aone (interp_vl v)) with (interp_vl v); auto.
 
 elim (varlist_lt l v); simpl in |- *; intros; auto.
@@ -806,7 +825,8 @@ rewrite (ics_aux_ok (interp_m (Amult a a0) v) (canonical_sum_scalar a c));
 rewrite (interp_m_ok (Amult a a0) v); rewrite (interp_m_ok a0 v).
 rewrite H.
 setoid_replace (Amult a (Aplus (Amult a0 (interp_vl v)) (interp_setcs c)))
- with (Aplus (Amult a (Amult a0 (interp_vl v))) (Amult a (interp_setcs c))).
+ with (Aplus (Amult a (Amult a0 (interp_vl v))) (Amult a (interp_setcs c)));
+ [ idtac | trivial ].
 auto.
 
 rewrite (ics_aux_ok (interp_m a v) (canonical_sum_scalar a c));
@@ -829,7 +849,8 @@ rewrite (varlist_merge_ok l v).
 setoid_replace
  (Amult (interp_vl l) (Aplus (Amult a (interp_vl v)) (interp_setcs c))) with
  (Aplus (Amult (interp_vl l) (Amult a (interp_vl v)))
-    (Amult (interp_vl l) (interp_setcs c))).
+    (Amult (interp_vl l) (interp_setcs c)));
+ [ idtac | trivial ].
 auto.
 
 rewrite (varlist_insert_ok (varlist_merge l v) (canonical_sum_scalar2 l c)).
@@ -858,15 +879,18 @@ rewrite (varlist_merge_ok l v).
 setoid_replace
  (Amult (interp_vl l) (Aplus (Amult a (interp_vl v)) (interp_setcs c0))) with
  (Aplus (Amult (interp_vl l) (Amult a (interp_vl v)))
-    (Amult (interp_vl l) (interp_setcs c0))).
+    (Amult (interp_vl l) (interp_setcs c0)));
+ [ idtac | trivial ].
 setoid_replace
  (Amult c
     (Aplus (Amult (interp_vl l) (Amult a (interp_vl v)))
        (Amult (interp_vl l) (interp_setcs c0)))) with
  (Aplus (Amult c (Amult (interp_vl l) (Amult a (interp_vl v))))
-    (Amult c (Amult (interp_vl l) (interp_setcs c0)))).
+    (Amult c (Amult (interp_vl l) (interp_setcs c0))));
+ [ idtac | trivial ].
 setoid_replace (Amult (Amult c a) (Amult (interp_vl l) (interp_vl v))) with
- (Amult c (Amult a (Amult (interp_vl l) (interp_vl v)))).
+ (Amult c (Amult a (Amult (interp_vl l) (interp_vl v))));
+ [ idtac | trivial ].
 auto.
 
 rewrite
@@ -880,7 +904,8 @@ setoid_replace
     (Amult c (Amult (interp_vl l) (interp_setcs c0)))) with
  (Amult c
     (Aplus (Amult (interp_vl l) (interp_vl v))
-       (Amult (interp_vl l) (interp_setcs c0)))).
+       (Amult (interp_vl l) (interp_setcs c0))));
+ [ idtac | trivial ].
 auto.
 Qed.
 
@@ -900,12 +925,14 @@ rewrite (ics_aux_ok (interp_m a v) c).
 rewrite (interp_m_ok a v).
 rewrite (H y).
 setoid_replace (Amult a (Amult (interp_vl v) (interp_setcs y))) with
- (Amult (Amult a (interp_vl v)) (interp_setcs y)).
+ (Amult (Amult a (interp_vl v)) (interp_setcs y));
+ [ idtac | trivial ].
 setoid_replace
  (Amult (Aplus (Amult a (interp_vl v)) (interp_setcs c)) (interp_setcs y))
  with
  (Aplus (Amult (Amult a (interp_vl v)) (interp_setcs y))
-    (Amult (interp_setcs c) (interp_setcs y))).
+    (Amult (interp_setcs c) (interp_setcs y)));
+ [ idtac | trivial ].
 trivial.
 
 rewrite
@@ -947,7 +974,8 @@ intros.
 rewrite (ics_aux_ok (interp_m a v) c).
 rewrite (interp_m_ok a v).
 rewrite (H0 I).
-setoid_replace (Amult Azero (interp_vl v)) with Azero.
+setoid_replace (Amult Azero (interp_vl v)) with Azero;
+ [ idtac | trivial ].
 rewrite H.
 trivial.
 
@@ -1134,4 +1162,4 @@ Qed.
 
 End setoid_rings.
 
-End setoid.
\ No newline at end of file
+End setoid.
diff --git a/contrib/ring/Setoid_ring_theory.v b/contrib/ring/Setoid_ring_theory.v
index 69712216..ae6610d3 100644
--- a/contrib/ring/Setoid_ring_theory.v
+++ b/contrib/ring/Setoid_ring_theory.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: Setoid_ring_theory.v,v 1.16.2.1 2004/07/16 19:30:13 herbelin Exp $ *)
+(* $Id: Setoid_ring_theory.v 6662 2005-02-02 21:33:14Z sacerdot $ *)
 
 Require Export Bool.
 Require Export Setoid.
@@ -22,7 +22,7 @@ Infix Local "==" := Aequiv (at level 70, no associativity).
 
 Variable S : Setoid_Theory A Aequiv.
 
-Add Setoid A Aequiv S.
+Add Setoid A Aequiv S as Asetoid.
 
 Variable Aplus : A -> A -> A.
 Variable Amult : A -> A -> A.
@@ -37,18 +37,18 @@ Notation "0" := Azero.
 Notation "1" := Aone.
 Notation "- x" := (Aopp x).
 
-Variable
-  plus_morph : forall a a0 a1 a2:A, a == a0 -> a1 == a2 -> a + a1 == a0 + a2.
-Variable
-  mult_morph : forall a a0 a1 a2:A, a == a0 -> a1 == a2 -> a * a1 == a0 * a2.
+Variable plus_morph :
+ forall a a0:A, a == a0 -> forall a1 a2:A, a1 == a2 -> a + a1 == a0 + a2.
+Variable mult_morph :
+  forall a a0:A, a == a0 -> forall a1 a2:A, a1 == a2 -> a * a1 == a0 * a2.
 Variable opp_morph : forall a a0:A, a == a0 -> - a == - a0.
 
 Add Morphism Aplus : Aplus_ext.
-exact plus_morph.
+intros; apply plus_morph; assumption.
 Qed.
 
 Add Morphism Amult : Amult_ext.
-exact mult_morph.
+intros; apply mult_morph; assumption.
 Qed.
 
 Add Morphism Aopp : Aopp_ext.
@@ -424,4 +424,4 @@ Section power_ring.
 
 End power_ring.
 
-End Setoid_rings.
\ No newline at end of file
+End Setoid_rings.
diff --git a/contrib/ring/ZArithRing.v b/contrib/ring/ZArithRing.v
index c511c076..3999b632 100644
--- a/contrib/ring/ZArithRing.v
+++ b/contrib/ring/ZArithRing.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: ZArithRing.v,v 1.5.2.1 2004/07/16 19:30:13 herbelin Exp $ *)
+(* $Id: ZArithRing.v 6295 2004-11-12 16:40:39Z gregoire $ *)
 
 (* Instantiation of the Ring tactic for the binary integers of ZArith *)
 
@@ -14,7 +14,7 @@ Require Export ArithRing.
 Require Export ZArith_base.
 Require Import Eqdep_dec.
 
-Definition Zeq (x y:Z) :=
+Unboxed Definition Zeq (x y:Z) :=
   match (x ?= y)%Z with
   | Datatypes.Eq => true
   | _ => false
@@ -27,10 +27,10 @@ Lemma Zeq_prop : forall x y:Z, Is_true (Zeq x y) -> x = y.
 Qed.
 
 Definition ZTheory : Ring_Theory Zplus Zmult 1%Z 0%Z Zopp Zeq.
-  split; intros; apply eq2eqT; eauto with zarith.
-  apply eqT2eq; apply Zeq_prop; assumption.
+  split; intros; eauto with zarith.
+  apply Zeq_prop; assumption.
 Qed.
 
 (* NatConstants and NatTheory are defined in Ring_theory.v *)
 Add Ring Z Zplus Zmult 1%Z 0%Z Zopp Zeq ZTheory
- [ Zpos Zneg 0%Z xO xI 1%positive ].
\ No newline at end of file
+ [ Zpos Zneg 0%Z xO xI 1%positive ].
diff --git a/contrib/ring/g_quote.ml4 b/contrib/ring/g_quote.ml4
index af23a8f7..d0058026 100644
--- a/contrib/ring/g_quote.ml4
+++ b/contrib/ring/g_quote.ml4
@@ -8,11 +8,11 @@
 
 (*i camlp4deps: "parsing/grammar.cma" i*)
 
-(* $Id: g_quote.ml4,v 1.1.12.1 2004/07/16 19:30:13 herbelin Exp $ *)
+(* $Id: g_quote.ml4 7734 2005-12-26 14:06:51Z herbelin $ *)
 
 open Quote
 
-TACTIC EXTEND Quote
-  [ "Quote" ident(f) ] -> [ quote f [] ]
-| [ "Quote" ident(f) "[" ne_ident_list(lc) "]"] -> [ quote f lc ]
+TACTIC EXTEND quote
+  [ "quote" ident(f) ] -> [ quote f [] ]
+| [ "quote" ident(f) "[" ne_ident_list(lc) "]"] -> [ quote f lc ]
 END
diff --git a/contrib/ring/g_ring.ml4 b/contrib/ring/g_ring.ml4
index f7c74c0b..dccd1944 100644
--- a/contrib/ring/g_ring.ml4
+++ b/contrib/ring/g_ring.ml4
@@ -8,13 +8,13 @@
 
 (*i camlp4deps: "parsing/grammar.cma" i*)
 
-(* $Id: g_ring.ml4,v 1.4.2.1 2004/07/16 19:30:13 herbelin Exp $ *)
+(* $Id: g_ring.ml4 7734 2005-12-26 14:06:51Z herbelin $ *)
 
 open Quote
 open Ring
 
-TACTIC EXTEND Ring
-  [ "Ring" constr_list(l) ] -> [ polynom l ]
+TACTIC EXTEND ring
+  [ "ring" constr_list(l) ] -> [ polynom l ]
 END
 
 (* The vernac commands "Add Ring" and co *)
diff --git a/contrib/ring/quote.ml b/contrib/ring/quote.ml
index bda04db3..462e5ed8 100644
--- a/contrib/ring/quote.ml
+++ b/contrib/ring/quote.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: quote.ml,v 1.30.2.1 2004/07/16 19:30:14 herbelin Exp $ *)
+(* $Id: quote.ml 7639 2005-12-02 10:01:15Z gregoire $ *)
 
 (* The `Quote' tactic *)
 
@@ -107,7 +107,6 @@ open Pp
 open Util
 open Names
 open Term
-open Instantiate
 open Pattern
 open Matching
 open Tacmach
@@ -213,7 +212,7 @@ let compute_rhs bodyi index_of_f =
 	  PMeta (Some (coerce_meta_in i))
       | App (f,args) ->
           PApp (pattern_of_constr f, Array.map aux args)
-      | Cast (c,t) -> aux c 
+      | Cast (c,_,_) -> aux c 
       | _ -> pattern_of_constr c
   in
   aux bodyi
@@ -298,7 +297,7 @@ binary search trees (see file \texttt{Quote.v}) *)
 let rec closed_under cset t =
   (ConstrSet.mem t cset) or
   (match (kind_of_term t) with
-     | Cast(c,_) -> closed_under cset c  
+     | Cast(c,_,_) -> closed_under cset c  
      | App(f,l) -> closed_under cset f & array_for_all (closed_under cset) l
      | _ -> false)
     
@@ -361,7 +360,7 @@ let rec subterm gl (t : constr) (t' : constr) =
   (pf_conv_x gl t t') or
   (match (kind_of_term t) with 
      | App (f,args) -> array_exists (fun t -> subterm gl t t') args
-     | Cast(t,_) -> (subterm gl t t')
+     | Cast(t,_,_) -> (subterm gl t t')
      | _ -> false)
            
 (*s We want to sort the list according to reverse subterm order. *)
@@ -386,7 +385,7 @@ let rec sort_subterm gl l =
   [gl: goal sigma]\\ *)
 
 let quote_terms ivs lc gl =
-  Library.check_required_library ["Coq";"ring";"Quote"];
+  Coqlib.check_required_library ["Coq";"ring";"Quote"];
   let varhash  = (Hashtbl.create 17 : (constr, constr) Hashtbl.t) in
   let varlist = ref ([] : constr list) in (* list of variables *)
   let counter = ref 1 in (* number of variables created + 1 *)
@@ -448,8 +447,8 @@ let quote f lid gl =
     | _ -> assert false
   in
   match ivs.variable_lhs with
-    | None -> Tactics.convert_concl (mkApp (f, [| p |])) gl
-    | Some _ -> Tactics.convert_concl (mkApp (f, [| vm; p |])) gl
+    | None -> Tactics.convert_concl (mkApp (f, [| p |])) DEFAULTcast gl
+    | Some _ -> Tactics.convert_concl (mkApp (f, [| vm; p |])) DEFAULTcast gl
 
 (*i 
 
diff --git a/contrib/ring/ring.ml b/contrib/ring/ring.ml
index 378f19a4..5251dcc5 100644
--- a/contrib/ring/ring.ml
+++ b/contrib/ring/ring.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: ring.ml,v 1.49.2.1 2004/07/16 19:30:14 herbelin Exp $ *)
+(* $Id: ring.ml 7837 2006-01-11 09:47:32Z herbelin $ *)
 
 (* ML part of the Ring tactic *)
 
@@ -34,6 +34,7 @@ open Pattern
 open Hiddentac
 open Nametab
 open Quote
+open Mod_subst
 
 let mt_evd = Evd.empty
 let constr_of c = Constrintern.interp_constr mt_evd (Global.env()) c
@@ -286,7 +287,7 @@ let guess_theory a =
   with Not_found -> 
     errorlabstrm "Ring" 
       (str "No Declared Ring Theory for " ++
-	 prterm a ++ fnl () ++
+	 pr_lconstr a ++ fnl () ++
 	 str "Use Add [Semi] Ring to declare it")
 
 (* Looks up an option *)
@@ -306,23 +307,42 @@ let safe_pf_conv_x gl c1 c2 = try pf_conv_x gl c1 c2 with _ -> false
 let implement_theory env t th args =
   is_conv env Evd.empty (Typing.type_of env Evd.empty t) (mkLApp (th, args))
 
+(* The following test checks whether the provided morphism is the default
+   one for the given operation. In principle the test is too strict, since
+   it should possible to provide another proof for the same fact (proof
+   irrelevance). In particular, the error message is be not very explicative. *)
+let states_compatibility_for env plus mult opp morphs =
+ let check op compat =
+  is_conv env Evd.empty (Setoid_replace.default_morphism op).Setoid_replace.lem
+   compat in
+ check plus morphs.plusm &&
+ check mult morphs.multm &&
+ (match (opp,morphs.oppm) with
+     None, None -> true
+   | Some opp, Some compat -> check opp compat
+   | _,_ -> assert false)
+
 let add_theory want_ring want_abstract want_setoid a aequiv asetth amorph aplus amult aone azero aopp aeq t cset = 
   if theories_map_mem a then errorlabstrm "Add Semi Ring" 
     (str "A (Semi-)(Setoid-)Ring Structure is already declared for " ++
-       prterm a);
+       pr_lconstr a);
   let env = Global.env () in
-    if (want_ring & want_setoid &
+    if (want_ring & want_setoid & (
 	not (implement_theory env t coq_Setoid_Ring_Theory
 	  [| a; (unbox aequiv); aplus; amult; aone; azero; (unbox aopp); aeq|])
-        &
+        ||
 	not (implement_theory env (unbox asetth) coq_Setoid_Theory
-	  [| a; (unbox aequiv) |])) then 
+	  [| a; (unbox aequiv) |]) ||
+        not (states_compatibility_for env aplus amult aopp (unbox amorph))
+        )) then 
       errorlabstrm "addring" (str "Not a valid Setoid-Ring theory");
-    if (not want_ring & want_setoid &
+    if (not want_ring & want_setoid & (
         not (implement_theory env t coq_Semi_Setoid_Ring_Theory 
-	  [| a; (unbox aequiv); aplus; amult; aone; azero; aeq|]) &
+	  [| a; (unbox aequiv); aplus; amult; aone; azero; aeq|]) ||
 	not (implement_theory env (unbox asetth) coq_Setoid_Theory
-	  [| a; (unbox aequiv) |])) then 
+	  [| a; (unbox aequiv) |]) ||
+        not (states_compatibility_for env aplus amult aopp (unbox amorph))))
+    then
       errorlabstrm "addring" (str "Not a valid Semi-Setoid-Ring theory");
     if (want_ring & not want_setoid &
 	not (implement_theory env t coq_Ring_Theory
@@ -705,10 +725,10 @@ let build_setspolynom gl th lc =
 			       th.th_eq; p |])) |]),
 	mkLApp(coq_setspolynomial_simplify_ok,
 	       [| th.th_a; (unbox th.th_equiv); th.th_plus;
-                  th.th_mult; th.th_one; th.th_zero; th.th_eq; v;
-                  th.th_t; (unbox th.th_setoid_th);
+                  th.th_mult; th.th_one; th.th_zero; th.th_eq;
+                  (unbox th.th_setoid_th);
 		  (unbox th.th_morph).plusm;
-                  (unbox th.th_morph).multm; p |])))
+                  (unbox th.th_morph).multm; v; th.th_t; p |])))
     lp
 
 module SectionPathSet =
@@ -724,7 +744,7 @@ let constants_to_unfold =
   let transform s = 
     let sp = path_of_string s in
     let dir, id = repr_path sp in
-      Libnames.encode_kn dir id 
+      Libnames.encode_con dir id 
   in
   List.map transform
     [ "Coq.ring.Ring_normalize.interp_cs";
@@ -753,7 +773,7 @@ open RedFlags
 let polynom_unfold_tac =
   let flags =
     (mkflags(fBETA::fIOTA::(List.map fCONST constants_to_unfold))) in
-  reduct_in_concl (cbv_norm_flags flags)
+  reduct_in_concl (cbv_norm_flags flags,DEFAULTcast)
       
 let polynom_unfold_tac_in_term gl =
   let flags = 
@@ -804,20 +824,22 @@ let raw_polynom th op lc gl =
 				  [| th.th_a; (unbox th.th_equiv);
                                      (unbox th.th_setoid_th);
 				     c'''i; ci; c'i_eq_c''i |]))))
-	      (tclTHEN 
-		 (Setoid_replace.setoid_replace ci c'''i None)
-		 (tclTHEN 
-		    (tclTRY (h_exact c'i_eq_c''i))
-		    tac)))
+	      (tclTHENS
+		 (tclORELSE
+                   (Setoid_replace.general_s_rewrite true c'i_eq_c''i
+                     ~new_goals:[])
+                   (Setoid_replace.general_s_rewrite false c'i_eq_c''i
+                     ~new_goals:[]))
+                 [tac]))
 	 else
            (tclORELSE
               (tclORELSE
 		 (h_exact c'i_eq_c''i)
-		 (h_exact (mkApp(build_coq_sym_eqT (),
+		 (h_exact (mkApp(build_coq_sym_eq (),
 				 [|th.th_a; c'''i; ci; c'i_eq_c''i |]))))
 	      (tclTHENS 
 		 (elim_type 
-		    (mkApp(build_coq_eqT (), [|th.th_a; c'''i; ci |])))
+		    (mkApp(build_coq_eq (), [|th.th_a; c'''i; ci |])))
 		 [ tac;
                    h_exact c'i_eq_c''i ]))
 )
@@ -863,7 +885,7 @@ let match_with_equiv c = match (kind_of_term c) with
   | _ -> None
 
 let polynom lc gl =
-  Library.check_required_library ["Coq";"ring";"Ring"];
+  Coqlib.check_required_library ["Coq";"ring";"Ring"];
   match lc with 
    (* If no argument is given, try to recognize either an equality or
       a declared relation with arguments c1 ... cn,