Extraction: (yet another) rework of the renaming code

 - Add module parameters in the structure of visible_layer,
   in order for module params to be part of name clash detection,
   avoiding this way a source of potentially wrong code.
 - In case of clash, module params are alpha-renamed to something
   unique (Foo__XXX where XXX is the number contained in the mbid).
   This solves some situations that were unsupported by extraction.
   for instance the "Module F (X:T). Module X:=X. ... End F."
 - We now check in Coq identifiers the presence of the
   extraction-reserved string __. If it is found, we issue a warning
   (which might become an error someday).

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

0 files changed, 0 insertions, 0 deletions