Partial revert of Yann commit in order to use CLib.List when opening

Util module.

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

41 files changed, 42 insertions, 0 deletions

diff --git a/interp/modintern.ml b/interp/modintern.ml
index ba5c68a5d9..0f386ec04b 100644
--- a/interp/modintern.ml
+++ b/interp/modintern.ml
@@ -7,6 +7,7 @@
 (************************************************************************)
 
 open Errors
+open Util
 open Names
 open Entries
 open Libnames
diff --git a/interp/smartlocate.ml b/interp/smartlocate.ml
index adf611b563..b38177d48b 100644
--- a/interp/smartlocate.ml
+++ b/interp/smartlocate.ml
@@ -14,6 +14,7 @@
 (* *)
 open Pp
 open Errors
+open Util
 open Libnames
 open Globnames
 open Misctypes
diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml
index 8307783074..202a3d7704 100644
--- a/interp/syntax_def.ml
+++ b/interp/syntax_def.ml
@@ -7,6 +7,7 @@
 (************************************************************************)
 
 open Errors
+open Util
 open Pp
 open Names
 open Libnames
diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index 098da5184a..9e695e3d3d 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/cbytegen.ml
@@ -10,6 +10,7 @@
    machine, Oct 2004 *)
 (* Extension: Arnaud Spiwack (support for native arithmetic), May 2005 *)
 
+open Util
 open Names
 open Cbytecodes
 open Cemitcodes
diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index a015cdf927..f016a20b76 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -14,6 +14,7 @@
    declarations over global constants and inductive types *)
 
 open Errors
+open Util
 open Names
 open Term
 open Sign
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index d9f3c3bf0a..b2312d689a 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -13,6 +13,7 @@
    declarations *)
 
 open Errors
+open Util
 open Names
 open Univ
 open Declarations
diff --git a/kernel/modops.ml b/kernel/modops.ml
index 19075058a6..2f7d480afb 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -16,6 +16,7 @@
 (* This file provides with various operations on modules and module types *)
 
 open Errors
+open Util
 open Names
 open Term
 open Declarations
diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml
index 476a92bedc..ffa1d304e0 100644
--- a/kernel/pre_env.ml
+++ b/kernel/pre_env.ml
@@ -13,6 +13,7 @@
 
 (* This file defines the type of kernel environments *)
 
+open Util
 open Names
 open Sign
 open Univ
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 11d647d9aa..143b22c34c 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -58,6 +58,7 @@
 *)
 
 open Errors
+open Util
 open Names
 open Univ
 open Declarations
diff --git a/lib/dyn.ml b/lib/dyn.ml
index de5158b141..13d1ec0608 100644
--- a/lib/dyn.ml
+++ b/lib/dyn.ml
@@ -7,6 +7,7 @@
 (************************************************************************)
 
 open Errors
+open Util
 
 (* Dynamics, programmed with DANGER !!! *)
 
diff --git a/library/assumptions.ml b/library/assumptions.ml
index 2d4b6169d1..d721311e06 100644
--- a/library/assumptions.ml
+++ b/library/assumptions.ml
@@ -15,6 +15,7 @@
    Module-traversing code: Pierre Letouzey *)
 
 open Errors
+open Util
 open Names
 open Term
 open Declarations
diff --git a/library/dischargedhypsmap.ml b/library/dischargedhypsmap.ml
index c26f652dfa..9dbbc947df 100644
--- a/library/dischargedhypsmap.ml
+++ b/library/dischargedhypsmap.ml
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Util
 open Libnames
 
 type discharged_hyps = full_path list
diff --git a/library/global.ml b/library/global.ml
index c2bd551284..2d958f799f 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Util
 open Names
 open Term
 open Environ
diff --git a/library/globnames.ml b/library/globnames.ml
index 8d298bc949..27683278bb 100644
--- a/library/globnames.ml
+++ b/library/globnames.ml
@@ -7,6 +7,7 @@
 (************************************************************************)
 
 open Errors
+open Util
 open Names
 open Term
 open Mod_subst
