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

0 files changed, 0 insertions, 0 deletions