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, 8 insertions, 16 deletions

diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index a380654c6..6691e2622 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -82,7 +82,7 @@ let rec get_nth_label_mp n = function
 let common_prefix_from_list mp0 mpl =
   let prefixes = prefixes_mp mp0 in
   let rec f = function
-    | [] -> raise Not_found
+    | [] -> assert false
     | mp :: l -> if MPset.mem mp prefixes then mp else f l
   in f mpl
 
@@ -108,19 +108,6 @@ let labels_of_ref r =
   in
   parse_labels2 [l] mp_top mp
 
-
-
-
-let labels_of_ref2 r =
- let mp1,_,l =
-  match r with
-     ConstRef con -> repr_con con
-   | IndRef (kn,_)
-   | ConstructRef ((kn,_),_) -> repr_mind kn
-   | VarRef _ -> assert false
- in mp1,l
-
-
 let rec add_labels_mp mp = function
   | [] -> mp
   | l :: ll -> add_labels_mp (MPdot (mp,l)) ll
@@ -287,6 +274,10 @@ let check_inside_section () =
     err (str "You can't do that within a section." ++ fnl () ++
 	 str "Close it and try again.")
 
+let warning_id s =
+  msg_warning (str ("The identifier "^s^
+		    " contains __ which is reserved for the extraction"))
+
 let error_constant r =
   err (safe_pr_global r ++ str " is not a constant.")
 
@@ -296,8 +287,9 @@ let error_inductive r =
 let error_nb_cons () =
   err (str "Not the right number of constructors.")
 
-let error_module_clash s =
-  err (str ("There are two Coq modules with ML name " ^ s ^".\n") ++
+let error_module_clash mp1 mp2 =
+  err (str "The Coq modules " ++ pr_long_mp mp1 ++ str " and " ++
+       pr_long_mp mp2 ++ str " have the same ML name.\n" ++
        str "This is not supported yet. Please do some renaming first.")
 
 let error_unknown_module m =