nouvel algo de conversion plus uniforme

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

9 files changed, 10 insertions, 3 deletions

diff --git a/contrib/correctness/peffect.ml b/contrib/correctness/peffect.ml
index 23d4dea344..1db31269b9 100644
--- a/contrib/correctness/peffect.ml
+++ b/contrib/correctness/peffect.ml
@@ -11,6 +11,7 @@
 (* $Id$ *)
 
 open Names
+open Nameops
 open Pmisc
 
 (* The type of effects.
diff --git a/contrib/correctness/penv.ml b/contrib/correctness/penv.ml
index feee251ff5..c3cc1ec64a 100644
--- a/contrib/correctness/penv.ml
+++ b/contrib/correctness/penv.ml
@@ -14,6 +14,7 @@ open Pmisc
 open Past
 open Ptype
 open Names
+open Nameops
 open Libobject
 open Library
 open Term
diff --git a/contrib/correctness/perror.ml b/contrib/correctness/perror.ml
index 452e1b5811..17c673a543 100644
--- a/contrib/correctness/perror.ml
+++ b/contrib/correctness/perror.ml
@@ -13,6 +13,7 @@
 open Pp
 open Util
 open Names
+open Nameops
 open Term
 open Himsg
 
diff --git a/contrib/correctness/prename.ml b/contrib/correctness/prename.ml
index 6824632382..122ff16ab5 100644
--- a/contrib/correctness/prename.ml
+++ b/contrib/correctness/prename.ml
@@ -11,6 +11,7 @@
 (* $Id$ *)
 
 open Names
+open Nameops
 open Util
 open Pp
 open Himsg
diff --git a/contrib/correctness/psyntax.ml4 b/contrib/correctness/psyntax.ml4
index 77d2616532..6b487348a8 100644
--- a/contrib/correctness/psyntax.ml4
+++ b/contrib/correctness/psyntax.ml4
@@ -14,6 +14,7 @@
 
 open Options
 open Names
+open Nameops
 open Vernacentries
 open Reduction
 open Term
diff --git a/contrib/correctness/putil.ml b/contrib/correctness/putil.ml
index fecd577d7c..5e454a2520 100644
--- a/contrib/correctness/putil.ml
+++ b/contrib/correctness/putil.ml
@@ -12,6 +12,7 @@
 
 open Util
 open Names
+open Nameops
 open Term
 open Termops
 open Pattern
diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml
index 2fd9979868..77e20c7856 100644
--- a/contrib/extraction/extract_env.ml
+++ b/contrib/extraction/extract_env.ml
@@ -11,6 +11,7 @@
 open Pp
 open Util
 open Names
+open Nameops
 open Term
 open Lib
 open Extraction
diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml
index 9aecdd4c4e..132367de95 100644
--- a/contrib/extraction/extraction.ml
+++ b/contrib/extraction/extraction.ml
@@ -108,7 +108,7 @@ let sort_of env c =
   Retyping.get_sort_family_of env Evd.empty (strip_outer_cast c)
 
 open RedFlags
-let whd_betaiotalet = clos_norm_flags (UNIFORM, mkflags [fBETA;fIOTA;fZETA])
+let whd_betaiotalet = clos_norm_flags (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 1043ecbdb6..97258c5063 100644
--- a/contrib/ring/ring.ml
+++ b/contrib/ring/ring.ml
@@ -815,12 +815,12 @@ let constants_to_unfold =
 open RedFlags
 let polynom_unfold_tac =
   let flags =
-    (UNIFORM, mkflags(fBETA::fIOTA::(List.map fCONST constants_to_unfold))) in
+    (mkflags(fBETA::fIOTA::(List.map fCONST constants_to_unfold))) in
   reduct_in_concl (cbv_norm_flags flags)
       
 let polynom_unfold_tac_in_term gl =
   let flags = 
-    (UNIFORM,mkflags(fBETA::fIOTA::fZETA::(List.map fCONST constants_to_unfold)))
+    (mkflags(fBETA::fIOTA::fZETA::(List.map fCONST constants_to_unfold)))
   in
   cbv_norm_flags flags (pf_env gl) (project gl)