Better extraction renaming phase (fix #1914 plus other non-reported bugs)

Ocaml :
- Fix the Coq__1 that was appearing in a .mli for some functor app
  in the corresponding .ml (virtual printing of the interface in the .ml +
  a pp_modname delayed in MTfunsig)
- Cleanup in MTwith parts
- Better handling of subst for MTsig
- Correct push/pop_visible in pp_struct/pp_signature

Common :
- Merge most of pp_global and pp_module
- Clarify the use of tables : remove some of them, attach many others
  to their corresponding function.
- The "visible" table now groups mps, their content, and some subst
  (for the inside of MTsig)
- Cleanup of tables is done via a registration mecanism
- No more "initial" create_renamings, instead some fully on-the-fly
  renaming (thanks to the "Pre" phase)
- opened libaries are computed between "Pre" and "Impl" phases
- for simplicity, static_clash aren't computed statically anymore (cost?)

Extract_env:
- A "Pre" phase not only for Ocaml
- Extraction Library is in fact also Recursive (for getting a right
  mpfiles_content) ... but only last item is printed to a real file
  instead of /dev/null

Modutil: No more struct_get_references_*

Util : fix the evaluation order of prlist_strict

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

1 files changed, 4 insertions, 2 deletions

diff --git a/lib/util.ml b/lib/util.ml
index 7df706393..2ac913607 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -1238,11 +1238,13 @@ let rec prlist elem l = match l with
   | h::t -> Stream.lapp (fun () -> elem h) (prlist elem t)
 
 (* unlike all other functions below, [prlist] works lazily.
-   if a strict behavior is needed, use [prlist_strict] instead. *)
+   if a strict behavior is needed, use [prlist_strict] instead.
+   evaluation is done from left to right. *)
 
 let rec prlist_strict elem l = match l with 
   | []   -> mt ()
-  | h::t -> (elem h)++(prlist_strict elem t)
+  | h::t ->
+      let e = elem h in let r = prlist_strict elem t in e++r
 
 (* [prlist_with_sep sep pr [a ; ... ; c]] outputs
    [pr a ++ sep() ++ ... ++ sep() ++ pr c] *)