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 ba5c68a5d..0f386ec04 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 adf611b56..b38177d48 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 830778307..202a3d770 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 098da5184..9e695e3d3 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 a015cdf92..f016a20b7 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 d9f3c3bf0..b2312d689 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 19075058a..2f7d480af 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 476a92bed..ffa1d304e 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 11d647d9a..143b22c34 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 de5158b14..13d1ec060 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 2d4b6169d..d721311e0 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 c26f652df..9dbbc947d 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 c2bd55128..2d958f799 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 8d298bc94..27683278b 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 861109d3d..a78ca750d 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 ffd87ce80..18b4c0c65 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 9c2b9b53d..41017c289 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 e7d9ba4b2..75205c964 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 25c01f2bd..d5eab32c4 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 01f32e4a3..b72476a75 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 44ae42090..f678b898b 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 8f34ec495..5219124cd 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 7cad42d60..8e5a07e0d 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 f9eafd3ec..fca402c58 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 d9a050c08..d91273037 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 1909528c5..ce4b830cf 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 4a0b66a7b..053c1cd7b 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 551db10d5..e347b6c89 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 d7379c902..ff13cd46a 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 260d6d092..fb8e6b16e 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 ab80841d8..3dbb2190b 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 5d5972089..6459336b8 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 ffcde31ae..268c6a2e8 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 59cc3afd8..fa5dce73f 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 d1e379cca..74e4701c0 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 dfb74b9e9..7fe923954 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 a7bc895c9..8bfcfea6a 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 b9783a9cb..a6677a78b 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 ace83cf64..74ed231d1 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 a494a10cc..b897a6d91 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 dca47f714..5b848e834 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