distinguer interp_cs et interp_setcs

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

2 files changed, 55 insertions, 55 deletions

diff --git a/contrib/ring/Setoid_ring_normalize.v b/contrib/ring/Setoid_ring_normalize.v
index 43b1f481e..bbebde422 100644
--- a/contrib/ring/Setoid_ring_normalize.v
+++ b/contrib/ring/Setoid_ring_normalize.v
@@ -329,7 +329,7 @@ Definition ics_aux := Fix ics_aux{ics_aux[a:A; s:canonical_sum] : A :=
   | (Cons_monom c l t) => (Aplus a (ics_aux (interp_m c l) t))
   end}.
 
-Definition interp_cs : canonical_sum -> A  := 
+Definition interp_setcs : canonical_sum -> A  := 
   [s]Cases s of 
   | Nil_monom => Azero
   | (Cons_varlist l t) =>
@@ -437,7 +437,7 @@ Proof.
 Save.
 
 Remark ics_aux_ok : (x:A)(s:canonical_sum)
-  (Aequiv (ics_aux x s) (Aplus x (interp_cs s))).
+  (Aequiv (ics_aux x s) (Aplus x (interp_setcs s))).
 Proof.
  Induction s; Simpl; Intros;Trivial.
 Save.
@@ -455,8 +455,8 @@ Hint interp_m_ok_ := Resolve interp_m_ok.
 (* Hints Resolve ivl_aux_ok ics_aux_ok interp_m_ok. *)
 
 Lemma canonical_sum_merge_ok : (x,y:canonical_sum)
-  (Aequiv (interp_cs (canonical_sum_merge x y))
-  (Aplus (interp_cs x) (interp_cs y))).
+  (Aequiv (interp_setcs (canonical_sum_merge x y))
+  (Aplus (interp_setcs x) (interp_setcs y))).
 Proof.
 Induction x; Simpl.
 Trivial.
@@ -481,15 +481,15 @@ Setoid_replace (Amult (Aplus a a0) (interp_vl v0))
 Setoid_replace (Aplus
                  (Aplus (Amult a (interp_vl v0))
                    (Amult a0 (interp_vl v0)))
-                 (Aplus (interp_cs c) (interp_cs c0)))
+                 (Aplus (interp_setcs c) (interp_setcs c0)))
  with (Aplus (Amult a (interp_vl v0))
         (Aplus (Amult a0 (interp_vl v0))
-          (Aplus (interp_cs c) (interp_cs c0)))).
-Setoid_replace (Aplus (Aplus (Amult a (interp_vl v0)) (interp_cs c))
-                 (Aplus (Amult a0 (interp_vl v0)) (interp_cs c0)))
+          (Aplus (interp_setcs c) (interp_setcs c0)))).
+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_cs c)
-          (Aplus (Amult a0 (interp_vl v0)) (interp_cs c0)))).
+        (Aplus (interp_setcs c)
+          (Aplus (Amult a0 (interp_vl v0)) (interp_setcs c0)))).
 Auto.
 
 Elim (varlist_lt v v0); Simpl.
@@ -550,14 +550,14 @@ Setoid_replace (Amult (Aplus a Aone) (interp_vl v0))
 Setoid_replace (Aplus
                  (Aplus (Amult a (interp_vl v0))
                    (Amult Aone (interp_vl v0)))
-                 (Aplus (interp_cs c) (interp_cs c0)))
+                 (Aplus (interp_setcs c) (interp_setcs c0)))
  with (Aplus (Amult a (interp_vl v0))
         (Aplus (Amult Aone (interp_vl v0))
-          (Aplus (interp_cs c) (interp_cs c0)))).
-Setoid_replace (Aplus (Aplus (Amult a (interp_vl v0)) (interp_cs c))
-                 (Aplus (interp_vl v0) (interp_cs c0)))
+          (Aplus (interp_setcs c) (interp_setcs c0)))).
+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_cs c) (Aplus (interp_vl v0) (interp_cs c0)))).
+        (Aplus (interp_setcs c) (Aplus (interp_vl v0) (interp_setcs c0)))).
 Setoid_replace (Amult Aone (interp_vl v0)) with (interp_vl v0).
 Auto.
 
@@ -623,15 +623,15 @@ Setoid_replace (Amult (Aplus Aone a) (interp_vl v0))
 Setoid_replace (Aplus
                  (Aplus (Amult Aone (interp_vl v0))
                    (Amult a (interp_vl v0)))
-                 (Aplus (interp_cs c) (interp_cs c0)))
+                 (Aplus (interp_setcs c) (interp_setcs c0)))
  with (Aplus (Amult Aone (interp_vl v0))
         (Aplus (Amult a (interp_vl v0))
-          (Aplus (interp_cs c) (interp_cs c0))));
-Setoid_replace (Aplus (Aplus (interp_vl v0) (interp_cs c))
-                 (Aplus (Amult a (interp_vl v0)) (interp_cs c0)))
+          (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_cs c)
-          (Aplus (Amult a (interp_vl v0)) (interp_cs c0)))).
+        (Aplus (interp_setcs c)
+          (Aplus (Amult a (interp_vl v0)) (interp_setcs c0)))).
 Auto.
 
 Elim (varlist_lt v v0); Simpl; Intros.
