Abstraction de constr

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

3 files changed, 19 insertions, 21 deletions

diff --git a/contrib/omega/coq_omega.ml b/contrib/omega/coq_omega.ml
index 9b770512a0..678bdd8b39 100644
--- a/contrib/omega/coq_omega.ml
+++ b/contrib/omega/coq_omega.ml
@@ -489,8 +489,8 @@ let occurence path (t : constr) =
   loop path t
 
 let abstract_path typ path t =
-  let term_occur = ref (Rel 0) in
-  let abstract = context (fun i t -> term_occur:= t; Rel i) path t in
+  let term_occur = ref (mkRel 0) in
+  let abstract = context (fun i t -> term_occur:= t; mkRel i) path t in
   mkLambda (Name (id_of_string "x"), typ, abstract), !term_occur
 
 let focused_simpl path gl =
@@ -565,9 +565,9 @@ let clever_rewrite_base_poly typ p result theorem gl =
 	  mkArrow typ mkProp,
           mkLambda
 	    (Name (id_of_string "H"),
-	     applist (Rel 1,[result]),
+	     applist (mkRel 1,[result]),
 	     mkAppL (Lazy.force coq_eq_ind_r, 
-		       [| typ; result; Rel 2; Rel 1; occ; theorem |]))),
+		       [| typ; result; mkRel 2; mkRel 1; occ; theorem |]))),
        [abstracted]) 
   in
   exact (applist(t,[mkNewMeta()])) gl
@@ -1214,7 +1214,7 @@ let replay_history tactic_normalisation =
 		      mkLambda
 			(Name(id_of_string v),
 			 Lazy.force coq_Z,
-			 mk_eq (Rel 1) eq1) |])
+			 mk_eq (mkRel 1) eq1) |])
 	  in
 	  let mm = mk_integer m in
 	  let p_initial = [P_APP 2;P_TYPE] in
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 *)