réparation Ring (simplifications)

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

2 files changed, 12 insertions, 5 deletions

diff --git a/contrib/ring/Ring_abstract.v b/contrib/ring/Ring_abstract.v
index 762689985..05a6f6850 100644
--- a/contrib/ring/Ring_abstract.v
+++ b/contrib/ring/Ring_abstract.v
@@ -100,7 +100,7 @@ Fixpoint interp_asp [p:aspolynomial] : A :=
   | (ASPmult l r) => (Amult (interp_asp l) (interp_asp r))
   end.
 
-Local iacs_aux := Fix iacs_aux{iacs_aux [a:A; s:abstract_sum] : A :=  
+(* Local *) Definition iacs_aux := Fix iacs_aux{iacs_aux [a:A; s:abstract_sum] : A :=  
   Cases s of
   | Nil_acs => a
   | (Cons_acs l t) => (Aplus a (iacs_aux (interp_vl Amult Aone Azero vm l) t))
@@ -384,7 +384,7 @@ Variable Aeq : A -> A -> bool.
 Variable vm : (varmap A).
 Variable T : (Ring_Theory Aplus Amult Aone Azero Aopp Aeq).
 
-Local isacs_aux := Fix isacs_aux{isacs_aux [a:A; s:signed_sum] : A :=  
+(* Local *) Definition isacs_aux := Fix isacs_aux{isacs_aux [a:A; s:signed_sum] : A :=  
   Cases s of
   | Nil_varlist => a
   | (Plus_varlist l t) => 
diff --git a/contrib/ring/ring.ml b/contrib/ring/ring.ml
index 589c1580e..5c6ec33d5 100644
--- a/contrib/ring/ring.ml
+++ b/contrib/ring/ring.ml
@@ -536,7 +536,14 @@ let constants_to_unfold =
       path_of_string "Coq.ring.Ring_normalize.interp_vl";
       path_of_string "Coq.ring.Ring_abstract.interp_acs";
       path_of_string "Coq.ring.Ring_abstract.interp_sacs";
-      path_of_string "Coq.ring.Quote.varmap_find" ]
+      path_of_string "Coq.ring.Quote.varmap_find";
+      (* anciennement des Local devenus Definition *)
+      path_of_string "Coq.ring.Ring_normalize.ics_aux";
+      path_of_string "Coq.ring.Ring_normalize.ivl_aux";
+      path_of_string "Coq.ring.Ring_normalize.interp_m";
+      path_of_string "Coq.ring.Ring_abstract.iacs_aux";
+      path_of_string "Coq.ring.Ring_abstract.isacs_aux";
+    ]
 (*    SectionPathSet.empty *)
 
 (* Unfolds the functions interp and find_btree in the term c of goal gl *)
@@ -575,10 +582,10 @@ let raw_polynom th op lc gl =
              (tclORELSE
                (h_exact c'i_eq_c''i)
                (h_exact (mkAppA
-                 [| build_coq_sym_eqT (); th.th_a; c'''i; ci; c'i_eq_c''i |]))
+                 [| build_coq_sym_eqT (); th.th_a; c''i; ci; c'i_eq_c''i |]))
              ) 
 	     (tclTHENS 
-	       (elim_type (mkAppA [| build_coq_eqT (); th.th_a; c'''i; ci |]))
+	       (elim_type (mkAppA [| build_coq_eqT (); th.th_a; c''i; ci |]))
                [ tac ;
                  h_exact c'i_eq_c''i
                ]