Extraction: handling modules (not functors) in Haskell by name mangling

 Module types are ignored, functors and module ident raise an error
 When dealing with simple modules, even nested, the structure
 hierarchy is removed, and names are arranged in the following way:
  - For the monolithic extraction, we simply use next_ident_away
    on short names, as we do when the same name appears in two .v.
  - For modular extraction, A.B.t become A__B__t or _A__B__t
    depending whether t is a type, a constructor or a constant.

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

0 files changed, 0 insertions, 0 deletions