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, 2 insertions, 2 deletions

diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli
index b215e373e..e64f1de15 100644
--- a/plugins/extraction/table.mli
+++ b/plugins/extraction/table.mli
@@ -18,11 +18,12 @@ val safe_basename_of_global : global_reference -> identifier
 val warning_axioms : unit -> unit
 val warning_both_mod_and_cst :
  qualid -> module_path -> global_reference -> unit
+val warning_id : string -> unit
 val error_axiom_scheme : global_reference -> int -> 'a
 val error_constant : global_reference -> 'a
 val error_inductive : global_reference -> 'a
 val error_nb_cons : unit -> 'a
-val error_module_clash : string -> 'a
+val error_module_clash : module_path -> module_path -> 'a
 val error_unknown_module : qualid -> 'a
 val error_scheme : unit -> 'a
 val error_not_visible : global_reference -> 'a
@@ -56,7 +57,6 @@ val common_prefix_from_list : module_path -> module_path list -> module_path
 val add_labels_mp : module_path -> label list -> module_path
 val get_nth_label_mp : int -> module_path -> label
 val labels_of_ref : global_reference -> module_path * label list
-val labels_of_ref2 : global_reference -> module_path * label
 
 (*s Some table-related operations *)