Abstraction de constr

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

2 files changed, 14 insertions, 16 deletions

diff --git a/contrib/ring/quote.ml b/contrib/ring/quote.ml
index 633be8d914..f16b6049ed 100644
--- a/contrib/ring/quote.ml
+++ b/contrib/ring/quote.ml
@@ -198,7 +198,7 @@ let compute_lhs typ i nargsi =
 let compute_rhs bodyi index_of_f =
   let rec aux c = 
     match decomp_term c with
-      | IsAppL (Rel j, args) when j = index_of_f (* recursive call *) -> 
+      | IsAppL (j, args) when j = mkRel (index_of_f) (* recursive call *) -> 
           let i = destRel (array_last args) in mkMeta i
       | IsAppL (f,args) ->
           mkAppL (f, Array.map aux args)
@@ -209,8 +209,9 @@ let compute_rhs bodyi index_of_f =
 
 (*s Now the function [compute_ivs] itself *)
 
-let compute_ivs gl f cs = 
-  let body = constant_value (Global.env()) f in
+let compute_ivs gl f cs =
+  let cst = try destConst f with _ -> i_can't_do_that () in
+  let body = constant_value (Global.env()) cst in
   match decomp_term body with
     | IsFix(([| len |], 0), ([| typ |], [ name ], [| body2 |])) ->
         let (args3, body3) = decompose_lam body2 in
@@ -233,8 +234,9 @@ let compute_ivs gl f cs =
                                       i nargsi)
            (* Then we test if the RHS is the RHS for variables *)
                    else begin match decomp_app bodyi with 
-                     | vmf, [_; _; Rel ri; Rel rj]
-                         when pf_conv_x gl vmf 
+                     | vmf, [_; _; a3; a4 ]
+                         when isRel a3 & isRel a4 &
+			   pf_conv_x gl vmf 
                            (Lazy.force coq_varmap_find)->
                              v_lhs := Some (compute_lhs 
                                               (snd (List.hd args3))
diff --git a/contrib/ring/ring.ml b/contrib/ring/ring.ml
index b628956af7..f5a8746b97 100644
--- a/contrib/ring/ring.ml
+++ b/contrib/ring/ring.ml
@@ -15,7 +15,8 @@ open Printer
 open Equality
 open Vernacinterp
 open Libobject
-open Closure 
+open Closure
+open Tacred
 open Tactics
 open Pattern 
 open Hiddentac
@@ -518,26 +519,21 @@ module SectionPathSet =
 	     let compare = Pervasives.compare
 	   end)
 
+(* Avec l'uniformisation des red_kind, on perd ici sur la structure
+   SectionPathSet; peut-être faudra-t-il la déplacer dans Closure *)
 let constants_to_unfold = 
-  List.fold_right SectionPathSet.add 
+(*  List.fold_right SectionPathSet.add *)
     [ path_of_string "#Ring_normalize#interp_cs.cci";
       path_of_string "#Ring_normalize#interp_var.cci";
       path_of_string "#Ring_normalize#interp_vl.cci";
       path_of_string "#Ring_abstract#interp_acs.cci";
       path_of_string "#Ring_abstract#interp_sacs.cci";
       path_of_string "#Quote#varmap_find.cci" ]
-    SectionPathSet.empty 
+(*    SectionPathSet.empty *)
 
 (* Unfolds the functions interp and find_btree in the term c of goal gl *)
 let polynom_unfold_tac =
-  let flags = 
-    (UNIFORM,
-     { r_beta = true;
-       r_delta = (function
-                    | Const sp -> SectionPathSet.mem sp constants_to_unfold
-                    | _ -> false);
-       r_iota = true })
-  in
+  let flags = (UNIFORM, red_add betaiota_red (CONST constants_to_unfold)) in
   reduct_in_concl (cbv_norm_flags flags)
       
 (* lc : constr list *)