Major reorganisation of the extraction "backend".

Initial Idea: getting rid of nasty renaming issues in modules, in
 particular bugs #820 (part d) #1340 #1526 #1654

Final effect: lots of changes, simplifications, cleanups, unrelated
 fixes and ehancements, and also probably some regressions (time will 
 tell). 

A few details:

* no more experimental "Toplevel" language. 
* no more functors Make in Ocaml/Haskell/Scheme. The spirit of these
  functors and Mlpp_params was already not followed much, and this 
  framework was more a nuisance that anything else. 
* instead, some records language_descr regrouping the specific 
  features of the different output languages. 
* Common now comes before Ocaml/Haskell/Scheme, these ones are now 
  independant from each others. print_structure_to_file is now 
  in Extract_env. 
* A nice detail: no more duplications of warnings concerning axioms. 
* In modular extraction, the clashes due to the opened modules 
  are now computed once and for all thanks to record_contents_fstlev, 
  instead of re-asking Coq each time about these opened modules and 
  using Extraction.constant_kind 
* some utilities about modules_path added and/or moved from Modutil 
  to Table. 
* using a .v file as a module, e.g. in a functor application should 
  now works in modular extraction. 

Now concerning renaming issues themselves: 

* printing is done twice, the first time toward /dev/null, in order
  to encounter the naming issues unsolvable by a simple qualification. 
  On the second run, we create artificial modules Coq__123 for 
  allowing qualification of these hidden objects. 
* names are now fully separated into their syntaxic categories: 
  terms/types/constructors/modules
* Only one last unsupported situation (but at least detected and 
  signaled by an error): an object M.t from an external file-module
  M.v can't be printed when a local module M is in the way. 
  This situation is really unlikely (in Coq you must use _long_
  file-module name, e.g. Init.Datatypes.nat). It could be solved
  by inserting "module Coq_123 = M" at the beginning of the file, 
  but then the signature of Coq_123 (that is, the one of M) should 
  be written explicitely in the .mli, which is _really_ not nice. 





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

1 files changed, 1 insertions, 17 deletions

diff --git a/contrib/extraction/scheme.mli b/contrib/extraction/scheme.mli
index bded1a8a8..573bb9cef 100644
--- a/contrib/extraction/scheme.mli
+++ b/contrib/extraction/scheme.mli
@@ -8,20 +8,4 @@
 
 (*i $Id$ i*)
 
-(*s Some utility functions to be reused in module [Haskell]. *)
-
-open Pp
-open Miniml
-open Names
-
-val keywords : Idset.t
-
-val preamble : 
-  extraction_params -> module_path list -> bool*bool*bool -> bool -> std_ppcmds
-
-module Make : functor(P : Mlpp_param) -> Mlpp
-
-
-
-
-
+val scheme_descr : Miniml.language_descr