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/ring/ring.ml | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

(limited to 'contrib/ring')

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