@@ -687,14 +687,14 @@ Setoid_replace (Amult (Aplus Aone Aone) (interp_vl v0))
 Setoid_replace (Aplus
                  (Aplus (Amult Aone (interp_vl v0))
                    (Amult Aone (interp_vl v0)))
-                 (Aplus (interp_cs c) (interp_cs c0)))
+                 (Aplus (interp_setcs c) (interp_setcs c0)))
  with (Aplus (Amult Aone (interp_vl v0))
         (Aplus (Amult Aone (interp_vl v0))
-          (Aplus (interp_cs c) (interp_cs c0))));
-Setoid_replace (Aplus (Aplus (interp_vl v0) (interp_cs c))
-                 (Aplus (interp_vl v0) (interp_cs c0)))
+          (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_cs c) (Aplus (interp_vl v0) (interp_cs c0)))).
+        (Aplus (interp_setcs c) (Aplus (interp_vl v0) (interp_setcs c0)))).
 Setoid_replace (Amult Aone (interp_vl v0)) with (interp_vl v0); Auto.
 
 Elim (varlist_lt v v0); Simpl.
@@ -738,8 +738,8 @@ Rewrite (ics_aux_ok (interp_vl v0) c0); Simpl; Auto.
 Save.
 
 Lemma monom_insert_ok: (a:A)(l:varlist)(s:canonical_sum)
- (Aequiv (interp_cs (monom_insert a l s)) 
-   (Aplus (Amult a (interp_vl l)) (interp_cs s))).
+ (Aequiv (interp_setcs (monom_insert a l s)) 
+   (Aplus (Amult a (interp_vl l)) (interp_setcs s))).
 Proof.
 Induction s; Intros.
 Simpl; Rewrite (interp_m_ok a l); Trivial.
@@ -782,8 +782,8 @@ Save.
 
 Lemma varlist_insert_ok :
  (l:varlist)(s:canonical_sum)
- (Aequiv (interp_cs (varlist_insert l s)) 
-   (Aplus (interp_vl l) (interp_cs s))).
+ (Aequiv (interp_setcs (varlist_insert l s)) 
+   (Aplus (interp_vl l) (interp_setcs s))).
 Proof.
 Induction s; Simpl; Intros.
 Trivial.
@@ -820,7 +820,7 @@ Rewrite (ics_aux_ok (interp_vl v) c); Auto.
 Save.
 
 Lemma canonical_sum_scalar_ok : (a:A)(s:canonical_sum)
-  (Aequiv (interp_cs (canonical_sum_scalar a s)) (Amult a (interp_cs s))).
+  (Aequiv (interp_setcs (canonical_sum_scalar a s)) (Amult a (interp_setcs s))).
 Proof.
 Induction s; Simpl; Intros.
 Trivial.
@@ -831,8 +831,8 @@ Rewrite (ics_aux_ok (interp_m a0 v) 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_cs c)))
- with (Aplus (Amult a (Amult a0 (interp_vl v))) (Amult a (interp_cs c))).
+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))).
 Auto.
 
 Rewrite (ics_aux_ok (interp_m a v) (canonical_sum_scalar a c));
@@ -842,7 +842,7 @@ Auto.
 Save.
 
 Lemma canonical_sum_scalar2_ok : (l:varlist; s:canonical_sum)
-  (Aequiv (interp_cs (canonical_sum_scalar2 l s)) (Amult (interp_vl l) (interp_cs s))).
+  (Aequiv (interp_setcs (canonical_sum_scalar2 l s)) (Amult (interp_vl l) (interp_setcs s))).
 Proof.
 Induction s; Simpl; Intros; Auto.
 Rewrite (monom_insert_ok a (varlist_merge l v)
@@ -852,9 +852,9 @@ Rewrite (interp_m_ok a v).
 Rewrite H.
 Rewrite (varlist_merge_ok l v).
 Setoid_replace (Amult (interp_vl l)
-                 (Aplus (Amult a (interp_vl v)) (interp_cs c)))
+                 (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_cs c))).
+        (Amult (interp_vl l) (interp_setcs c))).
 Auto.
 
 Rewrite (varlist_insert_ok (varlist_merge l v)
@@ -866,7 +866,7 @@ Auto.
 Save.
 
 Lemma canonical_sum_scalar3_ok : (c:A; l:varlist; s:canonical_sum)
-  (Aequiv (interp_cs (canonical_sum_scalar3 c l s)) (Amult c (Amult (interp_vl l) (interp_cs s)))).
+  (Aequiv (interp_setcs (canonical_sum_scalar3 c l s)) (Amult c (Amult (interp_vl l) (interp_setcs s)))).
 Proof.
 Induction s; Simpl; Intros.
 Rewrite (SSR_mult_zero_right S T (interp_vl l)).
@@ -879,14 +879,14 @@ Rewrite (interp_m_ok a v).
 Rewrite H.
 Rewrite (varlist_merge_ok l v).
 Setoid_replace (Amult (interp_vl l)
-                 (Aplus (Amult a (interp_vl v)) (interp_cs c0)))
+                 (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_cs c0))).
+        (Amult (interp_vl l) (interp_setcs c0))).
 Setoid_replace (Amult c
                  (Aplus (Amult (interp_vl l) (Amult a (interp_vl v)))
-                   (Amult (interp_vl l) (interp_cs c0))))
+                   (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_cs c0)))).
+        (Amult c (Amult (interp_vl l) (interp_setcs c0)))).
 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)))).
 Auto.
