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

1 files changed, 1 insertions, 1 deletions

diff --git a/plugins/extraction/scheme.ml b/plugins/extraction/scheme.ml
index 9c600760f..64b86e6e2 100644
--- a/plugins/extraction/scheme.ml
+++ b/plugins/extraction/scheme.ml
@@ -195,7 +195,7 @@ and pp_module_expr = function
 
 let pp_struct =
   let pp_sel (mp,sel) =
-    push_visible mp;
+    push_visible mp [];
     let p = prlist_strict pp_structure_elem sel in
     pop_visible (); p
   in