From 9df7ef3bdd8288cb06888b7390441eae8d2c7aba Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 2 Jul 2001 22:31:43 +0000
Subject: Nettoyage/restructuration des ensembles d'indicateurs de réductions

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1819 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/extraction/extraction.ml | 3 ++-
 contrib/ring/ring.ml             | 6 ++++--
 2 files changed, 6 insertions(+), 3 deletions(-)

(limited to 'contrib')

diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml
index 2b0f93b0e3..0000b26a18 100644
--- a/contrib/extraction/extraction.ml
+++ b/contrib/extraction/extraction.ml
@@ -101,7 +101,8 @@ let none = Evd.empty
 
 let type_of env c = Typing.type_of env Evd.empty (strip_outer_cast c)
 
-let whd_betaiotalet = clos_norm_flags (UNIFORM, red_add betaiota_red ZETA)
+open RedFlags
+let whd_betaiotalet = clos_norm_flags (UNIFORM, mkflags [fBETA;fIOTA;fZETA])
 
 let is_axiom sp = (Global.lookup_constant sp).const_body = None
 
diff --git a/contrib/ring/ring.ml b/contrib/ring/ring.ml
index a326a7a18c..0a70426ea5 100644
--- a/contrib/ring/ring.ml
+++ b/contrib/ring/ring.ml
@@ -548,13 +548,15 @@ let constants_to_unfold =
 (*    SectionPathSet.empty *)
 
 (* Unfolds the functions interp and find_btree in the term c of goal gl *)
+open RedFlags
 let polynom_unfold_tac =
-  let flags = (UNIFORM, red_add betaiota_red (CONST constants_to_unfold)) in
+  let flags =
+    (UNIFORM, mkflags(fBETA::fIOTA::fEVAR::(List.map fCONST constants_to_unfold))) in
   reduct_in_concl (cbv_norm_flags flags)
       
 let polynom_unfold_tac_in_term gl =
   let flags = 
-    (UNIFORM, red_add betaiotazeta_red (CONST constants_to_unfold)) 
+    (UNIFORM,mkflags(fBETA::fIOTA::fEVAR::fZETA::(List.map fCONST constants_to_unfold)))
   in
   cbv_norm_flags flags (pf_env gl) (project gl)
 
-- 
cgit v1.2.3