@@ -897,15 +897,15 @@ Rewrite (ics_aux_ok (interp_vl v) c0).
 Rewrite H.
 Rewrite (varlist_merge_ok l v).
 Setoid_replace (Aplus (Amult c (Amult (interp_vl l) (interp_vl v)))
-                 (Amult c (Amult (interp_vl l) (interp_cs c0))))
+                 (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_cs c0)))).
+          (Amult (interp_vl l) (interp_setcs c0)))).
 Auto.
 Save.
 
 Lemma canonical_sum_prod_ok : (x,y:canonical_sum)
-  (Aequiv (interp_cs (canonical_sum_prod x y)) (Amult (interp_cs x) (interp_cs y))).
+  (Aequiv (interp_setcs (canonical_sum_prod x y)) (Amult (interp_setcs x) (interp_setcs y))).
 Proof.
 Induction x; Simpl; Intros.
 Trivial.
@@ -916,12 +916,12 @@ Rewrite (canonical_sum_scalar3_ok a v y).
 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_cs y)))
- with (Amult (Amult a (interp_vl v)) (interp_cs y)).
-Setoid_replace (Amult (Aplus (Amult a (interp_vl v)) (interp_cs c))
-                 (interp_cs y))
- with (Aplus (Amult (Amult a (interp_vl v)) (interp_cs y))
-        (Amult (interp_cs c) (interp_cs y))).
+Setoid_replace (Amult a (Amult (interp_vl v) (interp_setcs y)))
+ with (Amult (Amult a (interp_vl v)) (interp_setcs y)).
+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))).
 Trivial.
 
 Rewrite (canonical_sum_merge_ok (canonical_sum_scalar2 v y)
@@ -933,7 +933,7 @@ Trivial.
 Save.
 
 Theorem setspolynomial_normalize_ok : (p:setspolynomial)
-  (Aequiv (interp_cs (setspolynomial_normalize p)) (interp_setsp p)).
+  (Aequiv (interp_setcs (setspolynomial_normalize p)) (interp_setsp p)).
 Proof.
 Induction p; Simpl; Intros; Trivial.
 Rewrite (canonical_sum_merge_ok (setspolynomial_normalize s)
@@ -946,7 +946,7 @@ Rewrite H; Rewrite H0; Trivial.
 Save.
 
 Lemma canonical_sum_simplify_ok : (s:canonical_sum)
-  (Aequiv (interp_cs (canonical_sum_simplify s)) (interp_cs s)).
+  (Aequiv (interp_setcs (canonical_sum_simplify s)) (interp_setcs s)).
 Proof.
 Induction s; Simpl; Intros.
 Trivial.
@@ -986,7 +986,7 @@ Auto.
 Save.
 
 Theorem setspolynomial_simplify_ok : (p:setspolynomial)
-  (Aequiv (interp_cs (setspolynomial_simplify p)) (interp_setsp p)).
+  (Aequiv (interp_setcs (setspolynomial_simplify p)) (interp_setsp p)).
 Proof.
 Intro.
 Unfold setspolynomial_simplify.
@@ -1121,7 +1121,7 @@ Elim (canonical_sum_scalar3 (Aopp Aone) Nil_var
 Save.
 
 Theorem setpolynomial_simplify_ok : (p:setpolynomial)
- (Aequiv (interp_cs vm (setpolynomial_simplify p)) (interp_setp p)).
+ (Aequiv (interp_setcs vm (setpolynomial_simplify p)) (interp_setp p)).
 Intro.
 Unfold setpolynomial_simplify.
 Rewrite (setspolynomial_of_ok p).
diff --git a/contrib/ring/ring.ml b/contrib/ring/ring.ml
index 7a95671b8..ac3274ae7 100644
--- a/contrib/ring/ring.ml
+++ b/contrib/ring/ring.ml
@@ -94,7 +94,7 @@ let coq_SetPconst = lazy (ring_constant "SetPconst")
 let coq_SetPopp = lazy (ring_constant "SetPopp")
 let coq_interp_setsp = lazy (ring_constant "interp_setsp")
 let coq_interp_setp = lazy (ring_constant "interp_setp")
-let coq_interp_setcs = lazy (ring_constant "interp_cs")
+let coq_interp_setcs = lazy (ring_constant "interp_setcs")
 let coq_setspolynomial_simplify = 
   lazy (ring_constant "setspolynomial_simplify")
 let coq_setpolynomial_simplify =