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, 0 insertions, 10 deletions

diff --git a/contrib/extraction/extraction.mli b/contrib/extraction/extraction.mli
index b26a577e2..cb0600d05 100644
--- a/contrib/extraction/extraction.mli
+++ b/contrib/extraction/extraction.mli
@@ -26,16 +26,6 @@ val extract_fixpoint :
 
 val extract_inductive : env -> kernel_name -> ml_ind
 
-(*s ML declaration corresponding to a Coq reference. *)
-
-val extract_declaration : env -> global_reference -> ml_decl
-
-(*s Without doing complete extraction, just guess what a constant would be. *) 
-
-type kind = Logical | Term | Type 
-
-val constant_kind : env -> constant_body -> kind
-
 (*s Is a [ml_decl] or a [ml_spec] logical ? *) 
 
 val logical_decl : ml_decl -> bool