diff --git a/library/goptions.ml b/library/goptions.ml
index 861109d3db..a78ca750da 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -10,6 +10,7 @@
 
 open Pp
 open Errors
+open Util
 open Libobject
 open Libnames
 open Mod_subst
diff --git a/library/libobject.ml b/library/libobject.ml
index ffd87ce806..18b4c0c654 100644
--- a/library/libobject.ml
+++ b/library/libobject.ml
@@ -7,6 +7,7 @@
 (************************************************************************)
 
 open Errors
+open Util
 open Libnames
 open Mod_subst
 
diff --git a/library/nametab.ml b/library/nametab.ml
index 9c2b9b53d7..41017c289a 100644
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -7,6 +7,7 @@
 (************************************************************************)
 
 open Errors
+open Util
 open Pp
 open Names
 open Libnames
diff --git a/parsing/extrawit.ml b/parsing/extrawit.ml
index e7d9ba4b2f..75205c9644 100644
--- a/parsing/extrawit.ml
+++ b/parsing/extrawit.ml
@@ -7,6 +7,7 @@
 (************************************************************************)
 
 open Errors
+open Util
 open Genarg
 
 (* This file defines extra argument types *)
diff --git a/plugins/cc/ccproof.ml b/plugins/cc/ccproof.ml
index 25c01f2bd3..d5eab32c4f 100644
--- a/plugins/cc/ccproof.ml
+++ b/plugins/cc/ccproof.ml
@@ -10,6 +10,7 @@
 (* proof-trees that will be transformed into proof-terms in cctac.ml4   *)
 
 open Errors
+open Util
 open Names
 open Term
 open Ccalgo
diff --git a/plugins/decl_mode/ppdecl_proof.ml b/plugins/decl_mode/ppdecl_proof.ml
index 01f32e4a32..b72476a756 100644
--- a/plugins/decl_mode/ppdecl_proof.ml
+++ b/plugins/decl_mode/ppdecl_proof.ml
@@ -7,6 +7,7 @@
 (************************************************************************)
 
 open Errors
+open Util
 open Pp
 open Decl_expr
 open Names
diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml
index 44ae420904..f678b898ba 100644
--- a/plugins/funind/glob_termops.ml
+++ b/plugins/funind/glob_termops.ml
@@ -1,6 +1,7 @@
 open Pp
 open Glob_term
 open Errors
+open Util
 open Names
 open Decl_kinds
 open Misctypes
diff --git a/plugins/syntax/nat_syntax.ml b/plugins/syntax/nat_syntax.ml
index 8f34ec495f..5219124cd0 100644
--- a/plugins/syntax/nat_syntax.ml
+++ b/plugins/syntax/nat_syntax.ml
@@ -9,11 +9,13 @@
 (* This file defines the printer for natural numbers in [nat] *)
 
 (*i*)
+open Util
 open Glob_term
 open Bigint
 open Coqlib
 open Pp
 open Errors
+open Util
 (*i*)
 
 (**********************************************************************)
diff --git a/plugins/syntax/z_syntax.ml b/plugins/syntax/z_syntax.ml
index 7cad42d60d..8e5a07e0d6 100644
--- a/plugins/syntax/z_syntax.ml
+++ b/plugins/syntax/z_syntax.ml
@@ -8,6 +8,7 @@
 
 open Pp
 open Errors
+open Util
 open Names
 open Bigint
 
diff --git a/pretyping/arguments_renaming.ml b/pretyping/arguments_renaming.ml
index f9eafd3ec3..fca402c58e 100644
--- a/pretyping/arguments_renaming.ml
+++ b/pretyping/arguments_renaming.ml
@@ -11,6 +11,7 @@ open Names
 open Globnames
 open Term
 open Environ
+open Util
 open Libobject
 (*i*)
 
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index d9a050c083..d91273037d 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Util
 open Names
 open Term
 open Termops
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 1909528c54..ce4b830cfb 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -7,6 +7,7 @@
 (************************************************************************)
 
 open Errors
+open Util
 open Term
 open Inductive
 open Inductiveops
