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 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'contrib/extraction')

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
 
-- 
cgit v1.2.3