diff --git a/pretyping/typeclasses_errors.ml b/pretyping/typeclasses_errors.ml
index 4a0b66a7b6..053c1cd7b7 100644
--- a/pretyping/typeclasses_errors.ml
+++ b/pretyping/typeclasses_errors.ml
@@ -12,6 +12,7 @@ open Term
 open Evd
 open Environ
 open Constrexpr
+open Util
 open Globnames
 (*i*)
 
diff --git a/printing/tactic_printer.ml b/printing/tactic_printer.ml
index 551db10d55..e347b6c89a 100644
--- a/printing/tactic_printer.ml
+++ b/printing/tactic_printer.ml
@@ -8,6 +8,7 @@
 
 open Pp
 open Errors
+open Util
 open Evd
 open Tacexpr
 open Proof_type
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index d7379c9024..ff13cd46a2 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Util
 open Names
 open Term
 open Termops
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index 260d6d0926..fb8e6b16e8 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -7,6 +7,7 @@
 (************************************************************************)
 
 open Errors
+open Util
 open Names
 open Evd
 open Evarutil
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index ab80841d8b..3dbb2190b2 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -7,6 +7,7 @@
 (************************************************************************)
 
 open Pp
+open Util
 open Names
 open Entries
 open Environ
diff --git a/tactics/nbtermdn.ml b/tactics/nbtermdn.ml
index 5d5972089b..6459336b8a 100644
--- a/tactics/nbtermdn.ml
+++ b/tactics/nbtermdn.ml
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Util
 open Names
 open Term
 open Pattern
diff --git a/tactics/termdn.ml b/tactics/termdn.ml
index ffcde31aee..268c6a2e8a 100644
--- a/tactics/termdn.ml
+++ b/tactics/termdn.ml
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Util
 open Names
 open Term
 open Pattern
diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml
index 59cc3afd83..fa5dce73f3 100644
--- a/toplevel/auto_ind_decl.ml
+++ b/toplevel/auto_ind_decl.ml
@@ -11,6 +11,7 @@
 
 open Tacmach
 open Errors
+open Util
 open Pp
 open Termops
 open Declarations
diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml
index d1e379cca2..74e4701c0f 100644
--- a/toplevel/cerrors.ml
+++ b/toplevel/cerrors.ml
@@ -8,6 +8,7 @@
 
 open Pp
 open Errors
+open Util
 open Indtypes
 open Type_errors
 open Pretype_errors
diff --git a/toplevel/class.ml b/toplevel/class.ml
index dfb74b9e9e..7fe9239548 100644
--- a/toplevel/class.ml
+++ b/toplevel/class.ml
@@ -7,6 +7,7 @@
 (************************************************************************)
 
 open Errors
+open Util
 open Pp
 open Names
 open Term
diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml
index a7bc895c9a..8bfcfea6ae 100644
--- a/toplevel/ide_slave.ml
+++ b/toplevel/ide_slave.ml
@@ -8,6 +8,7 @@
 
 open Vernacexpr
 open Errors
+open Util
 open Pp
 open Printer
 
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index b9783a9cb1..a6677a78b0 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -3,6 +3,7 @@ open Globnames
 open Libobject
 open Entries
 open Decl_kinds
+open Util
 open Declare
 
 (**
diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml
index ace83cf64d..74ed231d17 100644
--- a/toplevel/toplevel.ml
+++ b/toplevel/toplevel.ml
@@ -8,6 +8,7 @@
 
 open Pp
 open Errors
+open Util
 open Flags
 open Vernac
 open Pcoq
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index a494a10cc1..b897a6d919 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -10,6 +10,7 @@
 
 open Pp
 open Errors
+open Util
 open Flags
 open System
 open Vernacexpr
diff --git a/toplevel/vernacinterp.ml b/toplevel/vernacinterp.ml
index dca47f7146..5b848e8342 100644
--- a/toplevel/vernacinterp.ml
+++ b/toplevel/vernacinterp.ml
@@ -8,6 +8,7 @@
 
 open Pp
 open Errors
+open Util
 
 let disable_drop e =
   if e <> Drop then e