Imported Upstream snapshot 8.3~beta0+13298

24 files changed, 0 insertions, 6688 deletions

diff --git a/contrib/extraction/BUGS b/contrib/extraction/BUGS
deleted file mode 100644
index 7f3f59c1..00000000
--- a/contrib/extraction/BUGS
+++ /dev/null
@@ -1,2 +0,0 @@
-It's not a bug, it's a lack of feature !!
-Cf TODO.
diff --git a/contrib/extraction/CHANGES b/contrib/extraction/CHANGES
deleted file mode 100644
index acd1dbda..00000000
--- a/contrib/extraction/CHANGES
+++ /dev/null
@@ -1,409 +0,0 @@
-7.4 -> 8.0
-
-No revolution this time. Mostly "behind-the-scene" clean-up and bug-fixes, 
-but also a few steps toward a more user-friendly extraction:
-
-* syntax of extraction: 
-- The old   (Recursive) Extraction Module M.
-  is now    (Recursive) Extraction Library M.
-  The old name was misleading since this command only works with M being a 
-  library M.v, and not a module produced by interactive command Module M. 
-- The other commands 
-    Extraction foo.
-    Recursive Extraction foo bar.
-    Extraction "myfile.ml" foo bar. 
-  now accept that foo can be a module name instead of just a constant name. 
-
-* Support of type scheme axioms (i.e. axiom whose type is an arity 
-  (x1:X1)...(xn:Xn)s with s a sort). For example: 
-
-   Axiom myprod : Set -> Set -> Set.
-   Extract Constant myprod "'a" "'b" => "'a * 'b". 
-   Recursive Extraction myprod. 
-   -------> type ('a,'b) myprod = 'a * 'b		
-
-* More flexible support of axioms. When an axiom isn't realized via Extract 
-  Constant before extraction, a warning is produced (instead of an error), 
-  and the extracted code must be completed later by hand. To find what
-  needs to be completed, search for the following string: AXIOM TO BE REALIZED
-
-* Cosmetics: When extraction produces a file, it tells it. 
-
-* (Experimental) It is allowed to extract under a opened interactive module
-  (but still outside sections). Feature to be used with caution. 
-
-* A problem has been identified concerning .v files used as normal interactive 
-  modules, like in 
-    
-    <file A.v>
-    Definition foo :=O.
-    <End file A.v>
-
-    <at toplevel>
-    Require A.
-    Module M:=A
-    Extraction M.
-
-  I might try to support that in the future. In the meanwhile, the
-  current behaviour of extraction is to forbid this.
-
-* bug fixes: 
-- many concerning Records. 
-- a Stack Overflow with mutual inductive (PR#320)
-- some optimizations have been removed since they were not type-safe:
-  For example if e has type:  type 'x a = A
-  Then:       match e with A -> A     -----X---->    e
-  To be investigated further.
-
-
-7.3 -> 7.4
-
-* The two main new features: 
-  - Automatic generation of Obj.magic when the extracted code 
-  in Ocaml is not directly typable.
-  - An experimental extraction of Coq's new modules to Ocaml modules. 
-
-* Concerning those Obj.magic: 
-  - The extraction now computes the expected type of any terms. Then 
-  it compares it with the actual type of the produced code. And when 
-  a mismatch is found, a Obj.magic is inserted. 
-  
-  - As a rule, any extracted development that was compiling out of the box 
-  should not contain any Obj.magic. At the other hand, generation of 
-  Obj.magic is not optimized yet: there might be several of them at a place 
-  were one would have been enough. 
-  
-  - Examples of code needing those Obj.magic: 
-     * contrib/extraction/test_extraction.v in the Coq source
-     * in the users' contributions: 
-	Lannion
-	Lyon/CIRCUITS
-        Rocq/HIGMAN
- 
-  - As a side-effect of this Obj.magic feature, we now print the types 
-  of the extracted terms, both in .ml files as commented documentation 
-  and in interfaces .mli files
-
-  - This feature hasn't been ported yet to Haskell. We are aware of 
-  some unsafe casting functions like "unsafeCoerce" on some Haskell implems.
-  So it will eventually be done.
-
-* Concerning the extraction of Coq's new modules: 
-  - Taking in account the new Coq's modules system has implied a *huge*
-  rewrite of most of the extraction code.
-
-  - The extraction core (translation from Coq to an abstract mini-ML) 
-  is now complete and fairly stable, and supports modules, modules type 
-  and functors and all that stuff.
-
-  - The ocaml pretty-print part, especially the renaming issue, is 
-  clearly weaker, and certainly still contains bugs. 
-
-  - Nothing done for translating these Coq Modules to Haskell.
-
-  - A temporary drawback of this module extraction implementation is that 
-  efficiency (especially extraction speed) has been somehow neglected.
-  To improve ...
-
-  - As an interesting side-effect, definitions are now printed according to 
-  the user's original order. No more of this "dependency-correct but weird"
-  order. In particular realized axioms via Extract Constant are now at their 
-  right place, and not at the beginning. 
-
-* Other news: 
-  
-  - Records are now printed using the Ocaml record syntax
- 
-  - Syntax output toward Scheme. Quite funny, but quite experimental and 
-  not documented. I recommend using the bigloo compiler since it contains 
-  natively some pattern matching.
-
-  - the dummy constant "__" have changed. see README
-
-  - a few bug-fixes (#191 and others)
-
-7.2 -> 7.3
-
-* Improved documentation in the Reference Manual.
-
-* Theoretical bad news: 
-- a naughty example (see the end of test_extraction.v)
-forced me to stop eliminating lambdas and arguments corresponding to 
-so-called "arity" in the general case. 
-
-- The dummy constant used in extraction ( let prop = () in ocaml ) 
-may in some cases be applied to arguments. This problem is dealt by 
-generating sufficient abstraction before the (). 
-
-
-* Theoretical good news: 
-- there is now a mechanism that remove useless prop/arity lambdas at the 
-top of function declarations. If your function had signature 
-nat -> prop -> nat in the previous extraction, it will now be nat -> nat. 
-So the extractions of common terms should look very much like the old 
-V6.2 one, except in some particular cases (functions as parameters, partial 
-applications, etc). In particular the bad news above have nearly no 
-impact...
-
-
-* By the way there is no more "let prop = ()" in ocaml. Those () are
-directly inlined. And in Haskell the dummy constant is now __ (two
-underscore) and is defined by 
-__ = Prelude.error "Logical or arity value used"
-This dummy constant should never be evaluated when computing an
-informative value, thanks to the lazy strategy. Hence the error message. 
-
-
-* Syntax changes, see Documentation for details: 
-
-Extraction Language Ocaml.
-Extraction Language Haskell. 
-Extraction Language Toplevel.
-
-That fixes the target language of extraction. Default is Ocaml, even in the 
-coq toplevel: you can now do copy-paste from the coq toplevel without 
-renaming problems. Toplevel language is the ocaml pseudo-language used 
-previously used inside the coq toplevel: coq names are printed with the coq 
-way, i.e. with no renaming. 
-
-So there is no more particular commands for Haskell, like 
-Haskell Extraction "file" id. Just set your favourite language and go... 
-
-
-* Haskell extraction has been tested at last (and corrected...). 
-See specificities in Documentation. 
-
-
-* Extraction of CoInductive in Ocaml language is now correct: it uses the 
-Lazy.force and lazy features of Ocaml. 
-
-
-* Modular extraction in Ocaml is now far more readable: 
-instead of qualifying everywhere (A.foo), there are now some "open" at the 
-beginning of files. Possible clashes are dealt with. 
-
-
-* By default, any recursive function associated with an inductive type 
-(foo_rec and foo_rect when foo is inductive type) will now be inlined 
-in extracted code. 
-
-
-* A few constants are explicitely declared to be inlined in extracted code. 
-For the moment there are: 
-	Wf.Acc_rec
-	Wf.Acc_rect
-	Wf.well_founded_induction
-	Wf.well_founded_induction_type
-Those constants does not match the auto-inlining criterion based on strictness.
-Of course, you can still overide this behaviour via some Extraction NoInline. 
-
-* There is now a web page showing the extraction of all standard theories: 
-http://www.lri.fr/~letouzey/extraction
-
-
-7.1 -> 7.2 :
-
-* Syntax changes, see Documentation for more details: 
-
-Set/Unset Extraction Optimize. 
-
-Default is Set. This control all optimizations made on the ML terms 
-(mostly reduction of dummy beta/iota redexes, but also simplications on 
-Cases, etc). Put this option to Unset if you what a ML term as close as 
-possible to the Coq term.
-
-Set/Unset Extraction AutoInline. 
-
-Default in Set, so by default, the extraction mechanism feels free to 
-inline the bodies of some defined constants, according to some heuristics 
-like size of bodies, useness of some arguments, etc. Those heuristics are 
-not always perfect, you may want to disable this feature, do it by Unset. 
-
-Extraction Inline toto foo. 
-Extraction NoInline titi faa bor. 
-
-In addition to the automatic inline feature, you can now tell precisely to 
-inline some more constants by the Extraction Inline command. Conversely, 
-you can forbid the inlining of some specific constants by automatic inlining. 
-Those two commands enable a precise control of what is inlined and what is not. 
-
-Print Extraction Inline. 
-
-Sum up the current state of the table recording the custom inlings 
-(Extraction (No)Inline). 
-
-Reset Extraction Inline. 
-
-Put the table recording the custom inlings back to empty. 
-
-As a consequence, there is no more need for options inside the commands of 
-extraction: 
-
-Extraction foo. 
-Recursive Extraction foo bar. 
-Extraction "file" foo bar. 
-Extraction Module Mymodule. 
-Recursive Extraction Module Mymodule. 
-
-New: The last syntax extracts the module Mymodule and all the modules 
-it depends on. 
-
-You can also try the Haskell versions (not tested yet): 
-
-Haskell Extraction foo.
-Haskell Recursive Extraction foo bar.
-Haskell Extraction "file" foo bar.
-Haskell Extraction Module Mymodule.
-Haskell Recursive Extraction Module Mymodule.
-
-And there's still the realization syntax: 
-
-Extract Constant coq_bla => "caml_bla".
-Extract Inlined Constant coq_bla => "caml_bla".
-Extract Inductive myinductive => mycamlind [my_caml_constr1 ... ].
-
-Note that now, the Extract Inlined Constant command is sugar for an Extract 
-Constant followed by a Extraction Inline. So be careful with 
-Reset Extraction Inline. 
-
- 
-
-* Lot of works around optimization of produced code. Should make code more 
-readable. 
-
-- fixpoint definitions : there should be no more stupid printings like 
-
-let foo x = 
-  let rec f x = 
-    .... (f y) ....
-  in f x
-
-but rather 
-
-let rec foo x = 
-  .... (foo y) .... 
-
-- generalized iota (in particular iota and permutation cases/cases):
-
-A generalized iota redex is a "Cases e of ...." where e is ok. 
-And the recursive predicate "ok" is given by:  
-e is ok if e is a Constructor or a Cases where all branches are ok.
-In the case of generalized iota redex, it might be good idea to reduce it, 
-so we do it. 
-Example: 
-
-match (match t with 
-         O -> Left
-       | S n -> match n with 
-                  O -> Right 
-                | S m -> Left) with 
- Left -> blabla 
-| Right -> bloblo
-
-After simplification, that gives: 
-
-match t with 
-  O -> blabla
-| S n -> match n with 
-          O -> bloblo
-        | S n -> blabla
-
-As shown on the example, code duplication can occur. In practice 
-it seems not to happen frequently. 
-
-- "constant" case:
-In V7.1 we used to simplify cases where all branches are the same. 
-In V7.2 we can simplify in addition terms like 
-	cases e of 
-	  C1 x y -> f (C x y)
-	| C2 z -> f (C2 z) 
-If x y z don't occur in f, we can produce (f e). 
-
-- permutation cases/fun: 
-extracted code has frequenty functions in branches of cases: 
-
-let foo x = match x with 
-   O -> fun _ -> .... 
- | S y -> fun _ -> .... 
-
-the optimization consist in lifting the common "fun _ ->", and that gives
- 
-let foo x _ = match x with 
-   O -> .....
- | S y -> ....
- 
-
-* Some bug corrections (many thanks in particular to Michel Levy). 
-
-* Testing in coq contributions: 
-If you are interested in extraction, you can look at the extraction tests 
-I'have put in the following coq contributions 
-
-Bordeaux/Additions			computation of fibonacci(2000)
-Bordeaux/EXCEPTIONS			multiplication using exception.
-Bordeaux/SearchTrees			list -> binary tree. maximum.
-Dyade/BDDS				boolean tautology checker.
-Lyon/CIRCUITS				multiplication via a modelization of a circuit.
-Lyon/FIRING-SQUAD			print the states of the firing squad.
-Marseille/CIRCUITS			compares integers via a modelization of a circuit. 
-Nancy/FOUnify				unification of two first-order terms.
-Rocq/ARITH/Chinese			computation of the chinese remainder.  
-Rocq/COC				small coc typechecker. (test by B. Barras, not by me)
-Rocq/HIGMAN				run the proof on one example. 
-Rocq/GRAPHS				linear constraints checker in Z. 
-Sophia-Antipolis/Stalmarck		boolean tautology checker.
-Suresnes/BDD				boolean tautology checker.
-
-Just do "make" in those contributions, the extraction test is integrated. 
-More tests will follow on more contributions.
-
-
-
-7.0 -> 7.1 : mostly bug corrections. No theoretical problems dealed with.
-
-* The semantics of Extract Constant changed: If you provide a extraction 
-for p by Extract Constant p => "0", your generated ML file will begin by 
-a let p = 0. The old semantics, which was to replace p everywhere by the
-provided terms, is still available via the Extract Inlined Constant p => 
-"0" syntax.
-
-
-* There are more optimizations applied to the generated code: 
-- identity cases: match e with P x y -> P x y | Q z -> Q z | ...
-is simplified into e. Especially interesting with the sumbool terms: 
-there will be no more match ... with Left -> Left | Right -> Right
-
-- constant cases: match e with P x y -> c | Q z -> c | ...
-is simplified into c as soon as x, y, z do not occur in c.
-So no more match ... with Left -> Left | Right -> Left.
-  
-
-* the extraction at Toplevel (Extraction foo and Recursive Extraction foo),
-which was only a development tool at the beginning, is now closer to 
-the real extraction to a file. In particular optimizations are done, 
-and constants like recursors ( ..._rec ) are expanded. 
-
-
-* the singleton optimization is now protected against circular type.
-( Remind : this optimization is the one that simplify 
-type 'a sig = Exists of 'a  into type 'a sig = 'a and 
-match e with (Exists c) -> d into let c = e in d ) 
-
-
-* Fixed one bug concerning casted code
-
-
-* The inductives generated should now have always correct type-var list 
-('a,'b,'c...)
-
-
-* Code cleanup until three days before release. Messing-up code 
-in the last three days before release.
-
-
-
-
-
-
-
-6.x -> 7.0 : Everything changed. See README
diff --git a/contrib/extraction/README b/contrib/extraction/README
deleted file mode 100644
index 7350365e..00000000
--- a/contrib/extraction/README
+++ /dev/null
@@ -1,139 +0,0 @@
-
-Status of Extraction in Coq version 7.x
-======================================
-
-(* 22 jan 2003 : Updated for version 7.4 *)
-
-
-J.C. Filliâtre
-P. Letouzey
-
-
-
-Extraction code has been completely rewritten since version V6.3. 
-This work is still not finished, but most parts of it are already usable. 
-In consequence it is included in the Coq V7.0 final release. 
-But don't be mistaken: 
-
-	THIS WORK IS STILL EXPERIMENTAL !
-
-1) Principles 
-
-The main goal of the new extraction is to handle any Coq term, even 
-those upon sort Type, and to produce code that always compiles. 
-Thus it will never answer something like "Not an ML type", but rather
-a dummy term like the ML unit. 
-
-Translation between Coq and ML is based upon the following principles: 
-
-- Terms of sort Prop don't have any computational meaning, so they are
-merged into one ML term "__". This part is done according to P. Letouzey's 
-works (*) and (**).
-
-This dummy constant "__" used to be implemented by the unit (), but 
-we recently found that this constant might be applied in some cases. 
-So "__" is now in Ocaml a fixpoint that forgets its arguments: 
-
-           let __ = let rec f _ = Obj.repr f in Obj.repr f
-
-
-- Terms that are type schemes (i.e. something of type ( : )( : )...s with 
-s a sort ) don't have any ML counterpart at the term level, since they 
-are types transformers. In fact they do not have any computational
-meaning either. So we also merge them into that dummy term "__".
-
-- A Coq term gives a ML term or a ML type depending of its type: 
-type schemes will (try to) give ML types, and all other terms give ML terms.
-
-And the rest of the translation is (almost) straightforward: an inductive
-gives an inductive, etc...
-
-This gives ML code that have no special reason to typecheck, due 
-to the incompatibilities between Coq and ML typing systems. In fact
-most of the time everything goes right. For example, it is sufficient 
-to extract and compile everything in the "theories" directory 
-(cf test subdirectory).
-
-We now verify during extraction that the produced code is typecheckable, 
-and if it is not we insert unsafe type casting at critical points in the 
-code. For the moment, it is an Ocaml-only feature, using the "Obj.magic"
-function, but the same kind of trick will be soon made in Haskell.
-
-
-2) Differences with previous extraction (V6.3 and before)
-
-2.a) The pros 
-
-The ability to extract every Coq term, as explain in the previous 
-paragraph. 
-
-The ability to extract from a file an ML module (cf Extraction Module in the 
-documentation)
-
-You can have a taste of extraction directly at the toplevel by 
-using the "Extraction <ident>" or the "Recursive Extraction <ident>".
-This toplevel extraction was already there in V6.3, but was printing 
-Fw terms. It now prints in the language of your choice: 
-Ocaml, Haskell, Scheme, or an Ocaml-like with Coq namings. 
-
-The optimization done on extracted code has been ported between 
-V6.3 and V7 and enhanced, and in particular the mechanism of automatic
-expansion. 
-
-2.b) The cons 
-
-The presence of some parasite "__" as dummy arguments
-in functions. This denotes the rests of a proof part. The previous 
-extraction was able to remove them totally. The current implementation
-removes a good deal of them (more that in 7.0), but not all. 
-
-This problem is due to extraction upon Type.
-For example, let's take this pathological term: 
-	(if b then Set else Prop)  : Type
-The only way to know if this is an Set (to keep) or a Prop (to remove) 
-is to compute the boolean b, and we do not want to do that during 
-extraction. 
-
-There is no more "ML import" feature. You can compensate by using 
-Axioms, and then "Extract Constant ..." 
-
-3) Examples 
-
-The file "test-extraction.v" is made of some examples used while debugging.
-
-In the subdirectory "test", you can test extraction on the Coq theories.
-Go there.
-"make tree" to make a local copy of the "theories" tree
-"make" to extract & compile most of the theories file in Ocaml
-"make -f Makefile.haskell" to extract & compile in Haskell
-
-See also Reference Manual for explanation of extraction syntaxes
-and more examples. 
-
-
-(*):
-Exécution de termes de preuves: une nouvelle méthode d'extraction 
-pour le Calcul des Constructions Inductives, Pierre Letouzey,
-DEA thesis, 2000, 
-http://www.lri.fr/~letouzey/download/rapport_dea.ps.gz
-
-(**) 
-A New Extraction for Coq, Pierre Letouzey, 
-Types 2002 Post-Workshop Proceedings, to appear, 
-draft at http://www.lri.fr/~letouzey/download/extraction2002.ps.gz
-
-
-Any feedback is welcome: 
-Pierre.Letouzey@lri.fr
-Jean.Christophe.Filliatre@lri.fr
-
-
-
-
-
-
-
-
-
-
-
diff --git a/contrib/extraction/TODO b/contrib/extraction/TODO
deleted file mode 100644
index 174be06e..00000000
--- a/contrib/extraction/TODO
+++ /dev/null
@@ -1,31 +0,0 @@
-
- 16. Haskell : 
-     - equivalent of Obj.magic (unsafeCoerce ?) 
-     - look again at the syntax (make it independant of layout ...)  
-     - producing .hi files
-     - modules/modules types/functors in Haskell ?
-
- 17. Scheme : 
-     - modular Scheme ? 
-
- 18. Improve speed (profiling)
-
- 19. Look again at those hugly renamings functions. 
-     Especially get rid of ML clashes like 
-   
-    let t = 0
-    module M = struct 
-       let t = 1 
-       let u = The.External.t (* ?? *)
-    end
-
- 20. Support the .v-as-internal-module, like in 
-    
-    <file A.v>
-    Definition foo :=O.
-    <End file A.v>
-
-    <at toplevel>
-    Require A.
-    Module M:=A
-    Extraction M.
\ No newline at end of file
diff --git a/contrib/extraction/common.ml b/contrib/extraction/common.ml
deleted file mode 100644
index 73f44e68..00000000
--- a/contrib/extraction/common.ml
+++ /dev/null
@@ -1,444 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(*i $Id: common.ml 13200 2010-06-25 22:36:25Z letouzey $ i*)
-
-open Pp
-open Util
-open Names
-open Term
-open Declarations
-open Nameops
-open Libnames
-open Table
-open Miniml
-open Mlutil
-open Modutil
-open Mod_subst
-
-let string_of_id id = ascii_of_ident (Names.string_of_id id)
-
-(*s Some pretty-print utility functions. *)
-
-let pp_par par st = if par then str "(" ++ st ++ str ")" else st
-
-let pp_apply st par args = match args with
-  | [] -> st
-  | _  -> hov 2 (pp_par par (st ++ spc () ++ prlist_with_sep spc identity args))
-
-let pr_binding = function
-  | [] -> mt ()
-  | l  -> str " " ++ prlist_with_sep (fun () -> str " ") pr_id l
-
-let fnl2 () = fnl () ++ fnl () 
-
-let space_if = function true -> str " " | false -> mt ()
-
-let sec_space_if = function true -> spc () | false -> mt ()
-
-let is_digit = function 
-  | '0'..'9' -> true
-  | _ -> false
-
-let begins_with_CoqXX s = 
-  let n = String.length s in 
-  n >= 4 && s.[0] = 'C' && s.[1] = 'o' && s.[2] = 'q' &&
-  let i = ref 3 in 
-  try while !i < n do
-    if s.[!i] = '_' then i:=n (*Stop*)
-    else if is_digit s.[!i] then incr i 
-    else raise Not_found
-  done; true
-  with Not_found -> false
-  
-let unquote s = 
-  if lang () <> Scheme then s 
-  else 
-    let s = String.copy s in 
-    for i=0 to String.length s - 1 do if s.[i] = '\'' then s.[i] <- '~' done;
-    s
-
-let rec dottify = function
-  | [] -> assert false
-  | [s] -> s
-  | s::[""] -> s
-  | s::l -> (dottify l)^"."^s
-
-(*s Uppercase/lowercase renamings. *)
-
-let is_upper s = match s.[0] with 'A' .. 'Z' -> true | _ -> false
-let is_lower s = match s.[0] with 'a' .. 'z' | '_' -> true | _ -> false
-
-let lowercase_id id = id_of_string (String.uncapitalize (string_of_id id))
-let uppercase_id id =
-  let s = string_of_id id in
-  assert (s<>"");
-  if s.[0] = '_' then id_of_string ("Coq_"^s)
-  else id_of_string (String.capitalize s)
-
-type kind = Term | Type | Cons | Mod
-
-let upperkind = function
-  | Type -> lang () = Haskell
-  | Term -> false
-  | Cons | Mod -> true
-
-let kindcase_id k id =
-  if upperkind k then uppercase_id id else lowercase_id id
-
-(*s de Bruijn environments for programs *)
-
-type env = identifier list * Idset.t
-
-(*s Generic renaming issues for local variable names. *)
-
-let rec rename_id id avoid = 
-  if Idset.mem id avoid then rename_id (lift_ident id) avoid else id
-
-let rec rename_vars avoid = function
-  | [] -> 
-      [], avoid
-  | id :: idl when id == dummy_name ->
-      (* we don't rename dummy binders *)
-      let (idl', avoid') = rename_vars avoid idl in
-      (id :: idl', avoid')
-  | id :: idl ->
-      let (idl, avoid) = rename_vars avoid idl in
-      let id = rename_id (lowercase_id id) avoid in
-      (id :: idl, Idset.add id avoid)
-
-let rename_tvars avoid l = 
-  let rec rename avoid = function 
-    | [] -> [],avoid 
-    | id :: idl -> 
-	let id = rename_id (lowercase_id id) avoid in 
-	let idl, avoid = rename (Idset.add id avoid) idl in 
-	(id :: idl, avoid) in
-  fst (rename avoid l)
-
-let push_vars ids (db,avoid) =
-  let ids',avoid' = rename_vars avoid ids in
-  ids', (ids' @ db, avoid')
-
-let get_db_name n (db,_) = 
-  let id = List.nth db (pred n) in 
-  if id = dummy_name then id_of_string "__" else id
-
-
-(*S Renamings of global objects. *)
-
-(*s Tables of global renamings *)
-
-let register_cleanup, do_cleanup =
-  let funs = ref [] in
-  (fun f -> funs:=f::!funs), (fun () -> List.iter (fun f -> f ()) !funs)
-
-type phase = Pre | Impl | Intf
-
-let set_phase, get_phase =
-  let ph = ref Impl in ((:=) ph), (fun () -> !ph)
-
-let set_keywords, get_keywords =
-  let k = ref Idset.empty in
-  ((:=) k), (fun () -> !k)
-
-let add_global_ids, get_global_ids =
-  let ids = ref Idset.empty in
-  register_cleanup (fun () -> ids := get_keywords ());
-  let add s = ids := Idset.add s !ids
-  and get () = !ids
-  in (add,get)
-
-let empty_env () = [], get_global_ids ()
-
-let mktable autoclean =
-  let h = Hashtbl.create 97 in
-  if autoclean then register_cleanup (fun () -> Hashtbl.clear h);
-  (Hashtbl.add h, Hashtbl.find h, fun () -> Hashtbl.clear h)
-
-(* A table recording objects in the first level of all MPfile *)
-
-let add_mpfiles_content,get_mpfiles_content,clear_mpfiles_content =
-  mktable false
-
-(*s The list of external modules that will be opened initially *)
-
-let mpfiles_add, mpfiles_mem, mpfiles_list, mpfiles_clear =
-  let m = ref MPset.empty in
-  let add mp = m:=MPset.add mp !m
-  and mem mp = MPset.mem mp !m
-  and list () = MPset.elements !m
-  and clear () = m:=MPset.empty
-  in
-  register_cleanup clear;
-  (add,mem,list,clear)
-
-(*s table indicating the visible horizon at a precise moment,
-    i.e. the stack of structures we are inside.
-
-  - The sequence of [mp] parts should have the following form: 
-  [X.Y; X; A.B.C; A.B; A; ...], i.e. each addition should either 
-  be a [MPdot] over the last entry, or something new, mainly 
-  [MPself], or [MPfile] at the beginning.
-
-  - The [content] part is used to recoard all the names already
-  seen at this level.
-  
-  - The [subst] part is here mainly for printing signature
-  (in which names are still short, i.e. relative to a [msid]).
-*)
-
-type visible_layer = { mp : module_path;
-		       content : ((kind*string),unit) Hashtbl.t }
-
-let pop_visible, push_visible, get_visible, subst_mp =
-  let vis = ref [] and sub = ref [empty_subst] in
-  register_cleanup (fun () -> vis := []; sub := [empty_subst]);
-  let pop () =
-    let v = List.hd !vis in
-    (* we save the 1st-level-content of MPfile for later use *)
-    if get_phase () = Impl && modular () && is_modfile v.mp
-    then add_mpfiles_content v.mp v.content;
-    vis := List.tl !vis;
-    sub := List.tl !sub
-  and push mp o =
-    vis := { mp = mp; content = Hashtbl.create 97 } :: !vis;
-    let s = List.hd !sub in
-    let s = match o with None -> s | Some msid -> add_msid msid mp s in
-    sub := s :: !sub
-  and get () = !vis
-  and subst mp = subst_mp (List.hd !sub) mp
-  in (pop,push,get,subst)
-
-let get_visible_mps () = List.map (function v -> v.mp) (get_visible ())
-let top_visible () = match get_visible () with [] -> assert false | v::_ -> v
-let top_visible_mp () = (top_visible ()).mp
-let add_visible ks = Hashtbl.add (top_visible ()).content ks ()
-
-(* table of local module wrappers used to provide non-ambiguous names *)
-
-let add_duplicate, check_duplicate =
-  let index = ref 0 and dups = ref Gmap.empty in
-  register_cleanup (fun () -> index := 0; dups := Gmap.empty);
-  let add mp l =
-     incr index;
-     let ren = "Coq__" ^ string_of_int (!index) in
-     dups := Gmap.add (mp,l) ren !dups
-  and check mp l = Gmap.find (subst_mp mp, l) !dups
-  in (add,check)
-
-type reset_kind = AllButExternal | Everything
-
-let reset_renaming_tables flag =
-  do_cleanup ();
-  if flag = Everything then clear_mpfiles_content ()
-
-(*S Renaming functions *)
-
-(* This function creates from [id] a correct uppercase/lowercase identifier. 
-   This is done by adding a [Coq_] or [coq_] prefix. To avoid potential clashes 
-   with previous [Coq_id] variable, these prefixes are duplicated if already 
-   existing. *)
-
-let modular_rename k id =
-  let s = string_of_id id in
-  let prefix,is_ok =
-    if upperkind k then "Coq_",is_upper else "coq_",is_lower
-  in
-  if not (is_ok s) ||
-    (Idset.mem id (get_keywords ())) ||
-    (String.length s >= 4 && String.sub s 0 4 = prefix)
-  then prefix ^ s
-  else s
-
-(*s For monolithic extraction, first-level modules might have to be renamed 
-    with unique numbers *)
-
-let modfstlev_rename =
-  let add_prefixes,get_prefixes,_ = mktable true in
-  fun l ->
-    let coqid = id_of_string "Coq" in
-    let id = id_of_label l in
-    try
-      let coqset = get_prefixes id in
-      let nextcoq = next_ident_away coqid coqset in
-      add_prefixes id (nextcoq::coqset);
-      (string_of_id nextcoq)^"_"^(string_of_id id)
-    with Not_found ->
-      let s = string_of_id id in
-      if is_lower s || begins_with_CoqXX s then
-	(add_prefixes id [coqid]; "Coq_"^s)
-      else
-	(add_prefixes id []; s)
-
-(*s Creating renaming for a [module_path] : first, the real function ... *)
-
-let rec mp_renaming_fun mp = match mp with
-  | _ when not (modular ()) && at_toplevel mp -> [""]
-  | MPdot (mp,l) ->
-      let lmp = mp_renaming mp in
-      if lmp = [""] then (modfstlev_rename l)::lmp
-      else (modular_rename Mod (id_of_label l))::lmp
-  | MPself msid -> [modular_rename Mod (id_of_msid msid)]
-  | MPbound mbid -> [modular_rename Mod (id_of_mbid mbid)]
-  | MPfile _ when not (modular ()) -> assert false (* see [at_toplevel] above *)
-  | MPfile _ ->
-      assert (get_phase () = Pre);
-      let current_mpfile = (list_last (get_visible ())).mp in
-      if mp <> current_mpfile then mpfiles_add mp;
-      [string_of_modfile mp]
-
-(* ... and its version using a cache *)
-
-and mp_renaming =
-  let add,get,_ = mktable true in
-  fun x ->  try get x with Not_found -> let y = mp_renaming_fun x in add x y; y
-
-(*s Renamings creation for a [global_reference]: we build its fully-qualified
-    name in a [string list] form (head is the short name). *)
-
-let ref_renaming_fun (k,r) =
-  let mp = subst_mp (modpath_of_r r) in
-  let l = mp_renaming mp in
-  let s =
-    if l = [""] (* this happens only at toplevel of the monolithic case *)
-    then
-      let globs = Idset.elements (get_global_ids ()) in
-      let id = next_ident_away (kindcase_id k (safe_id_of_global r)) globs in
-      string_of_id id
-    else modular_rename k (safe_id_of_global r)
-  in
-  add_global_ids (id_of_string s);
-  s::l
-
-(* Cached version of the last function *)
-
-let ref_renaming =
-  let add,get,_ = mktable true in
-  fun x -> try get x with Not_found -> let y = ref_renaming_fun x in add x y; y
-
-(* [visible_clash mp0 (k,s)] checks if [mp0-s] of kind [k]
-   can be printed as [s] in the current context of visible
-   modules. More precisely, we check if there exists a 
-   visible [mp] that contains [s]. 
-   The verification stops if we encounter [mp=mp0]. *)
-
-let rec clash mem mp0 ks = function
-  | [] -> false
-  | mp :: _ when mp = mp0 -> false
-  | mp :: _ when mem mp ks -> true
-  | _ :: mpl -> clash mem mp0 ks mpl
-
-let mpfiles_clash mp0 ks =
-  clash (fun mp -> Hashtbl.mem (get_mpfiles_content mp)) mp0 ks
-    (List.rev (mpfiles_list ()))
-
-let visible_clash mp0 ks =
-  let rec clash = function
-    | [] -> false
-    | v :: _ when v.mp = mp0 -> false
-    | v :: _ when Hashtbl.mem v.content ks -> true
-    | _ :: vis -> clash vis
-  in clash (get_visible ())
-
-(* After the 1st pass, we can decide which modules will be opened initially *)
-
-let opened_libraries () =
-  if not (modular ()) then []
-  else
-    let used = mpfiles_list () in
-    let rec check_elsewhere avoid = function
-      | [] -> []
-      | mp :: mpl ->
-	  let clash s = Hashtbl.mem (get_mpfiles_content mp) (Mod,s) in
-	  if List.exists clash avoid
-	  then check_elsewhere avoid mpl
-	  else mp :: check_elsewhere (string_of_modfile mp :: avoid) mpl
-    in
-    let opened = check_elsewhere [] used in
-    mpfiles_clear ();
-    List.iter mpfiles_add opened;
-    opened
-
-(*s On-the-fly qualification issues for both monolithic or modular extraction. *)
-
-(* First, a function that factorize the printing of both [global_reference]
-   and module names for ocaml. When [k=Mod] then [olab=None], otherwise it 
-   contains the label of the reference to print. 
-   Invariant: [List.length ls >= 2], simpler situations are handled elsewhere. *)
-
-let pp_gen k mp ls olab =
-  try (* what is the largest prefix of [mp] that belongs to [visible]? *)
-    let prefix = common_prefix_from_list mp (get_visible_mps ()) in
-    let delta = mp_length mp - mp_length prefix in
-    assert (k <> Mod || mp <> prefix); (* mp as whole module isn't in itself *)
-    let ls = list_firstn (delta + if k = Mod then 0 else 1) ls in
-    let s,ls' = list_sep_last ls in
-    (* Reference r / module path mp is of the form [<prefix>.s.<List.rev ls'>].
-       Difficulty: in ocaml the prefix part cannot be used for
-       qualification (we are inside it) and the rest of the long
-       name may be hidden. 
-       Solution: we duplicate the _definition_ of r / mp in a Coq__XXX module *)
-    let k' = if ls' = [] then k else Mod in
-    if visible_clash prefix (k',s) then
-      let front = if ls' = [] && k <> Mod then [s] else ls' in
-      let lab = (* label associated with s *)
-	if delta = 0 && k <> Mod then Option.get olab
-	else get_nth_label_mp delta mp
-      in
-      try dottify (front @ [check_duplicate prefix lab])
-      with Not_found ->
-	assert (get_phase () = Pre); (* otherwise it's too late *)
-	add_duplicate prefix lab; dottify ls
-    else dottify ls
-  with Not_found ->
-    (* [mp] belongs to a closed module, not one of [visible]. *)
-    let base = base_mp mp in
-    let base_s,ls1 = list_sep_last ls in
-    let s,ls2 = list_sep_last ls1 in
-    (* [List.rev ls] is [base_s :: s :: List.rev ls2] *)
-    let k' = if ls2 = [] then k else Mod in
-    if modular () && (mpfiles_mem base) &&
-      (not (mpfiles_clash base (k',s))) &&
-      (not (visible_clash base (k',s)))
-    then (* Standard situation of an object in another file: *)
-      (* Thanks to the "open" of this file we remove its name *)
-      dottify ls1
-    else if visible_clash base (Mod,base_s) then
-      error_module_clash base_s
-    else dottify ls
-
-let pp_global k r =
-  let ls = ref_renaming (k,r) in
-  assert (List.length ls > 1);
-  let s = List.hd ls in
-  let mp = subst_mp (modpath_of_r r) in
-  if mp = top_visible_mp () then
-    (* simpliest situation: definition of r (or use in the same context) *)
-    (* we update the visible environment *)
-    (add_visible (k,s); unquote s)
-  else match lang () with
-    | Scheme -> unquote s (* no modular Scheme extraction... *)
-    | Haskell -> if modular () then dottify ls else s
-	(* for the moment we always qualify in modular Haskell... *)
-    | Ocaml -> pp_gen k mp ls (Some (label_of_r r))
-
-(* The next function is used only in Ocaml extraction...*)
-let pp_module mp =
-  let mp = subst_mp mp in
-  let ls = mp_renaming mp in
-  if List.length ls = 1 then dottify ls
-  else match mp with
-    | MPdot (mp0,_) when mp0 = top_visible_mp () ->
-	(* simpliest situation: definition of mp (or use in the same context) *)
-	(* we update the visible environment *)
-	let s = List.hd ls in
-	add_visible (Mod,s); s
-    | _ -> pp_gen Mod mp ls None
-
-
diff --git a/contrib/extraction/common.mli b/contrib/extraction/common.mli
deleted file mode 100644
index b7e70414..00000000
--- a/contrib/extraction/common.mli
+++ /dev/null
@@ -1,57 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(*i $Id: common.mli 11559 2008-11-07 22:03:34Z letouzey $ i*)
-
-open Names
-open Libnames
-open Miniml
-open Mlutil
-open Pp
-
-val fnl2 : unit -> std_ppcmds
-val space_if : bool -> std_ppcmds
-val sec_space_if : bool -> std_ppcmds
-
-val pp_par : bool -> std_ppcmds -> std_ppcmds
-val pp_apply : std_ppcmds -> bool -> std_ppcmds list -> std_ppcmds 
-val pr_binding : identifier list -> std_ppcmds
-
-val rename_id : identifier -> Idset.t -> identifier
-
-type env = identifier list * Idset.t
-val empty_env : unit -> env
-
-val rename_vars: Idset.t -> identifier list -> env
-val rename_tvars: Idset.t -> identifier list -> identifier list 
-val push_vars : identifier list -> env -> identifier list * env
-val get_db_name : int -> env -> identifier
-
-type phase = Pre | Impl | Intf
-
-val set_phase : phase -> unit
-val get_phase : unit -> phase
-
-val opened_libraries : unit -> module_path list
-
-type kind = Term | Type | Cons | Mod
-
-val pp_global : kind -> global_reference -> string
-val pp_module : module_path -> string
-
-val top_visible_mp : unit -> module_path
-val push_visible : module_path -> mod_self_id option -> unit
-val pop_visible : unit -> unit
-
-val check_duplicate : module_path -> label -> string
-
-type reset_kind = AllButExternal | Everything
-
-val reset_renaming_tables : reset_kind -> unit
-
-val set_keywords : Idset.t -> unit
diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml
deleted file mode 100644
index 057a7b29..00000000
--- a/contrib/extraction/extract_env.ml
+++ /dev/null
@@ -1,529 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(*i $Id: extract_env.ml 13201 2010-06-25 22:36:27Z letouzey $ i*)
-
-open Term
-open Declarations
-open Names
-open Libnames
-open Pp
-open Util
-open Miniml
-open Table
-open Extraction
-open Modutil
-open Common
-open Mod_subst
-
-(***************************************)
-(*S Part I: computing Coq environment. *)
-(***************************************)
-
-let toplevel_env () = 
-  let seg = Lib.contents_after None in 
-  let get_reference = function 
-    | (_,kn), Lib.Leaf o ->
-	let mp,_,l = repr_kn kn in 
-	let seb = match Libobject.object_tag o with
-	  | "CONSTANT" -> SFBconst (Global.lookup_constant (constant_of_kn kn))
-	  | "INDUCTIVE" -> SFBmind (Global.lookup_mind kn) 
-	  | "MODULE" -> SFBmodule (Global.lookup_module (MPdot (mp,l)))
-	  | "MODULE TYPE" -> 
-	      SFBmodtype (Global.lookup_modtype (MPdot (mp,l)))
-	  | _ -> failwith "caught"
-	in l,seb
-    | _ -> failwith "caught"
-  in 
-  match current_toplevel () with 
-    | MPself msid -> SEBstruct (msid, List.rev (map_succeed get_reference seg))
-    | _ -> assert false
-
-let environment_until dir_opt = 
-  let rec parse = function 
-    | [] when dir_opt = None -> [current_toplevel (), toplevel_env ()]
-    | [] -> [] 
-    | d :: l -> 
-	match (Global.lookup_module (MPfile d)).mod_expr with 
-	  | Some meb -> 
-	      if dir_opt = Some d then [MPfile d, meb]
-	      else (MPfile d, meb) :: (parse l)
-	  | _ -> assert false
-  in parse (Library.loaded_libraries ())
-
-
-(*s Visit: 
-  a structure recording the needed dependencies for the current extraction *)
-
-module type VISIT = sig 
-  (* Reset the dependencies by emptying the visit lists *)
-  val reset : unit -> unit
-    
-  (* Add the module_path and all its prefixes to the mp visit list *)  
-  val add_mp : module_path -> unit
-    
-  (* Add kernel_name / constant / reference / ... in the visit lists. 
-     These functions silently add the mp of their arg in the mp list *)
-  val add_kn : kernel_name -> unit
-  val add_con : constant -> unit
-  val add_ref : global_reference -> unit
-  val add_decl_deps : ml_decl -> unit
-  val add_spec_deps : ml_spec -> unit
-
-  (* Test functions: 
-     is a particular object a needed dependency for the current extraction ? *)
-  val needed_kn : kernel_name -> bool 
-  val needed_con : constant -> bool
-  val needed_mp : module_path -> bool
-end
-  
-module Visit : VISIT = struct 
-  (* What used to be in a single KNset should now be split into a KNset
-     (for inductives and modules names) and a Cset for constants
-     (and still the remaining MPset) *)
-  type must_visit = 
-      { mutable kn : KNset.t; mutable con : Cset.t; mutable mp : MPset.t }
-  (* the imperative internal visit lists *)
-  let v = { kn = KNset.empty ; con = Cset.empty ; mp = MPset.empty } 
-  (* the accessor functions *)
-  let reset () = v.kn <- KNset.empty; v.con <- Cset.empty; v.mp <- MPset.empty
-  let needed_kn kn = KNset.mem kn v.kn
-  let needed_con c = Cset.mem c v.con
-  let needed_mp mp = MPset.mem mp v.mp
-  let add_mp mp = 
-    check_loaded_modfile mp; v.mp <- MPset.union (prefixes_mp mp) v.mp
-  let add_kn kn = v.kn <- KNset.add kn v.kn; add_mp (modpath kn)
-  let add_con c = v.con <- Cset.add c v.con; add_mp (con_modpath c)
-  let add_ref = function 
-    | ConstRef c -> add_con c
-    | IndRef (kn,_) | ConstructRef ((kn,_),_) -> add_kn kn
-    | VarRef _ -> assert false
-  let add_decl_deps = decl_iter_references add_ref add_ref add_ref 
-  let add_spec_deps = spec_iter_references add_ref add_ref add_ref
-end
-
-exception Impossible
-
-let check_arity env cb = 
-  let t = Typeops.type_of_constant_type env cb.const_type in
-  if Reduction.is_arity env t then raise Impossible
-
-let check_fix env cb i = 
-  match cb.const_body with 
-    | None -> raise Impossible
-    | Some lbody -> 
-	match kind_of_term (Declarations.force lbody) with 
-	  | Fix ((_,j),recd) when i=j -> check_arity env cb; (true,recd)
-	  | CoFix (j,recd) when i=j -> check_arity env cb; (false,recd)
-	  | _ -> raise Impossible
-
-let factor_fix env l cb msb = 
-  let _,recd as check = check_fix env cb 0 in 
-  let n = Array.length (let fi,_,_ = recd in fi) in
-  if n = 1 then [|l|], recd, msb
-  else begin 
-    if List.length msb < n-1 then raise Impossible; 
-    let msb', msb'' = list_chop (n-1) msb in 
-    let labels = Array.make n l in 
-    list_iter_i 
-      (fun j -> 
-	 function 
-	   | (l,SFBconst cb') -> 
-	       if check <> check_fix env cb' (j+1) then raise Impossible; 
-	       labels.(j+1) <- l; 
-	   | _ -> raise Impossible) msb'; 
-    labels, recd, msb''
-  end
-
-let build_mb expr typ_opt =
-  { mod_expr = Some expr;
-    mod_type = typ_opt;
-    mod_constraints = Univ.Constraint.empty;
-    mod_alias = Mod_subst.empty_subst;
-    mod_retroknowledge = [] }
-
-let my_type_of_mb env mb =
-  match mb.mod_type with
-    | Some mtb -> mtb
-    | None -> Modops.eval_struct env (Option.get mb.mod_expr)
-
-(** Ad-hoc update of environment, inspired by [Mod_type.check_with_aux_def].
-    To check with Elie. *)
-
-let env_for_mtb_with env mtb idl =
-  let msid,sig_b = match Modops.eval_struct env mtb with
-    | SEBstruct(msid,sig_b) -> msid,sig_b
-    | _ -> assert false
-  in
-  let l = label_of_id (List.hd idl) in
-  let before = fst (list_split_at (fun (l',_) -> l=l') sig_b) in
-  Modops.add_signature (MPself msid) before env
-
-(* From a [structure_body] (i.e. a list of [structure_field_body])
-   to specifications. *)
-
-let rec extract_sfb_spec env mp = function 
-  | [] -> [] 
-  | (l,SFBconst cb) :: msig -> 
-      let kn = make_con mp empty_dirpath l in 
-      let s = extract_constant_spec env kn cb in 
-      let specs = extract_sfb_spec env mp msig in
-      if logical_spec s then specs 
-      else begin Visit.add_spec_deps s; (l,Spec s) :: specs end
-  | (l,SFBmind _) :: msig -> 
-      let kn = make_kn mp empty_dirpath l in 
-      let s = Sind (kn, extract_inductive env kn) in 
-      let specs = extract_sfb_spec env mp msig in
-      if logical_spec s then specs 
-      else begin Visit.add_spec_deps s; (l,Spec s) :: specs end
-  | (l,SFBmodule mb) :: msig -> 
-      let specs = extract_sfb_spec env mp msig in 
-      let spec = extract_seb_spec env (my_type_of_mb env mb) in
-      (l,Smodule spec) :: specs
-  | (l,SFBmodtype mtb) :: msig -> 
-      let specs = extract_sfb_spec env mp msig in
-      (l,Smodtype (extract_seb_spec env mtb.typ_expr)) :: specs
-  | (l,SFBalias(mp1,typ_opt,_))::msig -> 
-      let mb = build_mb (SEBident mp1) typ_opt in
-      extract_sfb_spec env mp ((l,SFBmodule mb) :: msig)
-
-(* From [struct_expr_body] to specifications *)
-
-(* Invariant: the [seb] given to [extract_seb_spec] should either come:
-   - from a [mod_type] or [type_expr] field
-   - from the output of [Modops.eval_struct].
-   This way, any encountered [SEBident] should be a true module type.
-   For instance, [my_type_of_mb] ensures this invariant.
-*)
-
-and extract_seb_spec env = function
-  | SEBident mp -> Visit.add_mp mp; MTident mp
-  | SEBwith(mtb',With_definition_body(idl,cb))->
-      let env' = env_for_mtb_with env mtb' idl in
-      let mtb''= extract_seb_spec env mtb' in
-      (match extract_with_type env' cb with (* cb peut contenir des kn  *)
-	 | None ->  mtb''
-	 | Some (vl,typ) -> MTwith(mtb'',ML_With_type(idl,vl,typ)))
-  | SEBwith(mtb',With_module_body(idl,mp,_,_))-> 
-      Visit.add_mp mp;
-      MTwith(extract_seb_spec env mtb',
-	     ML_With_module(idl,mp))
-(* TODO: On pourrait peut-etre oter certaines eta-expansion, du genre:
-   | SEBfunctor(mbid,_,SEBapply(m,SEBident (MPbound mbid2),_)) 
-     when mbid = mbid2 -> extract_seb_spec env m 
-   (* faudrait alors ajouter un test de non-apparition de mbid dans mb *)
-*)
-  | SEBfunctor (mbid, mtb, mtb') -> 
-      let mp = MPbound mbid in 
-      let env' = Modops.add_module mp (Modops.module_body_of_type mtb) env in
-      MTfunsig (mbid, extract_seb_spec env mtb.typ_expr,
-		extract_seb_spec env' mtb')
-  | SEBstruct (msid, msig) -> 
-      let mp = MPself msid in 
-      let env' = Modops.add_signature mp msig env in 
-	MTsig (msid, extract_sfb_spec env' mp msig) 
-  | SEBapply _ as mtb ->
-      extract_seb_spec env (Modops.eval_struct env mtb)
-
-
-(* From a [structure_body] (i.e. a list of [structure_field_body])
-   to implementations. 
-
-   NB: when [all=false], the evaluation order of the list is
-   important: last to first ensures correct dependencies.
-*)
-
-let rec extract_sfb env mp all = function 
-  | [] -> [] 
-  | (l,SFBconst cb) :: msb -> 
-      (try 
-	 let vl,recd,msb = factor_fix env l cb msb in 
-	 let vc = Array.map (make_con mp empty_dirpath) vl in
-	 let ms = extract_sfb env mp all msb in 
-	 let b = array_exists Visit.needed_con vc in 
-	 if all || b then 
-	   let d = extract_fixpoint env vc recd in
-	   if (not b) && (logical_decl d) then ms 
-	   else begin Visit.add_decl_deps d; (l,SEdecl d) :: ms end
-	 else ms
-       with Impossible ->
-	 let ms = extract_sfb env mp all msb in 
-	 let c = make_con mp empty_dirpath l in 
-	 let b = Visit.needed_con c in 
-	 if all || b then 
-	   let d = extract_constant env c cb in
-	   if (not b) && (logical_decl d) then ms 
-	   else begin Visit.add_decl_deps d; (l,SEdecl d) :: ms end
-	 else ms)
-  | (l,SFBmind mib) :: msb ->
-      let ms = extract_sfb env mp all msb in
-      let kn = make_kn mp empty_dirpath l in 
-      let b = Visit.needed_kn kn in
-      if all || b then 
-	let d = Dind (kn, extract_inductive env kn) in 
-	if (not b) && (logical_decl d) then ms 
-	else begin Visit.add_decl_deps d; (l,SEdecl d) :: ms end
-      else ms
-  | (l,SFBmodule mb) :: msb -> 
-      let ms = extract_sfb env mp all msb in
-      let mp = MPdot (mp,l) in 
-      if all || Visit.needed_mp mp then 
-	(l,SEmodule (extract_module env mp true mb)) :: ms
-      else ms
-  | (l,SFBmodtype mtb) :: msb ->
-      let ms = extract_sfb env mp all msb in
-      let mp = MPdot (mp,l) in
-       if all || Visit.needed_mp mp then 
-	(l,SEmodtype (extract_seb_spec env mtb.typ_expr)) :: ms
-      else ms
-  | (l,SFBalias (mp1,typ_opt,_)) :: msb ->
-      let mb = build_mb (SEBident mp1) typ_opt in
-      extract_sfb env mp all ((l,SFBmodule mb) :: msb)
-
-(* From [struct_expr_body] to implementations *)
-
-and extract_seb env mpo all = function 
-  | SEBident mp ->  
-      if is_modfile mp && not (modular ()) then error_MPfile_as_mod mp false; 
-      Visit.add_mp mp; MEident mp 
-  | SEBapply (meb, meb',_) -> 
-      MEapply (extract_seb env None true meb, 
-	       extract_seb env None true meb')
-  | SEBfunctor (mbid, mtb, meb) -> 
-      let mp = MPbound mbid in 
-      let env' = Modops.add_module mp (Modops.module_body_of_type mtb) env in 
-      MEfunctor (mbid, extract_seb_spec env mtb.typ_expr,
-		 extract_seb env' None true meb)
-  | SEBstruct (msid, msb) -> 
-      let mp,msb = match mpo with 
-	| None -> MPself msid, msb 
-	| Some mp -> mp, Modops.subst_structure (map_msid msid mp) msb
-      in 
-      let env' = Modops.add_signature mp msb env in 
-      MEstruct (msid, extract_sfb env' mp all msb) 
-  | SEBwith (_,_) -> anomaly "Not available yet"
-
-and extract_module env mp all mb = 
-  (* [mb.mod_expr <> None ], since we look at modules from outside. *)
-  (* Example of module with empty [mod_expr] is X inside a Module F [X:SIG]. *)
-  { ml_mod_expr = extract_seb env (Some mp) all (Option.get mb.mod_expr);
-    ml_mod_type = extract_seb_spec env (my_type_of_mb env mb) }
-
-
-let unpack = function MEstruct (_,sel) -> sel | _ -> assert false 
-
-let mono_environment refs mpl = 
-  Visit.reset ();
-  List.iter Visit.add_ref refs; 
-  List.iter Visit.add_mp mpl; 
-  let env = Global.env () in 
-  let l = List.rev (environment_until None) in 
-  List.rev_map 
-    (fun (mp,m) -> mp, unpack (extract_seb env (Some mp) false m)) l
-
-(**************************************)
-(*S Part II : Input/Output primitives *)
-(**************************************)
-
-let descr () = match lang () with 
-  | Ocaml -> Ocaml.ocaml_descr 
-  | Haskell -> Haskell.haskell_descr 
-  | Scheme -> Scheme.scheme_descr
-
-(* From a filename string "foo.ml" or "foo", builds "foo.ml" and "foo.mli" 
-   Works similarly for the other languages. *)
-
-let default_id = id_of_string "Main"
-
-let mono_filename f = 
-  let d = descr () in 
-  match f with 
-    | None -> None, None, default_id
-    | Some f -> 
-	let f = 
-	  if Filename.check_suffix f d.file_suffix then 
-	    Filename.chop_suffix f d.file_suffix 
-	  else f
-	in
-	let id = 
-	  if lang () <> Haskell then default_id
-	  else try id_of_string (Filename.basename f)
-	  with _ -> error "Extraction: provided filename is not a valid identifier"
-	in
-	Some (f^d.file_suffix), Option.map ((^) f) d.sig_suffix, id
-
-(* Builds a suitable filename from a module id *)
-
-let module_filename fc =
-  let d = descr () in
-  let fn = if d.capital_file then fc else String.uncapitalize fc
-  in
-  Some (fn^d.file_suffix), Option.map ((^) fn) d.sig_suffix, id_of_string fc
-
-(*s Extraction of one decl to stdout. *)
-
-let print_one_decl struc mp decl =
-  let d = descr () in
-  reset_renaming_tables AllButExternal;
-  set_phase Pre;
-  ignore (d.pp_struct struc);
-  set_phase Impl;
-  push_visible mp None;
-  msgnl (d.pp_decl decl);
-  pop_visible ()
-
-(*s Extraction of a ml struct to a file. *)
-
-let formatter dry file =
-  if dry then Format.make_formatter (fun _ _ _ -> ()) (fun _ -> ())
-  else match file with
-    | None -> !Pp_control.std_ft
-    | Some cout ->
-	let ft = Pp_control.with_output_to cout in
-	Option.iter (Format.pp_set_margin ft) (Pp_control.get_margin ());
-	ft
-
-let print_structure_to_file (fn,si,mo) dry struc =
-  let d = descr () in
-  reset_renaming_tables AllButExternal;
-  let unsafe_needs = {
-    mldummy = struct_ast_search ((=) MLdummy) struc; 
-    tdummy = struct_type_search Mlutil.isDummy struc; 
-    tunknown = struct_type_search ((=) Tunknown) struc; 
-    magic = 
-      if lang () <> Haskell then false 
-      else struct_ast_search (function MLmagic _ -> true | _ -> false) struc }
-  in
-  (* First, a dry run, for computing objects to rename or duplicate *)
-  set_phase Pre;
-  let devnull = formatter true None in
-  msg_with devnull (d.pp_struct struc);
-  let opened = opened_libraries () in
-  (* Print the implementation *)
-  let cout = if dry then None else Option.map open_out fn in
-  let ft = formatter dry cout in
-  begin try
-    (* The real printing of the implementation *)
-    set_phase Impl;
-    msg_with ft (d.preamble mo opened unsafe_needs);
-    msg_with ft (d.pp_struct struc);
-    Option.iter close_out cout; 
-  with e -> 
-    Option.iter close_out cout; raise e
-  end;
-  if not dry then Option.iter info_file fn;
-  (* Now, let's print the signature *)
-  Option.iter
-    (fun si ->
-       let cout = open_out si in
-       let ft = formatter false (Some cout) in
-       begin try
-	 set_phase Intf;
-	 msg_with ft (d.sig_preamble mo opened unsafe_needs);
-	 msg_with ft (d.pp_sig (signature_of_structure struc));
-	 close_out cout;
-       with e -> 
-	 close_out cout; raise e 
-       end; 
-       info_file si)
-    (if dry then None else si)
-
-
-(*********************************************)
-(*s Part III: the actual extraction commands *)
-(*********************************************)
-
-
-let reset () =  
-  Visit.reset (); reset_tables (); reset_renaming_tables Everything
-
-let init modular = 
-  check_inside_section (); check_inside_module ();
-  set_keywords (descr ()).keywords;
-  set_modular modular;
-  reset ();
-  if modular && lang () = Scheme then error_scheme ()
-
-(* From a list of [reference], let's retrieve whether they correspond
-   to modules or [global_reference]. Warn the user if both is possible. *)
-
-let rec locate_ref = function
-  | [] -> [],[]
-  | r::l ->
-      let q = snd (qualid_of_reference r) in
-      let mpo = try Some (Nametab.locate_module q) with Not_found -> None
-      and ro = try Some (Nametab.locate q) with Not_found -> None in
-      match mpo, ro with
-	| None, None -> Nametab.error_global_not_found q
-	| None, Some r -> let refs,mps = locate_ref l in r::refs,mps
-	| Some mp, None -> let refs,mps = locate_ref l in refs,mp::mps
-	| Some mp, Some r ->
-	    warning_both_mod_and_cst q mp r;
-	    let refs,mps = locate_ref l in refs,mp::mps
-
-(*s Recursive extraction in the Coq toplevel. The vernacular command is
-    \verb!Recursive Extraction! [qualid1] ... [qualidn]. Also used when 
-    extracting to a file with the command: 
-    \verb!Extraction "file"! [qualid1] ... [qualidn]. *)
-
-let full_extr f (refs,mps) =
-  init false;
-  List.iter (fun mp -> if is_modfile mp then error_MPfile_as_mod mp true) mps;
-  let struc = optimize_struct refs (mono_environment refs mps) in
-  warning_axioms ();
-  print_structure_to_file (mono_filename f) false struc;
-  reset ()
-
-let full_extraction f lr = full_extr f (locate_ref lr)
-
-
-(*s Simple extraction in the Coq toplevel. The vernacular command 
-    is \verb!Extraction! [qualid]. *)
-
-let simple_extraction r = match locate_ref [r] with
-  | ([], [mp]) as p -> full_extr None p
-  | [r],[] ->
-      init false;
-      let struc = optimize_struct [r] (mono_environment [r] []) in
-      let d = get_decl_in_structure r struc in
-      warning_axioms ();
-      if is_custom r then msgnl (str "(** User defined extraction *)");
-      print_one_decl struc (modpath_of_r r) d;
-      reset ()
-  | _ -> assert false
-
-
-(*s (Recursive) Extraction of a library. The vernacular command is 
-  \verb!(Recursive) Extraction Library! [M]. *) 
-
-let extraction_library is_rec m =
-  init true; 
-  let dir_m = 
-    let q = make_short_qualid m in 
-    try Nametab.full_name_module q with Not_found -> error_unknown_module q
-  in 
-  Visit.add_mp (MPfile dir_m); 
-  let env = Global.env () in	
-  let l = List.rev (environment_until (Some dir_m)) in 
-  let select l (mp,meb) = 
-    if Visit.needed_mp mp 
-    then (mp, unpack (extract_seb env (Some mp) true meb)) :: l 
-    else l
-  in
-  let struc = List.fold_left select [] l in
-  let struc = optimize_struct [] struc in
-  warning_axioms ();
-  let print = function
-    | (MPfile dir as mp, sel) as e ->
-	let dry = not is_rec && dir <> dir_m in
-	let s = string_of_modfile mp in
-	print_structure_to_file (module_filename s) dry [e]
-    | _ -> assert false
-  in
-  List.iter print struc;
-  reset ()
diff --git a/contrib/extraction/extract_env.mli b/contrib/extraction/extract_env.mli
deleted file mode 100644
index 8d906985..00000000
--- a/contrib/extraction/extract_env.mli
+++ /dev/null
@@ -1,23 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(*i $Id: extract_env.mli 10895 2008-05-07 16:06:26Z letouzey $ i*)
-
-(*s This module declares the extraction commands. *)
-
-open Names
-open Libnames
-
-val simple_extraction : reference -> unit
-val full_extraction : string option -> reference list -> unit
-val extraction_library : bool -> identifier -> unit
-
-(* For debug / external output via coqtop.byte + Drop : *)
-
-val mono_environment : 
- global_reference list -> module_path list -> Miniml.ml_structure
diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml
deleted file mode 100644
index 2cf457c6..00000000
--- a/contrib/extraction/extraction.ml
+++ /dev/null
@@ -1,917 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(*i $Id: extraction.ml 11897 2009-02-09 19:28:02Z barras $ i*)
-
-(*i*)
-open Util
-open Names
-open Term
-open Declarations
-open Environ
-open Reduction
-open Reductionops
-open Inductive
-open Termops
-open Inductiveops
-open Recordops
-open Nameops
-open Summary
-open Libnames
-open Nametab
-open Miniml
-open Table
-open Mlutil
-(*i*)
-
-exception I of inductive_info
-
-(* A set of all fixpoint functions currently being extracted *)
-let current_fixpoints = ref ([] : constant list)
-
-let none = Evd.empty
-
-let type_of env c = Retyping.get_type_of env none (strip_outer_cast c)
-
-let sort_of env c = Retyping.get_sort_family_of env none (strip_outer_cast c)
-
-let is_axiom env kn = (Environ.lookup_constant kn env).const_body = None
-
-(*S Generation of flags and signatures. *)
-
-(* The type [flag] gives us information about any Coq term: 
-   \begin{itemize}
-   \item [TypeScheme] denotes a type scheme, that is 
-     something that will become a type after enough applications. 
-     More formally, a type scheme has type $(x_1:X_1)\ldots(x_n:X_n)s$ with 
-     [s = Set], [Prop] or [Type] 
-   \item [Default] denotes the other cases. It may be inexact after 
-     instanciation. For example [(X:Type)X] is [Default] and may give [Set]
-     after instanciation, which is rather [TypeScheme]
-   \item [Logic] denotes a term of sort [Prop], or a type scheme on sort [Prop]
-   \item [Info] is the opposite. The same example [(X:Type)X] shows 
-     that an [Info] term might in fact be [Logic] later on. 
-   \end{itemize} *)
-
-type info = Logic | Info
-
-type scheme = TypeScheme | Default
-
-type flag = info * scheme
-
-(*s [flag_of_type] transforms a type [t] into a [flag]. 
-  Really important function. *)
-
-let rec flag_of_type env t = 
-  let t = whd_betadeltaiota env none t in 
-  match kind_of_term t with
-    | Prod (x,t,c) -> flag_of_type (push_rel (x,None,t) env) c
-    | Sort (Prop Null) -> (Logic,TypeScheme)
-    | Sort _ -> (Info,TypeScheme)
-    | _ -> if (sort_of env t) = InProp then (Logic,Default) else (Info,Default)
-
-(*s Two particular cases of [flag_of_type]. *)
-
-let is_default env t = (flag_of_type env t = (Info, Default))
-
-exception NotDefault of kill_reason
-
-let check_default env t = 
-  match flag_of_type env t with 
-    | _,TypeScheme -> raise (NotDefault Ktype)
-    | Logic,_ -> raise (NotDefault Kother)
-    | _ -> ()
-
-let is_info_scheme env t = (flag_of_type env t = (Info, TypeScheme))
-
-(*s [type_sign] gernerates a signature aimed at treating a type application. *)
-
-let rec type_sign env c = 
-  match kind_of_term (whd_betadeltaiota env none c) with
-    | Prod (n,t,d) -> 
-	(if is_info_scheme env t then Keep else Kill Kother)
-	:: (type_sign (push_rel_assum (n,t) env) d)
-    | _ -> []
-
-let rec type_scheme_nb_args env c = 
-  match kind_of_term (whd_betadeltaiota env none c) with
-    | Prod (n,t,d) -> 
-	let n = type_scheme_nb_args (push_rel_assum (n,t) env) d in 
-	if is_info_scheme env t then n+1 else n
-    | _ -> 0
-
-let _ = register_type_scheme_nb_args type_scheme_nb_args
-
-(*s [type_sign_vl] does the same, plus a type var list. *)
-
-let rec type_sign_vl env c = 
-  match kind_of_term (whd_betadeltaiota env none c) with
-    | Prod (n,t,d) -> 
-	let s,vl = type_sign_vl (push_rel_assum (n,t) env) d in 
-	if not (is_info_scheme env t) then Kill Kother::s, vl
-	else Keep::s, (next_ident_away (id_of_name n) vl) :: vl
-    | _ -> [],[]
-
-let rec nb_default_params env c = 
-  match kind_of_term (whd_betadeltaiota env none c) with
-    | Prod (n,t,d) ->
-	let n = nb_default_params (push_rel_assum (n,t) env) d in 
-	if is_default env t then n+1 else n
-    | _ -> 0
-
-(*S Management of type variable contexts. *)
-
-(* A De Bruijn variable context (db) is a context for translating Coq [Rel]  
-   into ML type [Tvar]. *)
-
-(*s From a type signature toward a type variable context (db). *)
-
-let db_from_sign s = 
-  let rec make i acc = function 
-    | [] -> acc  
-    | Keep :: l -> make (i+1) (i::acc) l
-    | Kill _ :: l -> make i (0::acc) l
-  in make 1 [] s
-
-(*s Create a type variable context from indications taken from 
-  an inductive type (see just below). *) 
-
-let rec db_from_ind dbmap i = 
-  if i = 0 then []
-  else (try Intmap.find i dbmap with Not_found -> 0)::(db_from_ind dbmap (i-1))
-
-(*s [parse_ind_args] builds a map: [i->j] iff the i-th Coq argument 
-  of a constructor corresponds to the j-th type var of the ML inductive. *)
-
-(* \begin{itemize}
-   \item [si] : signature of the inductive
-   \item [i] :  counter of Coq args for [(I args)] 
-   \item [j] : counter of ML type vars 
-   \item [relmax] : total args number of the constructor 
-   \end{itemize} *)
-
-let parse_ind_args si args relmax = 
-  let rec parse i j = function 
-    | [] -> Intmap.empty
-    | Kill _ :: s -> parse (i+1) j s
-    | Keep :: s -> 
-      (match kind_of_term args.(i-1) with 
-	 | Rel k -> Intmap.add (relmax+1-k) j (parse (i+1) (j+1) s)
-	 | _ -> parse (i+1) (j+1) s)
-  in parse 1 1 si 
-
-(*S Extraction of a type. *)
-
-(* [extract_type env db c args] is used to produce an ML type from the 
-   coq term [(c args)], which is supposed to be a Coq type. *)
-
-(* [db] is a context for translating Coq [Rel] into ML type [Tvar]. *)
-
-(* [j] stands for the next ML type var. [j=0] means we do not 
-   generate ML type var anymore (in subterms for example). *) 
-
-
-let rec extract_type env db j c args = 
-  match kind_of_term (whd_betaiotazeta Evd.empty c) with
-    | App (d, args') ->
-	(* We just accumulate the arguments. *)
-	extract_type env db j d (Array.to_list args' @ args)
-    | Lambda (_,_,d) -> 
-	(match args with 
-	   | [] -> assert false (* otherwise the lambda would be reductible. *)
-	   | a :: args -> extract_type env db j (subst1 a d) args)
-    | Prod (n,t,d) ->
-	assert (args = []); 
-	let env' = push_rel_assum (n,t) env in 
-	(match flag_of_type env t with 
-	   | (Info, Default) -> 
-	       (* Standard case: two [extract_type] ... *)
-	       let mld = extract_type env' (0::db) j d [] in 
-	       (match expand env mld with 
-		  | Tdummy d -> Tdummy d
-		  | _ -> Tarr (extract_type env db 0 t [], mld))
-	   | (Info, TypeScheme) when j > 0 -> 
-	       (* A new type var. *)
-	       let mld = extract_type env' (j::db) (j+1) d [] in 
-	       (match expand env mld with 
-		  | Tdummy d -> Tdummy d
-		  | _ -> Tarr (Tdummy Ktype, mld))
-	   | _,lvl -> 
-	       let mld = extract_type env' (0::db) j d [] in 
-	       (match expand env mld with 
-		  | Tdummy d -> Tdummy d
-		  | _ -> 
-		      let reason = if lvl=TypeScheme then Ktype else Kother in
-		      Tarr (Tdummy reason, mld)))
-    | Sort _ -> Tdummy Ktype (* The two logical cases. *)
-    | _ when sort_of env (applist (c, args)) = InProp -> Tdummy Kother
-    | Rel n -> 
-	(match lookup_rel n env with
-           | (_,Some t,_) -> extract_type env db j (lift n t) args
-	   | _ -> 
-	       (* Asks [db] a translation for [n]. *)
-	       if n > List.length db then Tunknown 
-	       else let n' = List.nth db (n-1) in 
-	       if n' = 0 then Tunknown else Tvar n')
-    | Const kn -> 
-	let r = ConstRef kn in 
-	let cb = lookup_constant kn env in 
-	let typ = Typeops.type_of_constant_type env cb.const_type in 
-	(match flag_of_type env typ with 
-	   | (Info, TypeScheme) -> 
-	       let mlt = extract_type_app env db (r, type_sign env typ) args in 
-	       (match cb.const_body with 
-		  | None -> mlt
-		  | Some _ when is_custom r -> mlt 
-		  | Some lbody -> 
-		      let newc = applist (Declarations.force lbody, args) in 
-		      let mlt' = extract_type env db j newc [] in 
-		      (* ML type abbreviations interact badly with Coq *)
-		      (* reduction, so [mlt] and [mlt'] might be different: *)
-		      (* The more precise is [mlt'], extracted after reduction *)
-		      (* The shortest is [mlt], which use abbreviations *)
-		      (* If possible, we take [mlt], otherwise [mlt']. *)
-		      if expand env mlt = expand env mlt' then mlt else mlt')
-	   | _ -> (* only other case here: Info, Default, i.e. not an ML type *)
-	       (match cb.const_body with 
-		  | None -> Tunknown (* Brutal approximation ... *)
-		  | Some lbody -> 
-		      (* We try to reduce. *)
-		      let newc = applist (Declarations.force lbody, args) in 
-		      extract_type env db j newc []))
-    | Ind (kn,i) ->
-	let s = (extract_ind env kn).ind_packets.(i).ip_sign in  
-	extract_type_app env db (IndRef (kn,i),s) args
-    | Case _ | Fix _ | CoFix _ -> Tunknown
-    | _ -> assert false
-
-(* [extract_maybe_type] calls [extract_type] when used on a Coq type, 
-   and otherwise returns [Tdummy] or [Tunknown] *)
-
-and extract_maybe_type env db c = 
-  let t = whd_betadeltaiota env none (type_of env c) in 
-  if isSort t then extract_type env db 0 c [] 
-  else if sort_of env t = InProp then Tdummy Kother else Tunknown
-
-(*s Auxiliary function dealing with type application. 
-  Precondition: [r] is a type scheme represented by the signature [s], 
-  and is completely applied: [List.length args = List.length s]. *)
-		  
-and extract_type_app env db (r,s) args =
-  let ml_args = 
-    List.fold_right 
-      (fun (b,c) a -> if b=Keep then 
-	 let p = List.length (fst (splay_prod env none (type_of env c))) in
-         let db = iterate (fun l -> 0 :: l) p db in
-         (extract_type_scheme env db c p) :: a
-       else a)
-      (List.combine s args) []
-  in Tglob (r,  ml_args)
-
-(*S Extraction of a type scheme. *)
-
-(* [extract_type_scheme env db c p] works on a Coq term [c] which is
-  an informative type scheme. It means that [c] is not a Coq type, but will 
-  be when applied to sufficiently many arguments ([p] in fact).  
-  This function decomposes p lambdas, with eta-expansion if needed. *)
-
-(* [db] is a context for translating Coq [Rel] into ML type [Tvar]. *)
-
-and extract_type_scheme env db c p = 
-  if p=0 then extract_type env db 0 c [] 
-  else 
-    let c = whd_betaiotazeta Evd.empty c in 
-    match kind_of_term c with 
-      | Lambda (n,t,d) -> 
-          extract_type_scheme (push_rel_assum (n,t) env) db d (p-1)
-      | _ ->  
-          let rels = fst (splay_prod env none (type_of env c)) in
-          let env = push_rels_assum rels env in  
-          let eta_args = List.rev_map mkRel (interval 1 p) in 
-          extract_type env db 0 (lift p c) eta_args
-
-
-(*S Extraction of an inductive type. *)
-
-and extract_ind env kn = (* kn is supposed to be in long form *)
-  let mib = Environ.lookup_mind kn env in
-  try
-    (* For a same kn, we can get various bodies due to module substitutions.
-       We hence check that the mib has not changed from recording 
-       time to retrieving time. Ideally we should also check the env. *)
-    let (mib0,ml_ind) = lookup_ind kn in 
-    if not (mib = mib0) then raise Not_found; 
-    ml_ind
-  with Not_found -> 
-    (* First, if this inductive is aliased via a Module, *)
-    (* we process the original inductive. *)
-    Option.iter (fun kn -> ignore (extract_ind env kn)) mib.mind_equiv; 
-    (* Everything concerning parameters. *)
-    (* We do that first, since they are common to all the [mib]. *)
-    let mip0 = mib.mind_packets.(0) in 
-    let npar = mib.mind_nparams in
-    let epar = push_rel_context mib.mind_params_ctxt env in
-    (* First pass: we store inductive signatures together with *)
-    (* their type var list. *)
-    let packets = 
-      Array.map 
-	(fun mip ->
-	   let b = snd (mind_arity mip) <> InProp in
-	   let ar = Inductive.type_of_inductive env (mib,mip) in
-	   let s,v = if b then type_sign_vl env ar else [],[] in
-	   let t = Array.make (Array.length mip.mind_nf_lc) [] in 
-	   { ip_typename = mip.mind_typename;
-	     ip_consnames = mip.mind_consnames;
-	     ip_logical = (not b); 
-	     ip_sign = s; 
-	     ip_vars = v; 
-	     ip_types = t }) 
-	mib.mind_packets 
-    in 
-    add_ind kn mib
-      {ind_info = Standard; 
-       ind_nparams = npar; 
-       ind_packets = packets; 
-       ind_equiv = match mib.mind_equiv with 
-         | None -> NoEquiv 
-	 | Some kn -> Equiv kn
-      };
-    (* Second pass: we extract constructors *)
-    for i = 0 to mib.mind_ntypes - 1 do
-      let p = packets.(i) in 
-      if not p.ip_logical then
-	let types = arities_of_constructors env (kn,i) in 
-	for j = 0 to Array.length types - 1 do 
-	  let t = snd (decompose_prod_n npar types.(j)) in
-	  let prods,head = dest_prod epar t in 
-	  let nprods = List.length prods in 
-          let args = match kind_of_term head with
-            | App (f,args) -> args (* [kind_of_term f = Ind ip] *)
-            | _ -> [||]
-          in
-	  let dbmap = parse_ind_args p.ip_sign args (nprods + npar) in 
-	  let db = db_from_ind dbmap npar in 
-	  p.ip_types.(j) <- extract_type_cons epar db dbmap t (npar+1)
-	done
-    done;
-    (* Third pass: we determine special cases. *)
-    let ind_info = 
-      try 
-	if not mib.mind_finite then raise (I Coinductive); 
-	if mib.mind_ntypes <> 1 then raise (I Standard); 
-	let p = packets.(0) in 
-	if p.ip_logical then raise (I Standard);
-	if Array.length p.ip_types <> 1 then raise (I Standard);
-	let typ = p.ip_types.(0) in 
-	let l = List.filter (fun t -> not (isDummy (expand env t))) typ in 
-	if List.length l = 1 && not (type_mem_kn kn (List.hd l)) 
-	then raise (I Singleton); 
-	if l = [] then raise (I Standard);
-	if not mib.mind_record then raise (I Standard);
-	let ip = (kn, 0) in 
-	let r = IndRef ip in 
-	if is_custom r then raise (I Standard); 
-	(* Now we're sure it's a record. *)
-	(* First, we find its field names. *)
-	let rec names_prod t = match kind_of_term t with 
-	  | Prod(n,_,t) -> n::(names_prod t)
-	  | LetIn(_,_,_,t) -> names_prod t
-	  | Cast(t,_,_) -> names_prod t
-	  | _ -> []
-	in 
-	let field_names = 
-	  list_skipn mib.mind_nparams (names_prod mip0.mind_user_lc.(0)) in 
-	assert (List.length field_names = List.length typ);
-	let projs = ref Cset.empty in 
-	let mp,d,_ = repr_kn kn in 
-	let rec select_fields l typs = match l,typs with 
-	  | [],[] -> []
-	  | (Name id)::l, typ::typs -> 
-	      if isDummy (expand env typ) then select_fields l typs 
-	      else  
-		let knp = make_con mp d (label_of_id id) in 
-		if not (List.exists isKill (type2signature env typ))
-		then 
-		  projs := Cset.add knp !projs; 
-		(ConstRef knp) :: (select_fields l typs)
-	  | Anonymous::l, typ::typs -> 
-	      if isDummy (expand env typ) then select_fields l typs
-	      else error_record r
-	  | _ -> assert false 
-	in 
-	let field_glob = select_fields field_names typ
-	in
-	(* Is this record officially declared with its projections ? *)
-	(* If so, we use this information. *)
-	begin try 
-	  let n = nb_default_params env
-            (Inductive.type_of_inductive env (mib,mip0))
-	  in
-	  List.iter 
-	    (Option.iter 
-	       (fun kn -> if Cset.mem kn !projs then add_projection n kn))
-	    (lookup_projections ip)
-	with Not_found -> ()
-	end; 
-	Record field_glob
-      with (I info) -> info
-    in
-    let i = {ind_info = ind_info; 
-	     ind_nparams = npar; 
-	     ind_packets = packets; 
-	     ind_equiv = match mib.mind_equiv with 
-	       | None -> NoEquiv
-	       | Some kn -> Equiv kn }
-    in
-    add_ind kn mib i; 
-    i
-
-(*s [extract_type_cons] extracts the type of an inductive 
-  constructor toward the corresponding list of ML types. *)
-
-(* \begin{itemize}
-   \item [db] is a context for translating Coq [Rel] into ML type [Tvar] 
-   \item [dbmap] is a translation map (produced by a call to [parse_in_args])
-   \item [i] is the rank of the current product (initially [params_nb+1]) 
-   \end{itemize} *)
-
-and extract_type_cons env db dbmap c i =
-  match kind_of_term (whd_betadeltaiota env none c) with 
-    | Prod (n,t,d) -> 
-	let env' = push_rel_assum (n,t) env in
-	let db' = (try Intmap.find i dbmap with Not_found -> 0) :: db in
-	let l = extract_type_cons env' db' dbmap d (i+1) in 
-	(extract_type env db 0 t []) :: l 
-    | _ -> [] 
-
-(*s Recording the ML type abbreviation of a Coq type scheme constant. *)
-
-and mlt_env env r = match r with 
-  | ConstRef kn -> 
-      (try 
-	 if not (visible_con kn) then raise Not_found; 
-	 match lookup_term kn with 
-	   | Dtype (_,vl,mlt) -> Some mlt
-	   | _ -> None
-       with Not_found -> 
-	 let cb = Environ.lookup_constant kn env in
-	 let typ = Typeops.type_of_constant_type env cb.const_type in 
-	 match cb.const_body with
-	   | None -> None
-	   | Some l_body -> 
-	       (match flag_of_type env typ with 
-		  | Info,TypeScheme -> 
-		      let body = Declarations.force l_body in
-		      let s,vl = type_sign_vl env typ in 
-		      let db = db_from_sign s in 
-		      let t = extract_type_scheme env db body (List.length s) 
-		      in add_term kn (Dtype (r, vl, t)); Some t
-		  | _ -> None))
-  | _ -> None
-
-and expand env = type_expand (mlt_env env)
-and type2signature env = type_to_signature (mlt_env env)
-let type2sign env = type_to_sign (mlt_env env)
-let type_expunge env = type_expunge (mlt_env env)
-
-(*s Extraction of the type of a constant. *)
-
-let record_constant_type env kn opt_typ = 
-  try 
-    if not (visible_con kn) then raise Not_found; 
-    lookup_type kn 
-  with Not_found ->
-    let typ = match opt_typ with 
-      | None -> Typeops.type_of_constant env kn
-      | Some typ -> typ 
-    in let mlt = extract_type env [] 1 typ [] 
-    in let schema = (type_maxvar mlt, mlt)
-    in add_type kn schema; schema
-
-(*S Extraction of a term. *)
-
-(* Precondition: [(c args)] is not a type scheme, and is informative. *)
-
-(* [mle] is a ML environment [Mlenv.t]. *)
-(* [mlt] is the ML type we want our extraction of [(c args)] to have. *)
-
-let rec extract_term env mle mlt c args = 
-  match kind_of_term c with
-    | App (f,a) ->
-	extract_term env mle mlt f (Array.to_list a @ args)
-    | Lambda (n, t, d) ->
-	let id = id_of_name n in 
-	(match args with 
-	   | a :: l -> 
-	       (* We make as many [LetIn] as possible. *)
- 	       let d' = mkLetIn (Name id,a,t,applistc d (List.map (lift 1) l))
-	       in extract_term env mle mlt d' []
-	   | [] -> 
-	       let env' = push_rel_assum (Name id, t) env in 
-	       let id, a = try check_default env t; id, new_meta()
-	       with NotDefault d -> dummy_name, Tdummy d
-	       in 
-	       let b = new_meta () in 
-	       (* If [mlt] cannot be unified with an arrow type, then magic! *)
-	       let magic = needs_magic (mlt, Tarr (a, b)) in 
-	       let d' = extract_term env' (Mlenv.push_type mle a) b d [] in 
-	       put_magic_if magic (MLlam (id, d')))
-    | LetIn (n, c1, t1, c2) ->
-	let id = id_of_name n in 
-	let env' = push_rel (Name id, Some c1, t1) env in 
-	let args' = List.map (lift 1) args in 
-	(try 
-	  check_default env t1; 
-	  let a = new_meta () in 
-	  let c1' = extract_term env mle a c1 [] in
-	  (* The type of [c1'] is generalized and stored in [mle]. *)
-	  let mle' = Mlenv.push_gen mle a in 
-	  MLletin (id, c1', extract_term env' mle' mlt c2 args') 
-	with NotDefault d -> 
-	  let mle' = Mlenv.push_std_type mle (Tdummy d) in 
-	  ast_pop (extract_term env' mle' mlt c2 args'))
-    | Const kn ->
-	extract_cst_app env mle mlt kn args
-    | Construct cp ->
-	extract_cons_app env mle mlt cp args
-    | Rel n ->
-	(* As soon as the expected [mlt] for the head is known, *)
-	(* we unify it with an fresh copy of the stored type of [Rel n]. *)
-	let extract_rel mlt = put_magic (mlt, Mlenv.get mle n) (MLrel n)
-	in extract_app env mle mlt extract_rel args 
-    | Case ({ci_ind=ip},_,c0,br) ->
- 	extract_app env mle mlt (extract_case env mle (ip,c0,br)) args
-    | Fix ((_,i),recd) ->
- 	extract_app env mle mlt (extract_fix env mle i recd) args 
-    | CoFix (i,recd) ->
- 	extract_app env mle mlt (extract_fix env mle i recd) args
-    | Cast (c,_,_) -> extract_term env mle mlt c args
-    | Ind _ | Prod _ | Sort _ | Meta _ | Evar _ | Var _ -> assert false 
-
-(*s [extract_maybe_term] is [extract_term] for usual terms, else [MLdummy] *) 
-
-and extract_maybe_term env mle mlt c =
-  try check_default env (type_of env c); 
-    extract_term env mle mlt c [] 
-  with NotDefault d -> 
-    put_magic (mlt, Tdummy d) MLdummy
-
-(*s Generic way to deal with an application. *)
-
-(* We first type all arguments starting with unknown meta types. 
-   This gives us the expected type of the head. Then we use the 
-   [mk_head] to produce the ML head from this type. *)
-
-and extract_app env mle mlt mk_head args = 
-  let metas = List.map new_meta args in 
-  let type_head = type_recomp (metas, mlt) in 
-  let mlargs = List.map2 (extract_maybe_term env mle) metas args in 
-  if mlargs = [] then mk_head type_head else MLapp (mk_head type_head, mlargs)
-
-(*s Auxiliary function used to extract arguments of constant or constructor. *)
-
-and make_mlargs env e s args typs = 
-  let l = ref s in 
-  let keep () = match !l with [] -> true | b :: s -> l:=s; b=Keep in
-  let rec f = function  
-    | [], [] -> [] 
-    | a::la, t::lt when keep() -> extract_maybe_term env e t a :: (f (la,lt))
-    | _::la, _::lt -> f (la,lt)
-    | _ -> assert false 
-  in f (args,typs)
-
-(*s Extraction of a constant applied to arguments. *)
-
-and extract_cst_app env mle mlt kn args = 
-  (* First, the [ml_schema] of the constant, in expanded version. *) 
-  let nb,t = record_constant_type env kn None in 
-  let schema = nb, expand env t in 
-  (* Can we instantiate types variables for this constant ? *)
-  (* In Ocaml, inside the definition of this constant, the answer is no. *)
-  let instantiated = 
-    if lang () = Ocaml && List.mem kn !current_fixpoints then var2var' (snd schema)
-    else instantiation schema
-  in 
-  (* Then the expected type of this constant. *)
-  let a = new_meta () in 
-  (* We compare stored and expected types in two steps. *)
-  (* First, can [kn] be applied to all args ? *)
-  let metas = List.map new_meta args in 
-  let magic1 = needs_magic (type_recomp (metas, a), instantiated) in 
-  (* Second, is the resulting type compatible with the expected type [mlt] ? *)
-  let magic2 = needs_magic (a, mlt) in 
-  (* The internal head receives a magic if [magic1] *)
-  let head = put_magic_if magic1 (MLglob (ConstRef kn)) in 
-  (* Now, the extraction of the arguments. *)
-  let s = type2signature env (snd schema) in 
-  let ls = List.length s in 
-  let la = List.length args in
-  let mla = make_mlargs env mle s args metas in 
-  let mla =
-    if not magic1 then 
-      try 
-	let l,l' = list_chop (projection_arity (ConstRef kn)) mla in 
-	if l' <> [] then (List.map (fun _ -> MLexn "Proj Args") l) @ l'
-	else mla
-      with _ -> mla
-    else mla
-  in 			    
-  (* Different situations depending of the number of arguments: *)
-  if ls = 0 then put_magic_if magic2 head
-  else if List.mem Keep s then 
-    if la >= ls || not (List.exists isKill s) 
-    then 
-      put_magic_if (magic2 && not magic1) (MLapp (head, mla))
-    else 
-      (* Not enough arguments. We complete via eta-expansion. *)
-      let ls' = ls-la in
-      let s' = list_lastn ls' s in
-      let mla = (List.map (ast_lift ls') mla) @ (eta_args_sign ls' s') in
-      put_magic_if magic2 (anonym_or_dummy_lams (MLapp (head, mla)) s')
-  else if List.mem (Kill Kother) s then 
-    (* In the special case of always false signature, one dummy lam is left. *)
-    (* So a [MLdummy] is left accordingly. *) 
-    if la >= ls 
-    then put_magic_if (magic2 && not magic1) (MLapp (head, MLdummy :: mla))
-    else put_magic_if magic2 (dummy_lams head (ls-la-1))
-  else (* s is made only of [Kill Ktype] *)
-    if la >= ls 
-    then put_magic_if (magic2 && not magic1) (MLapp (head, mla))
-    else put_magic_if magic2 (dummy_lams head (ls-la))
-
-
-(*s Extraction of an inductive constructor applied to arguments. *)
-
-(* \begin{itemize}
-   \item In ML, contructor arguments are uncurryfied. 
-   \item We managed to suppress logical parts inside inductive definitions,
-   but they must appears outside (for partial applications for instance)
-   \item We also suppressed all Coq parameters to the inductives, since
-   they are fixed, and thus are not used for the computation.
-   \end{itemize} *)
-
-and extract_cons_app env mle mlt (((kn,i) as ip,j) as cp) args =
-  (* First, we build the type of the constructor, stored in small pieces. *)
-  let mi = extract_ind env kn in 
-  let params_nb = mi.ind_nparams in 
-  let oi = mi.ind_packets.(i) in 
-  let nb_tvars = List.length oi.ip_vars
-  and types = List.map (expand env) oi.ip_types.(j-1) in
-  let list_tvar = List.map (fun i -> Tvar i) (interval 1 nb_tvars) in 
-  let type_cons = type_recomp (types, Tglob (IndRef ip, list_tvar)) in
-  let type_cons = instantiation (nb_tvars, type_cons) in 
-  (* Then, the usual variables [s], [ls], [la], ... *)
-  let s = List.map (type2sign env) types in
-  let ls = List.length s in 
-  let la = List.length args in 
-  assert (la <= ls + params_nb);
-  let la' = max 0 (la - params_nb) in 
-  let args' = list_lastn la' args in 
-  (* Now, we build the expected type of the constructor *)
-  let metas = List.map new_meta args' in 
-  (* If stored and expected types differ, then magic! *)
-  let a = new_meta () in 
-  let magic1 = needs_magic (type_cons, type_recomp (metas, a)) in
-  let magic2 = needs_magic (a, mlt) in 
-  let head mla = 
-    if mi.ind_info = Singleton then 
-      put_magic_if magic1 (List.hd mla) (* assert (List.length mla = 1) *)
-    else put_magic_if magic1 (MLcons (mi.ind_info, ConstructRef cp, mla))
-  in 
-  (* Different situations depending of the number of arguments: *)
-  if la < params_nb then 
-    let head' = head (eta_args_sign ls s) in 
-    put_magic_if magic2 
-      (dummy_lams (anonym_or_dummy_lams head' s) (params_nb - la))
-  else 
-    let mla = make_mlargs env mle s args' metas in 
-    if la = ls + params_nb 
-    then put_magic_if (magic2 && not magic1) (head mla)
-    else (* [ params_nb <= la <= ls + params_nb ] *) 
-      let ls' = params_nb + ls - la in 
-      let s' = list_lastn ls' s in 
-      let mla = (List.map (ast_lift ls') mla) @ (eta_args_sign ls' s') in
-      put_magic_if magic2 (anonym_or_dummy_lams (head mla) s')
-
-(*S Extraction of a case. *)
-
-and extract_case env mle ((kn,i) as ip,c,br) mlt = 
-  (* [br]: bodies of each branch (in functional form) *)
-  (* [ni]: number of arguments without parameters in each branch *)
-  let ni = mis_constr_nargs_env env ip in
-  let br_size = Array.length br in 
-  assert (Array.length ni = br_size); 
-  if br_size = 0 then begin
-    add_recursors env kn; (* May have passed unseen if logical ... *)
-    MLexn "absurd case"
-  end else 
-    (* [c] has an inductive type, and is not a type scheme type. *)
-    let t = type_of env c in 
-    (* The only non-informative case: [c] is of sort [Prop] *)
-    if (sort_of env t) = InProp then 
-      begin 
-	add_recursors env kn; (* May have passed unseen if logical ... *)
-	(* Logical singleton case: *)
-	(* [match c with C i j k -> t] becomes [t'] *)
-	assert (br_size = 1);
-	let s = iterate (fun l -> Kill Kother :: l) ni.(0) [] in
-	let mlt = iterate (fun t -> Tarr (Tdummy Kother, t)) ni.(0) mlt in 
-	let e = extract_maybe_term env mle mlt br.(0) in 
-	snd (case_expunge s e)
-      end 
-    else 
-      let mi = extract_ind env kn in 
-      let oi = mi.ind_packets.(i) in 
-      let metas = Array.init (List.length oi.ip_vars) new_meta in 
-      (* The extraction of the head. *)
-      let type_head = Tglob (IndRef ip, Array.to_list metas) in
-      let a = extract_term env mle type_head c [] in 
-      (* The extraction of each branch. *)
-      let extract_branch i = 
-	(* The types of the arguments of the corresponding constructor. *)
-	let f t = type_subst_vect metas (expand env t) in 
-	let l = List.map f oi.ip_types.(i) in
-	(* the corresponding signature *)
-	let s = List.map (type2sign env) oi.ip_types.(i) in
-	(* Extraction of the branch (in functional form). *)
-	let e = extract_maybe_term env mle (type_recomp (l,mlt)) br.(i) in 
-	(* We suppress dummy arguments according to signature. *)
-	let ids,e = case_expunge s e in
-	(ConstructRef (ip,i+1), List.rev ids, e)
-      in
-      if mi.ind_info = Singleton then 
-	begin 
-	  (* Informative singleton case: *)
-	  (* [match c with C i -> t] becomes [let i = c' in t'] *)
-	  assert (br_size = 1);
-	  let (_,ids,e') = extract_branch 0 in
-	  assert (List.length ids = 1);
-	  MLletin (List.hd ids,a,e')
-	end 
-      else 
-	(* Standard case: we apply [extract_branch]. *)
-	MLcase ((mi.ind_info,[]), a, Array.init br_size extract_branch)
-  
-(*s Extraction of a (co)-fixpoint. *)
-
-and extract_fix env mle i (fi,ti,ci as recd) mlt = 
-  let env = push_rec_types recd env in 
-  let metas = Array.map new_meta fi in
-  metas.(i) <- mlt; 
-  let mle = Array.fold_left Mlenv.push_type mle metas in 
-  let ei = array_map2 (extract_maybe_term env mle) metas ci in 
-  MLfix (i, Array.map id_of_name fi, ei)
-
-(*S ML declarations. *)
-
-(* [decomp_lams_eta env c t] finds the number [n] of products in the type [t], 
-   and decompose the term [c] in [n] lambdas, with eta-expansion if needed. *)
-
-let rec decomp_lams_eta_n n env c t = 
-  let rels = fst (decomp_n_prod env none n t) in 
-  let rels = List.map (fun (id,_,c) -> (id,c)) rels in 
-  let m = nb_lam c in 
-  if m >= n then decompose_lam_n n c 
-  else
-    let rels',c = decompose_lam c in 
-    let d = n - m in 
-    (* we'd better keep rels' as long as possible. *)
-    let rels = (list_firstn d rels) @ rels' in
-    let eta_args = List.rev_map mkRel (interval 1 d) in 
-    rels, applist (lift d c,eta_args)
-
-(*s From a constant to a ML declaration. *)
-
-let extract_std_constant env kn body typ = 
-  reset_meta_count (); 
-  (* The short type [t] (i.e. possibly with abbreviations). *)
-  let t = snd (record_constant_type env kn (Some typ)) in 
-  (* The real type [t']: without head lambdas, expanded, *)
-  (* and with [Tvar] translated to [Tvar'] (not instantiable). *)
-  let l,t' = type_decomp (expand env (var2var' t)) in 
-  let s = List.map (type2sign env) l in 
-  (* The initial ML environment. *)
-  let mle = List.fold_left Mlenv.push_std_type Mlenv.empty l in 
-  (* Decomposing the top level lambdas of [body]. *)
-  let rels,c = decomp_lams_eta_n (List.length s) env body typ in
-  (* The lambdas names. *)
-  let ids = List.map (fun (n,_) -> id_of_name n) rels in 
-  (* The according Coq environment. *)
-  let env = push_rels_assum rels env in
-  (* The real extraction: *)
-  let e = extract_term env mle t' c [] in
-  (* Expunging term and type from dummy lambdas. *) 
-  term_expunge s (ids,e), type_expunge env t
-
-let extract_fixpoint env vkn (fi,ti,ci) = 
-  let n = Array.length vkn in 
-  let types = Array.make n (Tdummy Kother)
-  and terms = Array.make n MLdummy in 
-  let kns = Array.to_list vkn in 
-  current_fixpoints := kns; 
-  (* for replacing recursive calls [Rel ..] by the corresponding [Const]: *)
-  let sub = List.rev_map mkConst kns in 
-  for i = 0 to n-1 do 
-    if sort_of env ti.(i) <> InProp then begin 
-      let e,t = extract_std_constant env vkn.(i) (substl sub ci.(i)) ti.(i) in
-      terms.(i) <- e; 
-      types.(i) <- t;
-    end 
-  done; 
-  current_fixpoints := [];
-  Dfix (Array.map (fun kn -> ConstRef kn) vkn, terms, types) 
-		 
-let extract_constant env kn cb = 
-  let r = ConstRef kn in 
-  let typ = Typeops.type_of_constant_type env cb.const_type in 
-  match cb.const_body with
-    | None -> (* A logical axiom is risky, an informative one is fatal. *) 
-        (match flag_of_type env typ with
-	   | (Info,TypeScheme) -> 
-	       if not (is_custom r) then add_info_axiom r; 
-	       let n = type_scheme_nb_args env typ in 
-	       let ids = iterate (fun l -> anonymous::l) n [] in 
-	       Dtype (r, ids, Taxiom) 
-           | (Info,Default) -> 
-	       if not (is_custom r) then add_info_axiom r; 
-	       let t = snd (record_constant_type env kn (Some typ)) in 
-	       Dterm (r, MLaxiom, type_expunge env t) 
-           | (Logic,TypeScheme) -> 
-	       add_log_axiom r; Dtype (r, [], Tdummy Ktype)
-	   | (Logic,Default) -> 
-	       add_log_axiom r; Dterm (r, MLdummy, Tdummy Kother))
-    | Some body ->
-	(match flag_of_type env typ with
-	   | (Logic, Default) -> Dterm (r, MLdummy, Tdummy Kother)
-	   | (Logic, TypeScheme) -> Dtype (r, [], Tdummy Ktype)
-	   | (Info, Default) -> 
-	       let e,t = extract_std_constant env kn (force body) typ in 
-	       Dterm (r,e,t)
-	   | (Info, TypeScheme) -> 
-	       let s,vl = type_sign_vl env typ in 
-               let db = db_from_sign s in 
-               let t = extract_type_scheme env db (force body) (List.length s) 
-	       in Dtype (r, vl, t))
-
-let extract_constant_spec env kn cb = 
-  let r = ConstRef kn in 
-  let typ = Typeops.type_of_constant_type env cb.const_type in 
-  match flag_of_type env typ with 
-    | (Logic, TypeScheme) -> Stype (r, [], Some (Tdummy Ktype))
-    | (Logic, Default) -> Sval (r, Tdummy Kother) 
-    | (Info, TypeScheme) -> 
-	let s,vl = type_sign_vl env typ in 
-	(match cb.const_body with 
-	  | None -> Stype (r, vl, None)
-	  | Some body -> 
-	      let db = db_from_sign s in 
-	      let t = extract_type_scheme env db (force body) (List.length s)
-	      in Stype (r, vl, Some t)) 
-    | (Info, Default) -> 
-	let t = snd (record_constant_type env kn (Some typ)) in 
-	Sval (r, type_expunge env t)
-
-let extract_with_type env cb =
-  let typ = Typeops.type_of_constant_type env cb.const_type in
-  match flag_of_type env typ with
-    | (Info, TypeScheme) ->
-	let s,vl = type_sign_vl env typ in
-	let body = Option.get cb.const_body in
-	let db = db_from_sign s in
-	let t = extract_type_scheme env db (force body) (List.length s) in
-	Some (vl, t)
-    | _ -> None
-
-		   
-let extract_inductive env kn = 
-  let ind = extract_ind env kn in 
-  add_recursors env kn; 
-  let f l = List.filter (fun t -> not (isDummy (expand env t))) l in 
-  let packets = 
-    Array.map (fun p -> { p with ip_types = Array.map f p.ip_types }) 
-      ind.ind_packets
-  in { ind with ind_packets = packets }
-
-(*s Is a [ml_decl] logical ? *) 
-
-let logical_decl = function 
-  | Dterm (_,MLdummy,Tdummy _) -> true
-  | Dtype (_,[],Tdummy _) -> true 
-  | Dfix (_,av,tv) -> 
-      (array_for_all ((=) MLdummy) av) && 
-      (array_for_all isDummy tv)
-  | Dind (_,i) -> array_for_all (fun ip -> ip.ip_logical) i.ind_packets
-  | _ -> false
-
-(*s Is a [ml_spec] logical ? *)
-
-let logical_spec = function 
-  | Stype (_, [], Some (Tdummy _)) -> true
-  | Sval (_,Tdummy _) -> true
-  | Sind (_,i) -> array_for_all (fun ip -> ip.ip_logical) i.ind_packets
-  | _ -> false
diff --git a/contrib/extraction/extraction.mli b/contrib/extraction/extraction.mli
deleted file mode 100644
index 6d41b630..00000000
--- a/contrib/extraction/extraction.mli
+++ /dev/null
@@ -1,34 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(*i $Id: extraction.mli 10497 2008-02-01 12:18:37Z soubiran $ i*)
-
-(*s Extraction from Coq terms to Miniml. *)
-
-open Names
-open Term
-open Declarations
-open Environ
-open Libnames
-open Miniml
-
-val extract_constant : env -> constant -> constant_body -> ml_decl
-
-val extract_constant_spec : env -> constant -> constant_body -> ml_spec
-
-val extract_with_type : env -> constant_body -> ( identifier list * ml_type ) option
-
-val extract_fixpoint : 
-  env -> constant array -> (constr, types) prec_declaration -> ml_decl 
-
-val extract_inductive : env -> kernel_name -> ml_ind
-
-(*s Is a [ml_decl] or a [ml_spec] logical ? *) 
-
-val logical_decl : ml_decl -> bool
-val logical_spec : ml_spec -> bool
diff --git a/contrib/extraction/g_extraction.ml4 b/contrib/extraction/g_extraction.ml4
deleted file mode 100644
index 345cb307..00000000
--- a/contrib/extraction/g_extraction.ml4
+++ /dev/null
@@ -1,123 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(*i camlp4deps: "parsing/grammar.cma" i*)
-
-(* ML names *)
-
-open Vernacexpr
-open Pcoq
-open Genarg
-open Pp
-
-let pr_mlname _ _ _ s = spc () ++ qs s
-
-ARGUMENT EXTEND mlname
-  TYPED AS string
-  PRINTED BY pr_mlname
-| [ preident(id) ] -> [ id ]
-| [ string(s) ] -> [ s ]
-END
-
-open Table
-open Extract_env
-
-let pr_language = function
-  | Ocaml -> str "Ocaml" 
-  | Haskell -> str "Haskell"
-  | Scheme -> str "Scheme"
-
-VERNAC ARGUMENT EXTEND language
-PRINTED BY pr_language
-| [ "Ocaml" ] -> [ Ocaml ]
-| [ "Haskell" ] -> [ Haskell ]
-| [ "Scheme" ] -> [ Scheme ]
-END
-
-(* Extraction commands *)
-
-VERNAC COMMAND EXTEND Extraction
-(* Extraction in the Coq toplevel *)
-| [ "Extraction" global(x) ] -> [ simple_extraction x ]
-| [ "Recursive" "Extraction" ne_global_list(l) ] -> [ full_extraction None l ]
-
-(* Monolithic extraction to a file *)
-| [ "Extraction" string(f) ne_global_list(l) ] 
-  -> [ full_extraction (Some f) l ]
-END
-
-(* Modular extraction (one Coq library = one ML module) *)
-VERNAC COMMAND EXTEND ExtractionLibrary
-| [ "Extraction" "Library" ident(m) ]
-  -> [ extraction_library false m ]
-END
-
-VERNAC COMMAND EXTEND RecursiveExtractionLibrary
-| [ "Recursive" "Extraction" "Library" ident(m) ]
-  -> [ extraction_library true m ]
-END
-
-(* Target Language *)
-VERNAC COMMAND EXTEND ExtractionLanguage
-| [ "Extraction" "Language" language(l) ] 
-  -> [ extraction_language l ]
-END
-
-VERNAC COMMAND EXTEND ExtractionInline
-(* Custom inlining directives *)
-| [ "Extraction" "Inline" ne_global_list(l) ] 
-  -> [ extraction_inline true l ]
-END
-
-VERNAC COMMAND EXTEND ExtractionNoInline
-| [ "Extraction" "NoInline" ne_global_list(l) ] 
-  -> [ extraction_inline false l ]
-END
-
-VERNAC COMMAND EXTEND PrintExtractionInline
-| [ "Print" "Extraction" "Inline" ]
-  -> [ print_extraction_inline () ]
-END
-
-VERNAC COMMAND EXTEND ResetExtractionInline
-| [ "Reset" "Extraction" "Inline" ]
-  -> [ reset_extraction_inline () ]
-END
-
-VERNAC COMMAND EXTEND ExtractionBlacklist
-(* Force Extraction to not use some filenames *)
-| [ "Extraction" "Blacklist" ne_ident_list(l) ]
-  -> [ extraction_blacklist l ]
-END
-
-VERNAC COMMAND EXTEND PrintExtractionBlacklist
-| [ "Print" "Extraction" "Blacklist" ]
-  -> [ print_extraction_blacklist () ]
-END
-
-VERNAC COMMAND EXTEND ResetExtractionBlacklist
-| [ "Reset" "Extraction" "Blacklist" ]
-  -> [ reset_extraction_blacklist () ]
-END
-
-
-(* Overriding of a Coq object by an ML one *)
-VERNAC COMMAND EXTEND ExtractionConstant
-| [ "Extract" "Constant" global(x) string_list(idl) "=>" mlname(y) ]
-  -> [ extract_constant_inline false x idl y ]
-END
-
-VERNAC COMMAND EXTEND ExtractionInlinedConstant
-| [ "Extract" "Inlined" "Constant" global(x) "=>" mlname(y) ]
-  -> [ extract_constant_inline true x [] y ]
-END
-
-VERNAC COMMAND EXTEND ExtractionInductive
-| [ "Extract" "Inductive" global(x) "=>" mlname(id) "[" mlname_list(idl) "]" ]
-  -> [ extract_inductive x (id,idl) ]
-END
diff --git a/contrib/extraction/haskell.ml b/contrib/extraction/haskell.ml
deleted file mode 100644
index 3f0366e6..00000000
--- a/contrib/extraction/haskell.ml
+++ /dev/null
@@ -1,334 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(*i $Id: haskell.ml 11559 2008-11-07 22:03:34Z letouzey $ i*)
-
-(*s Production of Haskell syntax. *)
-
-open Pp
-open Util
-open Names
-open Nameops
-open Libnames
-open Table
-open Miniml
-open Mlutil
-open Common
-
-(*s Haskell renaming issues. *)
-
-let pr_lower_id id = str (String.uncapitalize (string_of_id id))
-let pr_upper_id id = str (String.capitalize (string_of_id id))
-
-let keywords =     
-  List.fold_right (fun s -> Idset.add (id_of_string s))
-  [ "case"; "class"; "data"; "default"; "deriving"; "do"; "else";
-    "if"; "import"; "in"; "infix"; "infixl"; "infixr"; "instance"; 
-    "let"; "module"; "newtype"; "of"; "then"; "type"; "where"; "_"; "__";
-    "as"; "qualified"; "hiding" ; "unit" ; "unsafeCoerce" ]
-  Idset.empty
-
-let preamble mod_name used_modules usf =
-  let pp_import mp = str ("import qualified "^ string_of_modfile mp ^"\n")
-  in 
-  (if not usf.magic then mt () 
-   else
-     str "{-# OPTIONS_GHC -cpp -fglasgow-exts #-}\n" ++
-     str "{- For Hugs, use the option -F\"cpp -P -traditional\" -}\n\n")
-  ++
-  str "module " ++ pr_upper_id mod_name ++ str " where" ++ fnl2 () ++
-  str "import qualified Prelude" ++ fnl () ++
-  prlist pp_import used_modules ++ fnl () ++ 
-  (if used_modules = [] then mt () else fnl ()) ++
-  (if not usf.magic then mt () 
-   else str "\
-#ifdef __GLASGOW_HASKELL__
-import qualified GHC.Base
-unsafeCoerce = GHC.Base.unsafeCoerce#
-#else
--- HUGS
-import qualified IOExts
-unsafeCoerce = IOExts.unsafeCoerce
-#endif" ++ fnl2 ())
-  ++
-  (if not usf.mldummy then mt () 
-   else str "__ = Prelude.error \"Logical or arity value used\"" ++ fnl2 ())
-
-let pp_abst = function
-  | [] -> (mt ())
-  | l  -> (str "\\" ++
-             prlist_with_sep (fun () -> (str " ")) pr_id l ++
-             str " ->" ++ spc ())
-
-(*s The pretty-printer for haskell syntax *)
-
-let pp_global k r = 
-  if is_inline_custom r then str (find_custom r) 
-  else str (Common.pp_global k r)
-
-(*s Pretty-printing of types. [par] is a boolean indicating whether parentheses
-    are needed or not. *)
-
-let kn_sig = 
-  let specif = MPfile (dirpath_of_string "Coq.Init.Specif") in 
-  make_kn specif empty_dirpath (mk_label "sig")
-
-let rec pp_type par vl t =
-  let rec pp_rec par = function
-    | Tmeta _ | Tvar' _ -> assert false 
-    | Tvar i -> (try pr_id (List.nth vl (pred i)) with _ -> (str "a" ++ int i))
-    | Tglob (r,[]) -> pp_global Type r	
-    | Tglob (r,l) -> 
-	if r = IndRef (kn_sig,0) then 
-	  pp_type true vl (List.hd l)
-	else 
-	  pp_par par 
-	    (pp_global Type r ++ spc () ++ 
-	     prlist_with_sep spc (pp_type true vl) l)
-    | Tarr (t1,t2) ->
-	pp_par par 
-	  (pp_rec true t1 ++ spc () ++ str "->" ++ spc () ++ pp_rec false t2)
-    | Tdummy _ -> str "()"
-    | Tunknown -> str "()"
-    | Taxiom -> str "() -- AXIOM TO BE REALIZED\n"
- in 
-  hov 0 (pp_rec par t)
-
-(*s Pretty-printing of expressions. [par] indicates whether
-    parentheses are needed or not. [env] is the list of names for the
-    de Bruijn variables. [args] is the list of collected arguments
-    (already pretty-printed). *)
-
-let expr_needs_par = function
-  | MLlam _  -> true
-  | MLcase _ -> true
-  | _        -> false 
-
-
-let rec pp_expr par env args =
-  let par' = args <> [] || par
-  and apply st = pp_apply st par args in 
-  function
-    | MLrel n -> 
-	let id = get_db_name n env in apply (pr_id id)
-    | MLapp (f,args') ->
-	let stl = List.map (pp_expr true env []) args' in
-        pp_expr par env (stl @ args) f
-    | MLlam _ as a -> 
-      	let fl,a' = collect_lams a in
-	let fl,env' = push_vars fl env in
-	let st = (pp_abst (List.rev fl) ++ pp_expr false env' [] a') in
-	apply (pp_par par' st)
-    | MLletin (id,a1,a2) ->
-	let i,env' = push_vars [id] env in
-	let pp_id = pr_id (List.hd i)
-	and pp_a1 = pp_expr false env [] a1
-	and pp_a2 = pp_expr (not par && expr_needs_par a2) env' [] a2 in
-	hv 0 
-	  (apply 
-	     (pp_par par' 
-		(hv 0 
-		   (hov 5 
-		      (str "let" ++ spc () ++ pp_id ++ str " = " ++ pp_a1) ++ 
-		    spc () ++ str "in") ++
-		 spc () ++ hov 0 pp_a2)))
-    | MLglob r -> 
-	apply (pp_global Term r)
-    | MLcons (_,r,[]) ->
-	assert (args=[]); pp_global Cons r
-    | MLcons (_,r,[a]) ->
-	assert (args=[]);
-	pp_par par (pp_global Cons r ++ spc () ++ pp_expr true env [] a)
-    | MLcons (_,r,args') ->
-	assert (args=[]);
-	pp_par par (pp_global Cons r ++ spc () ++ 
-		    prlist_with_sep spc (pp_expr true env []) args')
-    | MLcase ((_,factors),t, pv) ->
-      	apply (pp_par par' 
-		 (v 0 (str "case " ++ pp_expr false env [] t ++ str " of" ++
-		       fnl () ++ str "  " ++ pp_pat env factors pv)))
-    | MLfix (i,ids,defs) ->
-	let ids',env' = push_vars (List.rev (Array.to_list ids)) env in
-      	pp_fix par env' i (Array.of_list (List.rev ids'),defs) args
-    | MLexn s -> 
-	(* An [MLexn] may be applied, but I don't really care. *)
-	pp_par par (str "Prelude.error" ++ spc () ++ qs s)
-    | MLdummy ->
-	str "__" (* An [MLdummy] may be applied, but I don't really care. *)
-    | MLmagic a ->  
-	pp_apply (str "unsafeCoerce") par (pp_expr true env [] a :: args)
-    | MLaxiom -> pp_par par (str "Prelude.error \"AXIOM TO BE REALIZED\"")
-
-and pp_pat env factors pv = 
-  let pp_one_pat (name,ids,t) =
-    let ids,env' = push_vars (List.rev ids) env in
-    let par = expr_needs_par t in
-    hov 2 (pp_global Cons name ++
-	   (match ids with 
-	      | [] -> mt ()
-	      | _  -> (str " " ++ 
-		       prlist_with_sep 
-			 (fun () -> (spc ())) pr_id (List.rev ids))) ++
-	   str " ->" ++ spc () ++ pp_expr par env' [] t)
-  in 
-  prvecti 
-    (fun i x -> if List.mem i factors then mt () else 
-       (pp_one_pat pv.(i) ++
-	if factors = [] && i = Array.length pv - 1 then mt ()
-	else fnl () ++ str "  ")) pv
-  ++
-  match factors with 
-    | [] -> mt ()
-    | i::_ -> 
-	let (_,ids,t) = pv.(i) in 
-	let t = ast_lift (-List.length ids) t in 
-	hov 2 (str "_ ->" ++ spc () ++ pp_expr (expr_needs_par t) env [] t)
-
-(*s names of the functions ([ids]) are already pushed in [env],
-    and passed here just for convenience. *)
-
-and pp_fix par env i (ids,bl) args =
-  pp_par par
-    (v 0  
-       (v 2 (str "let" ++ fnl () ++
-	     prvect_with_sep fnl 
-	       (fun (fi,ti) -> pp_function env (pr_id fi) ti) 
-	       (array_map2 (fun a b -> a,b) ids bl)) ++ 
-	fnl () ++ 
-	hov 2 (str "in " ++ pp_apply (pr_id ids.(i)) false args)))
-
-and pp_function env f t =
-  let bl,t' = collect_lams t in
-  let bl,env' = push_vars bl env in
-  (f ++ pr_binding (List.rev bl) ++
-     str " =" ++ fnl () ++ str "  " ++
-     hov 2 (pp_expr false env' [] t'))
-
-(*s Pretty-printing of inductive types declaration. *)
-
-let pp_comment s = str "-- " ++ s ++ fnl ()
-
-let pp_logical_ind packet = 
-  pp_comment (pr_id packet.ip_typename ++ str " : logical inductive") ++
-  pp_comment (str "with constructors : " ++ 
-	      prvect_with_sep spc pr_id packet.ip_consnames)
-
-let pp_singleton kn packet = 
-  let l = rename_tvars keywords packet.ip_vars in 
-  let l' = List.rev l in 
-  hov 2 (str "type " ++ pp_global Type (IndRef (kn,0)) ++ spc () ++ 
-	 prlist_with_sep spc pr_id l ++
-	 (if l <> [] then str " " else mt ()) ++ str "=" ++ spc () ++
-	 pp_type false l' (List.hd packet.ip_types.(0)) ++ fnl () ++
-	 pp_comment (str "singleton inductive, whose constructor was " ++ 
-		     pr_id packet.ip_consnames.(0)))
-
-let pp_one_ind ip pl cv =
-  let pl = rename_tvars keywords pl in
-  let pp_constructor (r,l) =
-    (pp_global Cons r ++
-     match l with
-       | [] -> (mt ()) 
-       | _  -> (str " " ++
-      	       	prlist_with_sep 
-		  (fun () -> (str " ")) (pp_type true pl) l))
-  in
-  str (if Array.length cv = 0 then "type " else "data ") ++ 
-  pp_global Type (IndRef ip) ++ str " " ++
-  prlist_with_sep (fun () -> str " ") pr_lower_id pl ++
-  (if pl = [] then mt () else str " ") ++
-  if Array.length cv = 0 then str "= () -- empty inductive"
-  else 
-    (v 0 (str "= " ++
-	  prvect_with_sep (fun () -> fnl () ++ str "  | ") pp_constructor 
-	    (Array.mapi (fun i c -> ConstructRef (ip,i+1),c) cv)))
-  
-let rec pp_ind first kn i ind =
-  if i >= Array.length ind.ind_packets then 
-    if first then mt () else fnl () 
-  else 
-    let ip = (kn,i) in 
-    let p = ind.ind_packets.(i) in 
-    if is_custom (IndRef (kn,i)) then pp_ind first kn (i+1) ind 
-    else 
-      if p.ip_logical then  
-	pp_logical_ind p ++ pp_ind first kn (i+1) ind
-      else 
-	pp_one_ind ip p.ip_vars p.ip_types ++ fnl () ++ 
-	pp_ind false kn (i+1) ind
-	  
-
-(*s Pretty-printing of a declaration. *)
-
-let pp_string_parameters ids = prlist (fun id -> str id ++ str " ")
-
-let pp_decl = function
-  | Dind (kn,i) when i.ind_info = Singleton -> 
-      pp_singleton kn i.ind_packets.(0) ++ fnl ()
-  | Dind (kn,i) -> hov 0 (pp_ind true kn 0 i)
-  | Dtype (r, l, t) ->
-      if is_inline_custom r then mt () 
-      else 
-	let l = rename_tvars keywords l in 
-	let st = 
-	  try 
-	    let ids,s = find_type_custom r in 
-	    prlist (fun id -> str (id^" ")) ids ++ str "=" ++ spc () ++ str s
-	  with not_found -> 
-	    prlist (fun id -> pr_id id ++ str " ") l ++
-	    if t = Taxiom then str "= () -- AXIOM TO BE REALIZED\n"
-	    else str "=" ++ spc () ++ pp_type false l t
-	in 
-	hov 2 (str "type " ++ pp_global Type r ++ spc () ++ st) ++ fnl2 ()
-  | Dfix (rv, defs, typs) ->
-      let max = Array.length rv in 
-      let rec iter i = 
-	if i = max then mt () 
-	else
-	  let e = pp_global Term rv.(i) in 
-	  e ++ str " :: " ++ pp_type false [] typs.(i) ++ fnl () 
-	  ++ pp_function (empty_env ()) e defs.(i) ++ fnl2 ()
-	  ++ iter (i+1)
-      in iter 0
-  | Dterm (r, a, t) ->
-      if is_inline_custom r then mt () 
-      else 
-	let e = pp_global Term r in 
-	e ++ str " :: " ++ pp_type false [] t ++ fnl () ++
-	  if is_custom r then 	
-	    hov 0 (e ++ str " = " ++ str (find_custom r) ++ fnl2 ())
-	  else 
-	    hov 0 (pp_function (empty_env ()) e a ++ fnl2 ())
-
-let pp_structure_elem = function 
-  | (l,SEdecl d) -> pp_decl d
-  | (l,SEmodule m) -> 
-      failwith "TODO: Haskell extraction of modules not implemented yet"
-  | (l,SEmodtype m) -> 
-      failwith "TODO: Haskell extraction of modules not implemented yet"
-
-let pp_struct = 
-  let pp_sel (mp,sel) = 
-    push_visible mp None; 
-    let p = prlist_strict pp_structure_elem sel in 
-    pop_visible (); p
-  in 
-  prlist_strict pp_sel 
-
-
-let haskell_descr = {
-  keywords = keywords;  
-  file_suffix = ".hs"; 
-  capital_file = true;  
-  preamble = preamble; 
-  pp_struct = pp_struct; 
-  sig_suffix = None;
-  sig_preamble = (fun _ _ _ -> mt ()); 
-  pp_sig = (fun _ -> mt ());
-  pp_decl = pp_decl; 
-}
diff --git a/contrib/extraction/haskell.mli b/contrib/extraction/haskell.mli
deleted file mode 100644
index 1af9c231..00000000
--- a/contrib/extraction/haskell.mli
+++ /dev/null
@@ -1,12 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(*i $Id: haskell.mli 10232 2007-10-17 12:32:10Z letouzey $ i*)
-
-val haskell_descr : Miniml.language_descr
-
diff --git a/contrib/extraction/miniml.mli b/contrib/extraction/miniml.mli
deleted file mode 100644
index dfe4eb48..00000000
--- a/contrib/extraction/miniml.mli
+++ /dev/null
@@ -1,188 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(*i $Id: miniml.mli 10497 2008-02-01 12:18:37Z soubiran $ i*)
-
-(*s Target language for extraction: a core ML called MiniML. *)
-
-open Pp
-open Util
-open Names
-open Libnames
-
-(* The [signature] type is used to know how many arguments a CIC
-   object expects, and what these arguments will become in the ML
-   object. *)
-
-(* We eliminate from terms:  1) types 2) logical parts.
-   [Kother] stands both for logical or unknown reason. *)
-
-type kill_reason = Ktype | Kother
-
-type sign = Keep | Kill of kill_reason
-
-   
-(* Convention: outmost lambda/product gives the head of the list. *)
-
-type signature = sign list
-
-(*s ML type expressions. *)
-
-type ml_type = 
-  | Tarr    of ml_type * ml_type
-  | Tglob   of global_reference * ml_type list 
-  | Tvar    of int
-  | Tvar'   of int (* same as Tvar, used to avoid clash *)
-  | Tmeta   of ml_meta (* used during ML type reconstruction *)
-  | Tdummy  of kill_reason
-  | Tunknown
-  | Taxiom
-
-and ml_meta = { id : int; mutable contents : ml_type option }
-
-(* ML type schema. 
-   The integer is the number of variable in the schema. *)
-
-type ml_schema = int * ml_type 
-
-(*s ML inductive types. *)
-
-type inductive_info = 
-  | Singleton 
-  | Coinductive 
-  | Standard 
-  | Record of global_reference list 
-
-type case_info = int list (* list of branches to merge in a _ pattern *)
-
-(* A [ml_ind_packet] is the miniml counterpart of a [one_inductive_body]. 
-   If the inductive is logical ([ip_logical = false]), then all other fields
-   are unused. Otherwise, 
-   [ip_sign] is a signature concerning the arguments of the inductive, 
-   [ip_vars] contains the names of the type variables surviving in ML, 
-   [ip_types] contains the ML types of all constructors.    
-*)
-
-type ml_ind_packet = { 
-  ip_typename : identifier; 
-  ip_consnames : identifier array; 
-  ip_logical : bool;
-  ip_sign : signature; 
-  ip_vars : identifier list; 
-  ip_types : (ml_type list) array }  
-
-(* [ip_nparams] contains the number of parameters. *)
-
-type equiv = 
-  | NoEquiv
-  | Equiv of kernel_name 
-  | RenEquiv of string
-
-type ml_ind = {
-  ind_info : inductive_info;
-  ind_nparams : int; 	       
-  ind_packets : ml_ind_packet array;
-  ind_equiv : equiv
-}
-
-(*s ML terms. *)
-
-type ml_ast = 
-  | MLrel    of int
-  | MLapp    of ml_ast * ml_ast list
-  | MLlam    of identifier * ml_ast
-  | MLletin  of identifier * ml_ast * ml_ast
-  | MLglob   of global_reference
-  | MLcons   of inductive_info * global_reference * ml_ast list
-  | MLcase   of (inductive_info*case_info) * ml_ast * 
-      (global_reference * identifier list * ml_ast) array
-  | MLfix    of int * identifier array * ml_ast array
-  | MLexn    of string
-  | MLdummy
-  | MLaxiom
-  | MLmagic  of ml_ast
-
-(*s ML declarations. *)
-
-type ml_decl = 
-  | Dind  of kernel_name * ml_ind
-  | Dtype of global_reference * identifier list * ml_type
-  | Dterm of global_reference * ml_ast * ml_type
-  | Dfix  of global_reference array * ml_ast array * ml_type array
-
-type ml_spec = 
-  | Sind  of kernel_name * ml_ind
-  | Stype of global_reference * identifier list * ml_type option 
-  | Sval  of global_reference * ml_type
-
-type ml_specif = 
-  | Spec of ml_spec 
-  | Smodule of ml_module_type
-  | Smodtype of ml_module_type
-
-and ml_module_type = 
-  | MTident of module_path
-  | MTfunsig of mod_bound_id * ml_module_type * ml_module_type
-  | MTsig of mod_self_id * ml_module_sig
-  | MTwith of ml_module_type * ml_with_declaration
-
-and ml_with_declaration =  
-  | ML_With_type of identifier list * identifier list * ml_type
-  | ML_With_module of identifier list * module_path
-
-and ml_module_sig = (label * ml_specif) list
-
-type ml_structure_elem = 
-  | SEdecl of ml_decl
-  | SEmodule of ml_module
-  | SEmodtype of ml_module_type
-
-and ml_module_expr =
-  | MEident of module_path
-  | MEfunctor of mod_bound_id * ml_module_type * ml_module_expr 
-  | MEstruct of mod_self_id * ml_module_structure
-  | MEapply of ml_module_expr * ml_module_expr
-
-and ml_module_structure = (label * ml_structure_elem) list
-
-and ml_module = 
-    { ml_mod_expr : ml_module_expr; 
-      ml_mod_type : ml_module_type }
-
-(* NB: we do not translate the [mod_equiv] field, since [mod_equiv = mp] 
-   implies that [mod_expr = MEBident mp]. Same with [msb_equiv]. *)
-
-type ml_structure = (module_path * ml_module_structure) list
-
-type ml_signature = (module_path * ml_module_sig) list
-
-type unsafe_needs = {
-  mldummy : bool; 
-  tdummy : bool; 
-  tunknown : bool; 
-  magic : bool
-}
-
-type language_descr = {
-  keywords : Idset.t; 
-
-  (* Concerning the source file *)
-  file_suffix : string;  
-  capital_file : bool; (* should we capitalize filenames ? *)
-  preamble : identifier -> module_path list -> unsafe_needs -> std_ppcmds; 
-  pp_struct : ml_structure -> std_ppcmds; 
-
-  (* Concerning a possible interface file *)
-  sig_suffix : string option; 
-  sig_preamble : identifier -> module_path list -> unsafe_needs -> std_ppcmds;
-  pp_sig : ml_signature -> std_ppcmds; 
-
-  (* for an isolated declaration print *)
-  pp_decl : ml_decl -> std_ppcmds; 
-
-}  
diff --git a/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml
deleted file mode 100644
index 4e2904ba..00000000
--- a/contrib/extraction/mlutil.ml
+++ /dev/null
@@ -1,1167 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(*i $Id: mlutil.ml 13202 2010-06-25 22:36:30Z letouzey $ i*)
-
-(*i*)
-open Pp
-open Util
-open Names
-open Libnames
-open Nametab
-open Table
-open Miniml
-(*i*)
-
-(*s Exceptions. *)
-
-exception Found
-exception Impossible
-
-(*S Names operations. *)
-
-let anonymous = id_of_string "x"
-let dummy_name = id_of_string "_"
-
-let id_of_name = function
-  | Anonymous -> anonymous
-  | Name id when id = dummy_name -> anonymous
-  | Name id -> id 
-
-(*S Operations upon ML types (with meta). *)
-
-let meta_count = ref 0 
-		     
-let reset_meta_count () = meta_count := 0
-			      
-let new_meta _ = 
-  incr meta_count; 
-  Tmeta {id = !meta_count; contents = None}
-
-(*s Sustitution of [Tvar i] by [t] in a ML type. *)
-
-let type_subst i t0 t = 
-  let rec subst t = match t with
-    | Tvar j when i = j -> t0
-    | Tmeta {contents=None} -> t 
-    | Tmeta {contents=Some u} -> subst u
-    | Tarr (a,b) -> Tarr (subst a, subst b)
-    | Tglob (r, l) -> Tglob (r, List.map subst l)
-    | a -> a 
-  in subst t
-       
-(* Simultaneous substitution of [[Tvar 1; ... ; Tvar n]] by [l] in a ML type. *)
-
-let type_subst_list l t = 
-  let rec subst t = match t with 
-    | Tvar j -> List.nth l (j-1)
-    | Tmeta {contents=None} -> t
-    | Tmeta {contents=Some u} -> subst u
-    | Tarr (a,b) -> Tarr (subst a, subst b)
-    | Tglob (r, l) -> Tglob (r, List.map subst l)
-    | a -> a
-  in subst t
-
-(* Simultaneous substitution of [[|Tvar 1; ... ; Tvar n|]] by [v] in a ML type. *)
-
-let type_subst_vect v t = 
-  let rec subst t = match t with 
-    | Tvar j -> v.(j-1)
-    | Tmeta {contents=None} -> t
-    | Tmeta {contents=Some u} -> subst u
-    | Tarr (a,b) -> Tarr (subst a, subst b)
-    | Tglob (r, l) -> Tglob (r, List.map subst l)
-    | a -> a
-  in subst t
-
-(*s From a type schema to a type. All [Tvar] become fresh [Tmeta]. *)
-
-let instantiation (nb,t) = type_subst_vect (Array.init nb new_meta) t
-
-(*s Occur-check of a free meta in a type *)
-
-let rec type_occurs alpha t =
-  match t with
-  | Tmeta {id=beta; contents=None} -> alpha = beta
-  | Tmeta {contents=Some u} -> type_occurs alpha u
-  | Tarr (t1, t2) -> type_occurs alpha t1 || type_occurs alpha t2
-  | Tglob (r,l) -> List.exists (type_occurs alpha) l  
-  | _ -> false
-
-(*s Most General Unificator *)
-
-let rec mgu = function
-  | Tmeta m, Tmeta m' when m.id = m'.id -> ()
-  | Tmeta m, t when m.contents=None -> 
-      if type_occurs m.id t then raise Impossible
-      else m.contents <- Some t
-  | t, Tmeta m when m.contents=None -> 
-      if type_occurs m.id t then raise Impossible
-      else m.contents <- Some t
-  | Tmeta {contents=Some u}, t -> mgu (u, t)
-  | t, Tmeta {contents=Some u} -> mgu (t, u)
-  | Tarr(a, b), Tarr(a', b') ->
-      mgu (a, a'); mgu (b, b')
-  | Tglob (r,l), Tglob (r',l') when r = r' ->
-       List.iter mgu (List.combine l l')
-  | Tvar i, Tvar j when i = j -> ()
-  | Tvar' i, Tvar' j when i = j -> ()
-  | Tdummy _, Tdummy _ -> ()
-  | Tunknown, Tunknown -> ()
-  | _ -> raise Impossible
-
-let needs_magic p = try mgu p; false with Impossible -> true
-
-let put_magic_if b a = if b && lang () <> Scheme then MLmagic a else a
-
-let put_magic p a = if needs_magic p && lang () <> Scheme then MLmagic a else a
-
-
-(*S ML type env. *)
-
-module Mlenv = struct 
-  
-  let meta_cmp m m' = compare m.id m'.id 
-  module Metaset = Set.Make(struct type t = ml_meta let compare = meta_cmp end)
-
-  (* Main MLenv type. [env] is the real environment, whereas [free] 
-     (tries to) record the free meta variables occurring in [env]. *)
-
-  type t = { env : ml_schema list; mutable free : Metaset.t}
-
-  (* Empty environment. *)
-
-  let empty = { env = []; free = Metaset.empty }
-
-  (* [get] returns a instantiated copy of the n-th most recently added 
-     type in the environment. *)
-
-  let get mle n = 
-    assert (List.length mle.env >= n); 
-    instantiation (List.nth mle.env (n-1))
-
-  (* [find_free] finds the free meta in a type. *) 
-
-  let rec find_free set = function 
-    | Tmeta m when m.contents = None -> Metaset.add m set
-    | Tmeta {contents = Some t} -> find_free set t
-    | Tarr (a,b) -> find_free (find_free set a) b
-    | Tglob (_,l) -> List.fold_left find_free set l
-    | _ -> set
-
-  (* The [free] set of an environment can be outdate after 
-     some unifications. [clean_free] takes care of that. *) 
-			
-  let clean_free mle = 
-    let rem = ref Metaset.empty 
-    and add = ref Metaset.empty in 
-    let clean m = match m.contents with 
-      | None -> () 
-      | Some u -> rem := Metaset.add m !rem; add := find_free !add u
-    in 
-    Metaset.iter clean mle.free; 
-    mle.free <- Metaset.union (Metaset.diff mle.free !rem) !add
-
-  (* From a type to a type schema. If a [Tmeta] is still uninstantiated
-     and does appears in the [mle], then it becomes a [Tvar]. *)
-
-  let generalization mle t = 
-    let c = ref 0 in 
-    let map = ref (Intmap.empty : int Intmap.t) in 
-    let add_new i = incr c; map := Intmap.add i !c !map; !c in 
-    let rec meta2var t = match t with 
-      | Tmeta {contents=Some u} -> meta2var u 
-      | Tmeta ({id=i} as m) -> 
-	  (try Tvar (Intmap.find i !map) 
-	   with Not_found ->  
-	     if Metaset.mem m mle.free then t 
-	     else Tvar (add_new i))
-      | Tarr (t1,t2) -> Tarr (meta2var t1, meta2var t2)
-      | Tglob (r,l) -> Tglob (r, List.map meta2var l) 
-      | t -> t 
-    in !c, meta2var t
-	
-  (* Adding a type in an environment, after generalizing. *)
-
-  let push_gen mle t = 
-    clean_free mle; 
-    { env = generalization mle t :: mle.env; free = mle.free }
-
-  (* Adding a type with no [Tvar], hence no generalization needed. *)
-
-  let push_type {env=e;free=f} t = 
-    { env = (0,t) :: e; free = find_free f t} 
-    
-  (* Adding a type with no [Tvar] nor [Tmeta]. *)
-
-  let push_std_type {env=e;free=f} t = 
-    { env = (0,t) :: e; free = f}
-
-end
-
-(*S Operations upon ML types (without meta). *)
-
-(*s Does a section path occur in a ML type ? *)
-
-let rec type_mem_kn kn = function 
-  | Tmeta {contents = Some t} -> type_mem_kn kn t
-  | Tglob (r,l) -> occur_kn_in_ref kn r || List.exists (type_mem_kn kn) l
-  | Tarr (a,b) -> (type_mem_kn kn a) || (type_mem_kn kn b)
-  | _ -> false
-
-(*s Greatest variable occurring in [t]. *)
-
-let type_maxvar t = 
-  let rec parse n = function 
-    | Tmeta {contents = Some t} -> parse n t
-    | Tvar i -> max i n 
-    | Tarr (a,b) -> parse (parse n a) b
-    | Tglob (_,l) -> List.fold_left parse n l 
-    | _ -> n 
-  in parse 0 t
-
-(*s From [a -> b -> c] to [[a;b],c]. *) 
-
-let rec type_decomp = function 
-  | Tmeta {contents = Some t} -> type_decomp t 
-  | Tarr (a,b) -> let l,h = type_decomp b in a::l, h 
-  | a -> [],a
-
-(*s The converse: From [[a;b],c] to [a -> b -> c]. *)
-
-let rec type_recomp (l,t) = match l with 
-  | [] -> t 
-  | a::l -> Tarr (a, type_recomp (l,t))
-
-(*s Translating [Tvar] to [Tvar'] to avoid clash. *)
-
-let rec var2var' = function 
-  | Tmeta {contents = Some t} -> var2var' t
-  | Tvar i -> Tvar' i
-  | Tarr (a,b) -> Tarr (var2var' a, var2var' b)
-  | Tglob (r,l) -> Tglob (r, List.map var2var' l)
-  | a -> a
-
-type abbrev_map = global_reference -> ml_type option
-
-(*s Delta-reduction of type constants everywhere in a ML type [t].
-   [env] is a function of type [ml_type_env]. *)
-
-let type_expand env t = 
-  let rec expand = function
-    | Tmeta {contents = Some t} -> expand t
-    | Tglob (r,l) ->    
-	(match env r with 
-	   | Some mlt -> expand (type_subst_list l mlt) 
-	   | None -> Tglob (r, List.map expand l))
-    | Tarr (a,b) -> Tarr (expand a, expand b)
-    | a -> a
-  in if Table.type_expand () then expand t else t
-
-(*s Idem, but only at the top level of implications. *)
-
-let is_arrow = function Tarr _ -> true | _ -> false
-
-let type_weak_expand env t = 
-  let rec expand = function
-    | Tmeta {contents = Some t} -> expand t
-    | Tglob (r,l) as t ->    
-	(match env r with 
-	   | Some mlt -> 
-	       let u = expand (type_subst_list l mlt) in 
-	       if is_arrow u then u else t
-	   | None -> t)
-    | Tarr (a,b) -> Tarr (a, expand b)
-    | a -> a
-  in expand t
-
-(*s Generating a signature from a ML type. *)
-
-let type_to_sign env t = match type_expand env t with 
-  | Tdummy d -> Kill d 
-  | _ -> Keep
-
-let type_to_signature env t = 
-  let rec f = function 
-    | Tmeta {contents = Some t} -> f t 
-    | Tarr (Tdummy d, b) -> Kill d :: f b
-    | Tarr (_, b) -> Keep :: f b
-    | _ -> [] 
-  in f (type_expand env t)
-
-let isKill = function Kill _ -> true | _ -> false
-
-let isDummy = function Tdummy _ -> true | _ -> false
-
-let sign_of_id i = if i = dummy_name then Kill Kother else Keep
-
-(*s Removing [Tdummy] from the top level of a ML type. *)
-
-let type_expunge env t = 
-  let s = type_to_signature env t in 
-  if s = [] then t 
-  else if List.mem Keep s then 
-    let rec f t s = 
-      if List.exists isKill s then 
-	match t with 
-	  | Tmeta {contents = Some t} -> f t s
-	  | Tarr (a,b) -> 
-	      let t = f b (List.tl s) in 
-	      if List.hd s = Keep then Tarr (a, t) else t  
-	  | Tglob (r,l) ->
-	      (match env r with 
-		 | Some mlt -> f (type_subst_list l mlt) s
-		 | None -> assert false)
-	  | _ -> assert false
-      else t 
-    in f t s 
-  else if List.mem (Kill Kother) s then 
-    Tarr (Tdummy Kother, snd (type_decomp (type_weak_expand env t))) 
-  else snd (type_decomp (type_weak_expand env t))
-
-(*S Generic functions over ML ast terms. *)
-
-(*s [ast_iter_rel f t] applies [f] on every [MLrel] in t. It takes care 
-   of the number of bingings crossed before reaching the [MLrel]. *)
-
-let ast_iter_rel f = 
-  let rec iter n = function
-    | MLrel i -> f (i-n)
-    | MLlam (_,a) -> iter (n+1) a
-    | MLletin (_,a,b) -> iter n a; iter (n+1) b
-    | MLcase (_,a,v) ->
-	iter n a; Array.iter (fun (_,l,t) -> iter (n + (List.length l)) t) v
-    | MLfix (_,ids,v) -> let k = Array.length ids in Array.iter (iter (n+k)) v
-    | MLapp (a,l) -> iter n a; List.iter (iter n) l
-    | MLcons (_,_,l) ->  List.iter (iter n) l
-    | MLmagic a -> iter n a
-    | MLglob _ | MLexn _ | MLdummy | MLaxiom -> ()
-  in iter 0 
-
-(*s Map over asts. *)
-
-let ast_map_case f (c,ids,a) = (c,ids,f a)
-
-let ast_map f = function
-  | MLlam (i,a) -> MLlam (i, f a)
-  | MLletin (i,a,b) -> MLletin (i, f a, f b)
-  | MLcase (i,a,v) -> MLcase (i,f a, Array.map (ast_map_case f) v)
-  | MLfix (i,ids,v) -> MLfix (i, ids, Array.map f v)
-  | MLapp (a,l) -> MLapp (f a, List.map f l)
-  | MLcons (i,c,l) -> MLcons (i,c, List.map f l)
-  | MLmagic a -> MLmagic (f a)
-  | MLrel _ | MLglob _ | MLexn _ | MLdummy | MLaxiom as a -> a
-
-(*s Map over asts, with binding depth as parameter. *)
-
-let ast_map_lift_case f n (c,ids,a) = (c,ids, f (n+(List.length ids)) a)
-
-let ast_map_lift f n = function 
-  | MLlam (i,a) -> MLlam (i, f (n+1) a)
-  | MLletin (i,a,b) -> MLletin (i, f n a, f (n+1) b)
-  | MLcase (i,a,v) -> MLcase (i,f n a,Array.map (ast_map_lift_case f n) v)
-  | MLfix (i,ids,v) -> 
-      let k = Array.length ids in MLfix (i,ids,Array.map (f (k+n)) v)
-  | MLapp (a,l) -> MLapp (f n a, List.map (f n) l)
-  | MLcons (i,c,l) -> MLcons (i,c, List.map (f n) l)
-  | MLmagic a -> MLmagic (f n a)
-  | MLrel _ | MLglob _ | MLexn _ | MLdummy | MLaxiom as a -> a	
-
-(*s Iter over asts. *) 
-
-let ast_iter_case f (c,ids,a) = f a
-
-let ast_iter f = function
-  | MLlam (i,a) -> f a
-  | MLletin (i,a,b) -> f a; f b
-  | MLcase (_,a,v) -> f a; Array.iter (ast_iter_case f) v
-  | MLfix (i,ids,v) -> Array.iter f v
-  | MLapp (a,l) -> f a; List.iter f l
-  | MLcons (_,c,l) -> List.iter f l
-  | MLmagic a -> f a
-  | MLrel _ | MLglob _ | MLexn _ | MLdummy | MLaxiom  -> ()
-
-(*S Operations concerning De Bruijn indices. *)
-
-(*s [ast_occurs k t] returns [true] if [(Rel k)] occurs in [t]. *)
-
-let ast_occurs k t = 
-  try 
-    ast_iter_rel (fun i -> if i = k then raise Found) t; false 
-  with Found -> true
-
-(*s [occurs_itvl k k' t] returns [true] if there is a [(Rel i)] 
-   in [t] with [k<=i<=k'] *)
-
-let ast_occurs_itvl k k' t = 
-  try 
-    ast_iter_rel (fun i -> if (k <= i) && (i <= k') then raise Found) t; false 
-  with Found -> true
-
-(*s Number of occurences of [Rel k] and [Rel 1] in [t]. *)
-
-let nb_occur_k k t =
-  let cpt = ref 0 in 
-  ast_iter_rel (fun i -> if i = k then incr cpt) t;
-  !cpt
-
-let nb_occur t = nb_occur_k 1 t
-
-(* Number of occurences of [Rel 1] in [t], with special treatment of match:
-   occurences in different branches aren't added, but we rather use max. *)
-
-let nb_occur_match = 
-  let rec nb k = function 
-    | MLrel i -> if i = k then 1 else 0
-    | MLcase(_,a,v) -> 
-        (nb k a) +
-	Array.fold_left 
-	  (fun r (_,ids,a) -> max r (nb (k+(List.length ids)) a)) 0 v
-    | MLletin (_,a,b) -> (nb k a) + (nb (k+1) b) 
-    | MLfix (_,ids,v) -> let k = k+(Array.length ids) in 
-      Array.fold_left (fun r a -> r+(nb k a)) 0 v
-    | MLlam (_,a) -> nb (k+1) a
-    | MLapp (a,l) -> List.fold_left (fun r a -> r+(nb k a)) (nb k a) l
-    | MLcons (_,_,l) -> List.fold_left (fun r a -> r+(nb k a)) 0 l 
-    | MLmagic a -> nb k a
-    | MLglob _ | MLexn _ | MLdummy | MLaxiom -> 0
-  in nb 1
-
-(*s Lifting on terms.
-    [ast_lift k t] lifts the binding depth of [t] across [k] bindings. *)
-
-let ast_lift k t = 
-  let rec liftrec n = function
-    | MLrel i as a -> if i-n < 1 then a else MLrel (i+k)
-    | a -> ast_map_lift liftrec n a
-  in if k = 0 then t else liftrec 0 t
-
-let ast_pop t = ast_lift (-1) t
-
-(*s [permut_rels k k' c] translates [Rel 1 ... Rel k] to [Rel (k'+1) ... 
-  Rel (k'+k)] and [Rel (k+1) ... Rel (k+k')] to [Rel 1 ... Rel k'] *)
-
-let permut_rels k k' = 
-  let rec permut n = function
-    | MLrel i as a ->
-	let i' = i-n in
-	if i'<1 || i'>k+k' then a 
-	else if i'<=k then MLrel (i+k')
-	else MLrel (i-k)
-    | a -> ast_map_lift permut n a
-  in permut 0  
-
-(*s Substitution. [ml_subst e t] substitutes [e] for [Rel 1] in [t]. 
-    Lifting (of one binder) is done at the same time. *)
-
-let ast_subst e =
-  let rec subst n = function
-    | MLrel i as a ->
-	let i' = i-n in 
-	if i'=1 then ast_lift n e
-	else if i'<1 then a 
-	else MLrel (i-1)
-    | a -> ast_map_lift subst n a
-  in subst 0
-
-(*s Generalized substitution. 
-   [gen_subst v d t] applies to [t] the substitution coded in the 
-   [v] array: [(Rel i)] becomes [v.(i-1)]. [d] is the correction applies 
-   to [Rel] greater than [Array.length v]. *)
-
-let gen_subst v d t = 
-  let rec subst n = function
-    | MLrel i as a -> 
-	let i'= i-n in 
-	if i' < 1 then a 
-	else if i' <= Array.length v then 
-	  ast_lift n v.(i'-1) 
-	else MLrel (i+d) 
-    | a -> ast_map_lift subst n a
-  in subst 0 t
-
-(*S Operations concerning lambdas. *)
-
-(*s [collect_lams MLlam(id1,...MLlam(idn,t)...)] returns
-    [[idn;...;id1]] and the term [t]. *)
-
-let collect_lams = 
-  let rec collect acc = function
-    | MLlam(id,t) -> collect (id::acc) t
-    | x           -> acc,x
-  in collect []
-
-(*s [collect_n_lams] does the same for a precise number of [MLlam]. *)
-
-let collect_n_lams = 
-  let rec collect acc n t = 
-    if n = 0 then acc,t 
-    else match t with 
-      | MLlam(id,t) -> collect (id::acc) (n-1) t
-      | _ -> assert false
-  in collect [] 
-
-(*s [remove_n_lams] just removes some [MLlam]. *)
-
-let rec remove_n_lams n t = 
-  if n = 0 then t  
-  else match t with 
-      | MLlam(_,t) -> remove_n_lams (n-1) t
-      | _ -> assert false
-
-(*s [nb_lams] gives the number of head [MLlam]. *)
-
-let rec nb_lams = function 
-  | MLlam(_,t) -> succ (nb_lams t)
-  | _ -> 0 
-
-(*s [named_lams] does the converse of [collect_lams]. *)
-
-let rec named_lams ids a = match ids with 
-  | [] -> a 
-  | id :: ids -> named_lams ids (MLlam (id,a))
-
-(*s The same in anonymous version. *)
-
-let rec anonym_lams a = function 
-  | 0 -> a 
-  | n -> anonym_lams (MLlam (anonymous,a)) (pred n)
-
-(*s Idem for [dummy_name]. *)
-
-let rec dummy_lams a = function 
-  | 0 -> a 
-  | n -> dummy_lams (MLlam (dummy_name,a)) (pred n)
-
-(*s mixed according to a signature. *)
-
-let rec anonym_or_dummy_lams a = function 
-  | [] -> a 
-  | Keep :: s -> MLlam(anonymous, anonym_or_dummy_lams a s)
-  | Kill _ :: s -> MLlam(dummy_name, anonym_or_dummy_lams a s)
-
-(*S Operations concerning eta. *)
-
-(*s The following function creates [MLrel n;...;MLrel 1] *)
-
-let rec eta_args n = 
-  if n = 0 then [] else (MLrel n)::(eta_args (pred n))
-
-(*s Same, but filtered by a signature. *)
-
-let rec eta_args_sign n = function 
-  | [] -> [] 
-  | Keep :: s -> (MLrel n) :: (eta_args_sign (n-1) s) 
-  | Kill _ :: s -> eta_args_sign (n-1) s
-
-(*s This one tests [MLrel (n+k); ... ;MLrel (1+k)] *)
-
-let rec test_eta_args_lift k n = function 
-  | [] -> n=0
-  | a :: q -> (a = (MLrel (k+n))) && (test_eta_args_lift k (pred n) q)
-
-(*s Computes an eta-reduction. *)
-
-let eta_red e = 
-  let ids,t = collect_lams e in 
-  let n = List.length ids in
-  if n = 0 then e 
-  else match t with 
-    | MLapp (f,a) -> 
-	let m = List.length a in 
-	let ids,body,args = 
-	  if m = n then 
-	    [], f, a
-	  else if m < n then 
-	    list_skipn m ids, f, a
-	  else (* m > n *)
-	    let a1,a2 = list_chop (m-n) a in 
-	    [], MLapp (f,a1), a2
-	in 
-	let p = List.length args in  
-	if test_eta_args_lift 0 p args && not (ast_occurs_itvl 1 p body)
-	then named_lams ids (ast_lift (-p) body)
-	else e
-    | _ -> e
-
-(*s Computes all head linear beta-reductions possible in [(t a)].
-  Non-linear head beta-redex become let-in. *)
-
-let rec linear_beta_red a t = match a,t with  
-  | [], _ -> t 
-  | a0::a, MLlam (id,t) ->
-      (match nb_occur_match t with
-	 | 0 -> linear_beta_red a (ast_pop t)
-	 | 1 -> linear_beta_red a (ast_subst a0 t)
-	 | _ -> 
-	     let a = List.map (ast_lift 1) a in 
-	     MLletin (id, a0, linear_beta_red a t))
-  | _ -> MLapp (t, a)
-
-(*s Applies a substitution [s] of constants by their body, plus 
-  linear beta reductions at modified positions. *)  
-
-let rec ast_glob_subst s t = match t with 
-  | MLapp ((MLglob ((ConstRef kn) as refe)) as f, a) -> 
-      let a = List.map (ast_glob_subst s) a in 
-      (try linear_beta_red a (Refmap.find refe s) 
-       with Not_found -> MLapp (f, a))
-  | MLglob ((ConstRef kn) as refe) ->
-      (try Refmap.find refe s with Not_found -> t)
-  | _ -> ast_map (ast_glob_subst s) t
-
-
-(*S Auxiliary functions used in simplification of ML cases. *)
-
-(*s [check_and_generalize (r0,l,c)] transforms any [MLcons(r0,l)] in [MLrel 1]
-  and raises [Impossible] if any variable in [l] occurs outside such a 
-  [MLcons] *)
-
-let check_and_generalize (r0,l,c) = 
-  let nargs = List.length l in 
-  let rec genrec n = function 
-    | MLrel i as c -> 
-	let i' = i-n in 
-	if i'<1 then c 
-	else if i'>nargs then MLrel (i-nargs+1) 
-	else raise Impossible
-    | MLcons(_,r,args) when r=r0 && (test_eta_args_lift n nargs args) -> 
-	MLrel (n+1) 
-    | a -> ast_map_lift genrec n a
-  in genrec 0 c  
-
-(*s [check_generalizable_case] checks if all branches can be seen as the 
-  same function [f] applied to the term matched. It is a generalized version 
-  of the identity case optimization. *)
-
-(* CAVEAT: this optimization breaks typing in some special case. example: 
-   [type 'x a = A]. Then [let f = function A -> A] has type ['x a -> 'y a],
-   which is incompatible with the type of [let f x = x].
-   By default, we brutally disable this optim except for some known types: 
-   [bool], [sumbool], [sumor] *)
-
-let generalizable_list = 
-  let datatypes = MPfile (dirpath_of_string "Coq.Init.Datatypes")
-  and specif = MPfile (dirpath_of_string "Coq.Init.Specif")
-  in 
-  [ make_kn datatypes empty_dirpath (mk_label "bool"); 
-    make_kn specif empty_dirpath (mk_label "sumbool");
-    make_kn specif empty_dirpath (mk_label "sumor") ]
-
-let check_generalizable_case unsafe br = 
-  if not unsafe then 
-    (match br.(0) with 
-     | ConstructRef ((kn,_),_), _, _ ->
-	 if not (List.mem kn generalizable_list) then raise Impossible
-     | _ -> assert false); 
-  let f = check_and_generalize br.(0) in 
-  for i = 1 to Array.length br - 1 do 
-    if check_and_generalize br.(i) <> f then raise Impossible 
-  done; f
-
-(*s Detecting similar branches of a match *)
-
-(* If several branches of a match are equal (and independent from their 
-   patterns) we will print them using a _ pattern. If _all_ branches 
-   are equal, we remove the match.
-*)
-
-let common_branches br = 
-  let tab = Hashtbl.create 13 in 
-  for i = 0 to Array.length br - 1 do 
-    let (r,ids,t) = br.(i) in 
-    let n = List.length ids in 
-    if not (ast_occurs_itvl 1 n t) then 
-       let t = ast_lift (-n) t in 
-       let l = try Hashtbl.find tab t with Not_found -> [] in 
-       Hashtbl.replace tab t (i::l)
-  done; 
-  let best = ref [] in 
-  Hashtbl.iter 
-    (fun _ l -> if List.length l > List.length !best then best := l) tab; 
-  if List.length !best < 2 then [] else !best
-
-(*s If all branches are functions, try to permut the case and the functions. *)
-
-let rec merge_ids ids ids' = match ids,ids' with 
-  | [],l -> l 
-  | l,[] -> l
-  | i::ids, i'::ids' -> 
-      (if i = dummy_name then i' else i) :: (merge_ids ids ids')
-
-let is_exn = function MLexn _ -> true | _ -> false
-
-let rec permut_case_fun br acc = 
-  let nb = ref max_int in 
-  Array.iter (fun (_,_,t) -> 
-		let ids, c = collect_lams t in 
-		let n = List.length ids in 
-		if (n < !nb) && (not (is_exn c)) then nb := n) br; 
-  if !nb = max_int || !nb = 0 then ([],br) 
-  else begin
-    let br = Array.copy br in 
-    let ids = ref [] in  
-    for i = 0 to Array.length br - 1 do 
-      let (r,l,t) = br.(i) in 
-      let local_nb = nb_lams t in 
-      if local_nb < !nb then (* t = MLexn ... *)
-	br.(i) <- (r,l,remove_n_lams local_nb t)
-      else begin
-	let local_ids,t = collect_n_lams !nb t in 
-	ids := merge_ids !ids local_ids; 
-	br.(i) <- (r,l,permut_rels !nb (List.length l) t)
-      end
-    done; 
-    (!ids,br)
-  end
-  
-(*S Generalized iota-reduction. *)
-
-(* Definition of a generalized iota-redex: it's a [MLcase(e,_)] 
-   with [(is_iota_gen e)=true]. Any generalized iota-redex is 
-   transformed into beta-redexes. *)
-
-let rec is_iota_gen = function 
-  | MLcons _ -> true
-  | MLcase(_,_,br)-> array_for_all (fun (_,_,t)->is_iota_gen t) br
-  | _ -> false
-
-let constructor_index = function
-  | ConstructRef (_,j) -> pred j
-  | _ -> assert false
-
-let iota_gen br = 
-  let rec iota k = function 
-    | MLcons (i,r,a) ->
-	let (_,ids,c) = br.(constructor_index r) in
-	let c = List.fold_right (fun id t -> MLlam (id,t)) ids c in
-	let c = ast_lift k c in 
-	MLapp (c,a)
-    | MLcase(i,e,br') -> 
-	let new_br = 
-	  Array.map (fun (n,i,c)->(n,i,iota (k+(List.length i)) c)) br'
-	in MLcase(i,e, new_br)
-    | _ -> assert false
-  in iota 0 
-
-let is_atomic = function 
-  | MLrel _ | MLglob _ | MLexn _ | MLdummy -> true
-  | _ -> false
-
-(*S The main simplification function. *)
-
-(* Some beta-iota reductions + simplifications. *)
-
-let rec simpl o = function
-  | MLapp (f, []) ->
-      simpl o f
-  | MLapp (f, a) -> 
-      simpl_app o (List.map (simpl o) a) (simpl o f)
-  | MLcase (i,e,br) ->
-      let br = Array.map (fun (n,l,t) -> (n,l,simpl o t)) br in 
-      simpl_case o i br (simpl o e) 
-  | MLletin(id,c,e) -> 
-      let e = (simpl o e) in 
-      if 
-	(id = dummy_name) || (is_atomic c) || (is_atomic e) ||
-	(let n = nb_occur_match e in n = 0 || (n=1 && o.opt_lin_let))
-      then 
-	simpl o (ast_subst c e)
-      else 
-	MLletin(id, simpl o c, e)
-  | MLfix(i,ids,c) -> 
-      let n = Array.length ids in 
-      if ast_occurs_itvl 1 n c.(i) then 
-	MLfix (i, ids, Array.map (simpl o) c)
-      else simpl o (ast_lift (-n) c.(i)) (* Dummy fixpoint *)
-  | a -> ast_map (simpl o) a 
-
-and simpl_app o a = function  
-  | MLapp (f',a') -> simpl_app o (a'@a) f'
-  | MLlam (id,t) when id = dummy_name -> 
-      simpl o (MLapp (ast_pop t, List.tl a))
-  | MLlam (id,t) -> (* Beta redex *)
-      (match nb_occur_match t with
-	 | 0 -> simpl o (MLapp (ast_pop t, List.tl a))
-	 | 1 when o.opt_lin_beta -> 
-	     simpl o (MLapp (ast_subst (List.hd a) t, List.tl a))
-	 | _ -> 
-	     let a' = List.map (ast_lift 1) (List.tl a) in
-	     simpl o (MLletin (id, List.hd a, MLapp (t, a'))))
-  | MLletin (id,e1,e2) when o.opt_let_app -> 
-      (* Application of a letin: we push arguments inside *)
-      MLletin (id, e1, simpl o (MLapp (e2, List.map (ast_lift 1) a)))
-  | MLcase (i,e,br) when o.opt_case_app -> 
-      (* Application of a case: we push arguments inside *)
-      let br' = 
-	Array.map 
-      	  (fun (n,l,t) -> 
-	     let k = List.length l in
-	     let a' = List.map (ast_lift k) a in
-      	     (n, l, simpl o (MLapp (t,a')))) br 
-      in simpl o (MLcase (i,e,br')) 
-  | (MLdummy | MLexn _) as e -> e 
-	(* We just discard arguments in those cases. *)
-  | f -> MLapp (f,a)
-
-and simpl_case o i br e = 
-  if o.opt_case_iot && (is_iota_gen e) then (* Generalized iota-redex *)
-    simpl o (iota_gen br e)
-  else 
-    try (* Does a term [f] exist such that each branch is [(f e)] ? *)
-      if not o.opt_case_idr then raise Impossible;
-      let f = check_generalizable_case o.opt_case_idg br in 
-      simpl o (MLapp (MLlam (anonymous,f),[e]))
-    with Impossible -> 
-      (* Detect common branches *)
-      let common_br = if not o.opt_case_cst then [] else common_branches br in
-      if List.length common_br = Array.length br && br <> [||] then 
-	let (_,ids,t) = br.(0) in ast_lift (-List.length ids) t
-      else 
-	let new_i = (fst i, common_br) in 
-	(* Swap the case and the lam if possible *)
-	if o.opt_case_fun 
-	then 
-	  let ids,br = permut_case_fun br [] in 
-	  let n = List.length ids in 
-	  if n <> 0 then named_lams ids (MLcase (new_i,ast_lift n e, br))
-	  else MLcase (new_i,e,br) 
-	else MLcase (new_i,e,br)
-
-let rec post_simpl = function 
-  | MLletin(_,c,e) when (is_atomic (eta_red c)) -> 
-      post_simpl (ast_subst (eta_red c) e)
-  | a -> ast_map post_simpl a 
-
-(*S Local prop elimination. *) 
-(* We try to eliminate as many [prop] as possible inside an [ml_ast]. *)
-
-(*s In a list, it selects only the elements corresponding to a [Keep] 
-   in the boolean list [l]. *)
-
-let rec select_via_bl l args = match l,args with 
-  | [],_ -> args
-  | Keep::l,a::args -> a :: (select_via_bl l args)
-  | Kill _::l,a::args -> select_via_bl l args
-  | _ -> assert false 
-
-(*s [kill_some_lams] removes some head lambdas according to the signature [bl].
-   This list is build on the identifier list model: outermost lambda
-   is on the right. 
-   [Rels] corresponding to removed lambdas are supposed not to occur, and 
-   the other [Rels] are made correct via a [gen_subst].
-   Output is not directly a [ml_ast], compose with [named_lams] if needed. *)
-
-let kill_some_lams bl (ids,c) =
-  let n = List.length bl in
-  let n' = List.fold_left (fun n b -> if b=Keep then (n+1) else n) 0 bl in 
-  if n = n' then ids,c
-  else if n' = 0 then [],ast_lift (-n) c 
-  else begin
-    let v = Array.make n MLdummy in 
-    let rec parse_ids i j = function 
-      | [] -> ()
-      | Keep :: l -> v.(i) <- MLrel j; parse_ids (i+1) (j+1) l
-      | Kill _ :: l -> parse_ids (i+1) j l
-    in parse_ids 0 1 bl ; 
-    select_via_bl bl ids, gen_subst v (n'-n) c
-  end
-
-(*s [kill_dummy_lams] uses the last function to kill the lambdas corresponding 
-  to a [dummy_name]. It can raise [Impossible] if there is nothing to do, or 
-  if there is no lambda left at all. *)
-
-let kill_dummy_lams c = 
-  let ids,c = collect_lams c in 
-  let bl = List.map sign_of_id ids in
-  if (List.mem Keep bl) && (List.exists isKill bl) then 
-    let ids',c = kill_some_lams bl (ids,c) in 
-    ids, named_lams ids' c
-  else raise Impossible
-
-(*s [eta_expansion_sign] takes a function [fun idn ... id1 -> c] 
-   and a signature [s] and builds a eta-long version. *)
-
-(* For example, if [s = [Keep;Keep;Kill Prop;Keep]] then the output is :
-   [fun idn ... id1 x x _ x -> (c' 4 3 __ 1)]  with [c' = lift 4 c] *)
-
-let eta_expansion_sign s (ids,c) =
-  let rec abs ids rels i = function
-    | [] -> 
-	let a = List.rev_map (function MLrel x -> MLrel (i-x) | a -> a) rels
-	in ids, MLapp (ast_lift (i-1) c, a) 
-    | Keep :: l -> abs (anonymous :: ids) (MLrel i :: rels) (i+1) l 
-    | Kill _ :: l -> abs (dummy_name :: ids) (MLdummy :: rels) (i+1) l
-  in abs ids [] 1 s
-
-(*s If [s = [b1; ... ; bn]] then [case_expunge] decomposes [e] 
-  in [n] lambdas (with eta-expansion if needed) and removes all dummy lambdas 
-  corresponding to [Del] in [s]. *)
-
-let case_expunge s e = 
-  let m = List.length s in 
-  let n = nb_lams e in 
-  let p = if m <= n then collect_n_lams m e 
-  else eta_expansion_sign (list_skipn n s) (collect_lams e) in 
-  kill_some_lams (List.rev s) p
-
-(*s [term_expunge] takes a function [fun idn ... id1 -> c] 
-  and a signature [s] and remove dummy lams. The difference 
-  with [case_expunge] is that we here leave one dummy lambda 
-  if all lambdas are logical dummy. *)
-
-let term_expunge s (ids,c) =
-  if s = [] then c 
-  else 
-    let ids,c = kill_some_lams (List.rev s) (ids,c) in 
-    if ids = [] && List.mem (Kill Kother) s then 
-      MLlam (dummy_name, ast_lift 1 c)
-    else named_lams ids c
-
-(*s [kill_dummy_args ids t0 t] looks for occurences of [t0] in [t] and 
-  purge the args of [t0] corresponding to a [dummy_name]. 
-  It makes eta-expansion if needed. *) 
-
-let kill_dummy_args ids t0 t =
-  let m = List.length ids in 
-  let bl = List.rev_map sign_of_id ids in
-  let rec killrec n = function 
-    | MLapp(e, a) when e = ast_lift n t0 -> 
-	let k = max 0 (m - (List.length a)) in 
-	let a = List.map (killrec n) a in  
-	let a = List.map (ast_lift k) a in 
-	let a = select_via_bl bl (a @ (eta_args k)) in 
-	named_lams (list_firstn k ids) (MLapp (ast_lift k e, a)) 
-    | e when e = ast_lift n t0 -> 
-	let a = select_via_bl bl (eta_args m) in 
-	named_lams ids (MLapp (ast_lift m e, a))
-    | e -> ast_map_lift killrec n e 
-  in killrec 0 t 
-
-(*s The main function for local [dummy] elimination. *)
-
-let rec kill_dummy = function 
-  | MLfix(i,fi,c) -> 
-      (try 
-	 let ids,c = kill_dummy_fix i fi c in 
-	 ast_subst (MLfix (i,fi,c)) (kill_dummy_args ids (MLrel 1) (MLrel 1))
-       with Impossible -> MLfix (i,fi,Array.map kill_dummy c))
-  | MLapp (MLfix (i,fi,c),a) -> 
-      (try 
-	 let ids,c = kill_dummy_fix i fi c in 
-	 let a = List.map (fun t -> ast_lift 1 (kill_dummy t)) a in 
-	 let e = kill_dummy_args ids (MLrel 1) (MLapp (MLrel 1,a)) in
-	 ast_subst (MLfix (i,fi,c)) e  
-       with Impossible -> 
-	 MLapp(MLfix(i,fi,Array.map kill_dummy c),List.map kill_dummy a))
-  | MLletin(id, MLfix (i,fi,c),e) -> 
-      (try 
-	 let ids,c = kill_dummy_fix i fi c in
-	 let e = kill_dummy (kill_dummy_args ids (MLrel 1) e) in 
-	 MLletin(id, MLfix(i,fi,c),e)
-      with Impossible -> 
-	MLletin(id, MLfix(i,fi,Array.map kill_dummy c),kill_dummy e))
-  | MLletin(id,c,e) -> 
-      (try 
-	 let ids,c = kill_dummy_lams c in 
-	 let e = kill_dummy_args ids (MLrel 1) e in 
-	 MLletin (id, kill_dummy c,kill_dummy e) 
-       with Impossible -> MLletin(id,kill_dummy c,kill_dummy e))
-  | a -> ast_map kill_dummy a
-
-and kill_dummy_fix i fi c = 
-  let n = Array.length fi in 
-  let ids,ci = kill_dummy_lams c.(i) in 
-  let c = Array.copy c in c.(i) <- ci; 
-  for j = 0 to (n-1) do 
-    c.(j) <- kill_dummy (kill_dummy_args ids (MLrel (n-i)) c.(j)) 
-  done;
-  ids,c
-
-(*s Putting things together. *)
-
-let normalize a = 
-  let o = optims () in 
-  let a = simpl o a in 
-  if o.opt_kill_dum then post_simpl (kill_dummy a) else a
-
-(*S Special treatment of fixpoint for pretty-printing purpose. *)
-
-let general_optimize_fix f ids n args m c = 
-  let v = Array.make n 0 in 
-  for i=0 to (n-1) do v.(i)<-i done;
-  let aux i = function 
-    | MLrel j when v.(j-1)>=0 -> 
-	if ast_occurs (j+1) c then raise Impossible else v.(j-1)<-(-i-1)
-    | _ -> raise Impossible
-  in list_iter_i aux args; 
-  let args_f = List.rev_map (fun i -> MLrel (i+m+1)) (Array.to_list v) in
-  let new_f = anonym_lams (MLapp (MLrel (n+m+1),args_f)) m in  
-  let new_c = named_lams ids (normalize (MLapp ((ast_subst new_f c),args))) in
-  MLfix(0,[|f|],[|new_c|])
-
-let optimize_fix a = 
-  if not (optims()).opt_fix_fun then a 
-  else
-    let ids,a' = collect_lams a in 
-    let n = List.length ids in 
-    if n = 0 then a 
-    else match a' with 
-      | MLfix(_,[|f|],[|c|]) ->
-	  let new_f = MLapp (MLrel (n+1),eta_args n) in 
-	  let new_c = named_lams ids (normalize (ast_subst new_f c))
-	  in MLfix(0,[|f|],[|new_c|])
-      | MLapp(a',args) ->
-	  let m = List.length args in 
-	  (match a' with 
-	     | MLfix(_,_,_) when 
-		 (test_eta_args_lift 0 n args) && not (ast_occurs_itvl 1 m a') 
-		 -> a'
-	     | MLfix(_,[|f|],[|c|]) -> 
-		 (try general_optimize_fix f ids n args m c
-		  with Impossible -> a)
-	     | _ -> a)
-      | _ -> a
-
-(*S Inlining. *)
-
-(* Utility functions used in the decision of inlining. *)
-
-let rec ml_size = function
-  | MLapp(t,l) -> List.length l + ml_size t + ml_size_list l
-  | MLlam(_,t) -> 1 + ml_size t
-  | MLcons(_,_,l) -> ml_size_list l
-  | MLcase(_,t,pv) -> 
-      1 + ml_size t + (Array.fold_right (fun (_,_,t) a -> a + ml_size t) pv 0)
-  | MLfix(_,_,f) -> ml_size_array f
-  | MLletin (_,_,t) -> ml_size t
-  | MLmagic t -> ml_size t
-  | _ -> 0
-
-and ml_size_list l = List.fold_left (fun a t -> a + ml_size t) 0 l
-
-and ml_size_array l = Array.fold_left (fun a t -> a + ml_size t) 0 l
-
-let is_fix = function MLfix _ -> true | _ -> false
-
-let rec is_constr = function
-  | MLcons _   -> true
-  | MLlam(_,t) -> is_constr t
-  | _          -> false
-
-(*s Strictness *)
-
-(* A variable is strict if the evaluation of the whole term implies
-   the evaluation of this variable. Non-strict variables can be found 
-   behind Match, for example. Expanding a term [t] is a good idea when 
-   it begins by at least one non-strict lambda, since the corresponding 
-   argument to [t] might be unevaluated in the expanded code. *)
-
-exception Toplevel
-
-let lift n l = List.map ((+) n) l
-
-let pop n l = List.map (fun x -> if x<=n then raise Toplevel else x-n) l 
-
-(* This function returns a list of de Bruijn indices of non-strict variables,
-   or raises [Toplevel] if it has an internal non-strict variable. 
-   In fact, not all variables are checked for strictness, only the ones which 
-   de Bruijn index is in the candidates list [cand]. The flag [add] controls 
-   the behaviour when going through a lambda: should we add the corresponding 
-   variable to the candidates?  We use this flag to check only the external 
-   lambdas, those that will correspond to arguments. *)
-
-let rec non_stricts add cand = function 
-  | MLlam (id,t) -> 
-      let cand = lift 1 cand in
-      let cand = if add then 1::cand else cand in
-      pop 1 (non_stricts add cand t)
-  | MLrel n -> 
-      List.filter ((<>) n) cand  
-  | MLapp (MLrel n, _) -> 
-      List.filter ((<>) n) cand
-	(* In [(x y)] we say that only x is strict. Cf [sig_rec]. We may *)
-	(* gain something if x is replaced by a function like a projection *)
-  | MLapp (t,l)-> 
-      let cand = non_stricts false cand t in 
-      List.fold_left (non_stricts false) cand l 
-  | MLcons (_,_,l) -> 
-      List.fold_left (non_stricts false) cand l
-  | MLletin (_,t1,t2) -> 
-      let cand = non_stricts false cand t1 in 
-      pop 1 (non_stricts add (lift 1 cand) t2)
-  | MLfix (_,i,f)-> 
-      let n = Array.length i in
-      let cand = lift n cand in 
-      let cand = Array.fold_left (non_stricts false) cand f in 
-      pop n cand
-  | MLcase (_,t,v) -> 
-      (* The only interesting case: for a variable to be non-strict, *)
-      (* it is sufficient that it appears non-strict in at least one branch, *)
-      (* so we make an union (in fact a merge). *)
-      let cand = non_stricts false cand t in 
-      Array.fold_left 
-	(fun c (_,i,t)-> 
-	   let n = List.length i in 
-	   let cand = lift n cand in 
-	   let cand = pop n (non_stricts add cand t) in
-	   Sort.merge (<=) cand c) [] v
-	(* [merge] may duplicates some indices, but I don't mind. *)
-  | MLmagic t -> 
-      non_stricts add cand t
-  | _ -> 
-      cand
-
-(* The real test: we are looking for internal non-strict variables, so we start
-   with no candidates, and the only positive answer is via the [Toplevel] 
-   exception. *)
-
-let is_not_strict t = 
-  try let _ = non_stricts true [] t in false
-  with Toplevel -> true
-
-(*s Inlining decision *)
-
-(* [inline_test] answers the following question: 
-   If we could inline [t] (the user said nothing special), 
-   should we inline ? 
-   
-   We expand small terms with at least one non-strict 
-   variable (i.e. a variable that may not be evaluated).
-   
-   Futhermore we don't expand fixpoints. *)
-
-let inline_test t = 
-  let t1 = eta_red t in 
-  let t2 = snd (collect_lams t1) in
-  not (is_fix t2) && ml_size t < 12 && is_not_strict t
-
-let manual_inline_list = 
-  let mp = MPfile (dirpath_of_string "Coq.Init.Wf") in 
-  List.map (fun s -> (make_con mp empty_dirpath (mk_label s)))
-    [ "well_founded_induction_type"; "well_founded_induction"; 
-      "Acc_rect"; "Acc_rec" ; "Acc_iter" ; "Fix" ]
-
-let manual_inline = function 
-  | ConstRef c -> List.mem c manual_inline_list
-  | _ -> false 
-
-(* If the user doesn't say he wants to keep [t], we inline in two cases:
-   \begin{itemize}
-   \item the user explicitly requests it 
-   \item [expansion_test] answers that the inlining is a good idea, and 
-   we are free to act (AutoInline is set)
-   \end{itemize} *)
-
-let inline r t = 
-  not (to_keep r) (* The user DOES want to keep it *)
-  && not (is_inline_custom r) 
-  && (to_inline r (* The user DOES want to inline it *) 
-     || (auto_inline () && lang () <> Haskell && not (is_projection r)
-         && (is_recursor r || manual_inline r || inline_test t)))
-
diff --git a/contrib/extraction/mlutil.mli b/contrib/extraction/mlutil.mli
deleted file mode 100644
index a55caaf2..00000000
--- a/contrib/extraction/mlutil.mli
+++ /dev/null
@@ -1,113 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(*i $Id: mlutil.mli 8724 2006-04-20 09:57:01Z letouzey $ i*)
-
-open Util
-open Names
-open Term
-open Libnames
-open Miniml
-
-(*s Utility functions over ML types with meta. *)
-
-val reset_meta_count : unit -> unit
-val new_meta : 'a -> ml_type
-
-val type_subst : int -> ml_type -> ml_type -> ml_type
-val type_subst_list : ml_type list -> ml_type -> ml_type
-val type_subst_vect : ml_type array -> ml_type -> ml_type
-
-val instantiation : ml_schema -> ml_type
-
-val needs_magic : ml_type * ml_type -> bool
-val put_magic_if : bool -> ml_ast -> ml_ast
-val put_magic : ml_type * ml_type -> ml_ast -> ml_ast
-
-(*s ML type environment. *)
-
-module Mlenv : sig 
-  type t 
-  val empty : t
-    
-  (* get the n-th more recently entered schema and instantiate it. *) 
-  val get : t -> int -> ml_type
-
-  (* Adding a type in an environment, after generalizing free meta *)
-  val push_gen : t -> ml_type -> t
-
-  (* Adding a type with no [Tvar] *)
-  val push_type : t -> ml_type -> t
-     
-  (* Adding a type with no [Tvar] nor [Tmeta] *)
-  val push_std_type : t -> ml_type -> t
-end
-
-(*s Utility functions over ML types without meta *)
-
-val type_mem_kn : kernel_name -> ml_type -> bool
-
-val type_maxvar : ml_type -> int
-
-val type_decomp : ml_type -> ml_type list * ml_type
-val type_recomp : ml_type list * ml_type -> ml_type
-
-val var2var' : ml_type -> ml_type 
-
-type abbrev_map = global_reference -> ml_type option
-
-val type_expand : abbrev_map -> ml_type -> ml_type 
-val type_to_sign : abbrev_map -> ml_type -> sign
-val type_to_signature : abbrev_map -> ml_type -> signature
-val type_expunge : abbrev_map -> ml_type -> ml_type
-
-val isDummy : ml_type -> bool
-val isKill : sign -> bool
-
-val case_expunge : signature -> ml_ast -> identifier list * ml_ast
-val term_expunge : signature -> identifier list * ml_ast -> ml_ast
-
-
-(*s Special identifiers. [dummy_name] is to be used for dead code
-    and will be printed as [_] in concrete (Caml) code. *)
-
-val anonymous : identifier
-val dummy_name : identifier
-val id_of_name : name -> identifier
-
-(*s [collect_lambda MLlam(id1,...MLlam(idn,t)...)] returns
-    the list [idn;...;id1] and the term [t]. *)
-
-val collect_lams : ml_ast -> identifier list * ml_ast
-val collect_n_lams : int -> ml_ast -> identifier list * ml_ast
-val nb_lams : ml_ast -> int
-
-val dummy_lams : ml_ast -> int -> ml_ast
-val anonym_or_dummy_lams : ml_ast -> signature -> ml_ast
-
-val eta_args_sign : int -> signature -> ml_ast list 
-
-(*s Utility functions over ML terms. *)
-
-val ast_map : (ml_ast -> ml_ast) -> ml_ast -> ml_ast
-val ast_map_lift : (int -> ml_ast -> ml_ast) -> int -> ml_ast -> ml_ast
-val ast_iter : (ml_ast -> unit) -> ml_ast -> unit
-val ast_occurs : int -> ml_ast -> bool
-val ast_occurs_itvl : int -> int -> ml_ast -> bool
-val ast_lift : int -> ml_ast -> ml_ast
-val ast_pop : ml_ast -> ml_ast
-val ast_subst : ml_ast -> ml_ast -> ml_ast
-
-val ast_glob_subst : ml_ast Refmap.t -> ml_ast -> ml_ast
-
-val normalize : ml_ast -> ml_ast 
-val optimize_fix : ml_ast -> ml_ast
-val inline : global_reference -> ml_ast -> bool
-
-
-
diff --git a/contrib/extraction/modutil.ml b/contrib/extraction/modutil.ml
deleted file mode 100644
index 68adeb81..00000000
--- a/contrib/extraction/modutil.ml
+++ /dev/null
@@ -1,365 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(*i $Id: modutil.ml 11602 2008-11-18 00:08:33Z letouzey $ i*)
-
-open Names
-open Declarations
-open Environ
-open Libnames
-open Util
-open Miniml
-open Table
-open Mlutil
-open Mod_subst
-
-(*S Functions upon ML modules. *)
-
-let rec msid_of_mt = function
-  | MTident mp -> begin
-      match Modops.eval_struct (Global.env()) (SEBident mp) with
-	| SEBstruct(msid,_) -> MPself msid
-	| _ -> anomaly "Extraction:the With can't be applied to a funsig"
-    end
-  | MTwith(mt,_)-> msid_of_mt mt
-  | _ -> anomaly "Extraction:the With operator isn't applied to a name"
-
-(*s Apply some functions upon all [ml_decl] and [ml_spec] found in a 
-   [ml_structure]. *) 
-
-let struct_iter do_decl do_spec s = 
-  let rec mt_iter = function 
-    | MTident _ -> () 
-    | MTfunsig (_,mt,mt') -> mt_iter mt; mt_iter mt'
-    | MTwith (mt,ML_With_type(idl,l,t))->
-	let mp_mt = msid_of_mt mt in
-	let l',idl' = list_sep_last idl in
-	let mp_w =
-	  List.fold_left (fun mp l -> MPdot(mp,label_of_id l)) mp_mt idl'
-	in
-	let r = ConstRef (make_con mp_w empty_dirpath (label_of_id l')) in
-	mt_iter mt; do_decl (Dtype(r,l,t))
-    | MTwith (mt,_)->mt_iter mt
-    | MTsig (_, sign) -> List.iter spec_iter sign
-  and spec_iter = function 
-    | (_,Spec s) -> do_spec s
-    | (_,Smodule mt) -> mt_iter mt
-    | (_,Smodtype mt) -> mt_iter mt
-  in
-  let rec se_iter = function 
-    | (_,SEdecl d) -> do_decl d
-    | (_,SEmodule m) -> 
-	me_iter m.ml_mod_expr; mt_iter m.ml_mod_type
-    | (_,SEmodtype m) -> mt_iter m
-  and me_iter = function 
-    | MEident _ -> () 
-    | MEfunctor (_,mt,me) -> me_iter me; mt_iter mt
-    | MEapply (me,me') -> me_iter me; me_iter me'
-    | MEstruct (msid, sel) -> List.iter se_iter sel
-  in 
-  List.iter (function (_,sel) -> List.iter se_iter sel) s
-
-(*s Apply some fonctions upon all references in [ml_type], [ml_ast], 
-  [ml_decl], [ml_spec] and [ml_structure]. *)
-
-type do_ref = global_reference -> unit
-
-let record_iter_references do_term = function 
-  | Record l -> List.iter do_term l 
-  | _ -> ()
-
-let type_iter_references do_type t = 
-  let rec iter = function 
-    | Tglob (r,l) -> do_type r; List.iter iter l 
-    | Tarr (a,b) -> iter a; iter b 
-    | _ -> () 
-  in iter t
-
-let ast_iter_references do_term do_cons do_type a = 
-  let rec iter a = 
-    ast_iter iter a;
-    match a with 
-      | MLglob r -> do_term r
-      | MLcons (i,r,_) -> 
-	  if lang () = Ocaml then record_iter_references do_term i; 
-	  do_cons r 
-      | MLcase (i,_,v) -> 
-	  if lang () = Ocaml then record_iter_references do_term (fst i); 
-	  Array.iter (fun (r,_,_) -> do_cons r) v
-      | _ -> ()
-  in iter a
-
-let ind_iter_references do_term do_cons do_type kn ind = 
-  let type_iter = type_iter_references do_type in
-  let cons_iter cp l = do_cons (ConstructRef cp); List.iter type_iter l in 
-  let packet_iter ip p = 
-    do_type (IndRef ip); 
-    if lang () = Ocaml then 
-      (match ind.ind_equiv with 
-	 | Equiv kne -> do_type (IndRef (kne, snd ip)); 
-	 | _ -> ()); 
-    Array.iteri (fun j -> cons_iter (ip,j+1)) p.ip_types 
-  in
-  if lang () = Ocaml then record_iter_references do_term ind.ind_info; 
-  Array.iteri (fun i -> packet_iter (kn,i)) ind.ind_packets
-  
-let decl_iter_references do_term do_cons do_type = 
-  let type_iter = type_iter_references do_type 
-  and ast_iter = ast_iter_references do_term do_cons do_type in
-  function 
-    | Dind (kn,ind) -> ind_iter_references do_term do_cons do_type kn ind 
-    | Dtype (r,_,t) -> do_type r; type_iter t 
-    | Dterm (r,a,t) -> do_term r; ast_iter a; type_iter t
-    | Dfix(rv,c,t) -> 	
-	Array.iter do_term rv; Array.iter ast_iter c; Array.iter type_iter t
-
-let spec_iter_references do_term do_cons do_type = function 
-  | Sind (kn,ind) -> ind_iter_references do_term do_cons do_type kn ind
-  | Stype (r,_,ot) -> do_type r; Option.iter (type_iter_references do_type) ot
-  | Sval (r,t) -> do_term r; type_iter_references do_type t
-
-(*s Searching occurrences of a particular term (no lifting done). *)
-
-exception Found
-
-let rec ast_search f a = 
-  if f a then raise Found else ast_iter (ast_search f) a
-
-let decl_ast_search f = function 
-  | Dterm (_,a,_) -> ast_search f a
-  | Dfix (_,c,_) -> Array.iter (ast_search f) c
-  | _ -> () 
-
-let struct_ast_search f s = 
-  try struct_iter (decl_ast_search f) (fun _ -> ()) s; false
-  with Found -> true
-
-let rec type_search f = function  
-  | Tarr (a,b) -> type_search f a; type_search f b 
-  | Tglob (r,l) -> List.iter (type_search f) l
-  | u -> if f u then raise Found
-
-let decl_type_search f = function 
-  | Dind (_,{ind_packets=p})  -> 
-      Array.iter 
-	(fun {ip_types=v} -> Array.iter (List.iter (type_search f)) v) p
-  | Dterm (_,_,u) -> type_search f u
-  | Dfix (_,_,v) -> Array.iter (type_search f) v
-  | Dtype (_,_,u) -> type_search f u
-
-let spec_type_search f = function 
-  | Sind (_,{ind_packets=p}) -> 
-      Array.iter 
-	(fun {ip_types=v} -> Array.iter (List.iter (type_search f)) v) p
-  | Stype (_,_,ot) -> Option.iter (type_search f) ot
-  | Sval (_,u) -> type_search f u
-
-let struct_type_search f s = 
-  try struct_iter (decl_type_search f) (spec_type_search f) s; false
-  with Found -> true
-
-
-(*s Generating the signature. *)
-
-let rec msig_of_ms = function 
-  | [] -> [] 
-  | (l,SEdecl (Dind (kn,i))) :: ms -> 
-      (l,Spec (Sind (kn,i))) :: (msig_of_ms ms)
-  | (l,SEdecl (Dterm (r,_,t))) :: ms -> 
-      (l,Spec (Sval (r,t))) :: (msig_of_ms ms)
-  | (l,SEdecl (Dtype (r,v,t))) :: ms -> 
-      (l,Spec (Stype (r,v,Some t))) :: (msig_of_ms ms) 
-  | (l,SEdecl (Dfix (rv,_,tv))) :: ms -> 
-      let msig = ref (msig_of_ms ms) in 
-      for i = Array.length rv - 1 downto 0 do 
-	msig := (l,Spec (Sval (rv.(i),tv.(i))))::!msig
-      done; 
-      !msig
-  | (l,SEmodule m) :: ms -> (l,Smodule m.ml_mod_type) :: (msig_of_ms ms)
-  | (l,SEmodtype m) :: ms -> (l,Smodtype m) :: (msig_of_ms ms)
-
-let signature_of_structure s = 
-  List.map (fun (mp,ms) -> mp,msig_of_ms ms) s 
-
-
-(*s Searching one [ml_decl] in a [ml_structure] by its [global_reference] *)
-
-let get_decl_in_structure r struc = 
-  try 
-    let base_mp,ll = labels_of_ref r in 
-    if not (at_toplevel base_mp) then error_not_visible r;
-    let sel = List.assoc base_mp struc in
-    let rec go ll sel = match ll with 
-      | [] -> assert false
-      | l :: ll -> 
-	  match List.assoc l sel with 
-	    | SEdecl d -> d 
-	    | SEmodtype m -> assert false
-	    | SEmodule m ->
-		match m.ml_mod_expr with 
-		  | MEstruct (_,sel) -> go ll sel 
-		  | _ -> error_not_visible r 
-    in go ll sel
-  with Not_found -> assert false
-
-
-(*s Optimization of a [ml_structure]. *)
-
-(* Some transformations of ML terms. [optimize_struct] simplify
-   all beta redexes (when the argument does not occur, it is just
-   thrown away; when it occurs exactly once it is substituted; otherwise
-   a let-in redex is created for clarity) and iota redexes, plus some other
-   optimizations. *)
-
-let dfix_to_mlfix rv av i = 
-  let rec make_subst n s = 
-    if n < 0 then s 
-    else make_subst (n-1) (Refmap.add rv.(n) (n+1) s)
-  in 
-  let s = make_subst (Array.length rv - 1) Refmap.empty 
-  in 
-  let rec subst n t = match t with 
-    | MLglob ((ConstRef kn) as refe) -> 
-	(try MLrel (n + (Refmap.find refe s)) with Not_found -> t)
-    | _ -> ast_map_lift subst n t 
-  in 
-  let ids = Array.map (fun r -> id_of_label (label_of_r r)) rv in 
-  let c = Array.map (subst 0) av 
-  in MLfix(i, ids, c)
-
-let rec optim to_appear s = function
-  | [] -> []
-  | (Dtype (r,_,Tdummy _) | Dterm(r,MLdummy,_)) as d :: l ->
-      if List.mem r to_appear 
-      then d :: (optim to_appear s l) 
-      else optim to_appear s l
-  | Dterm (r,t,typ) :: l ->
-      let t = normalize (ast_glob_subst !s t) in 
-      let i = inline r t in 
-      if i then s := Refmap.add r t !s; 
-      if not i || modular () || List.mem r to_appear 
-      then 
-	let d = match optimize_fix t with 
-	  | MLfix (0, _, [|c|]) -> 
-	      Dfix ([|r|], [|ast_subst (MLglob r) c|], [|typ|])
-	  | t -> Dterm (r, t, typ)
-	in d :: (optim to_appear s l)
-      else optim to_appear s l
-  | d :: l -> d :: (optim to_appear s l)
-
-let rec optim_se top to_appear s = function 
-  | [] -> [] 
-  | (l,SEdecl (Dterm (r,a,t))) :: lse -> 
-      let a = normalize (ast_glob_subst !s a) in 
-      let i = inline r a in 
-      if i then s := Refmap.add r a !s; 
-      if top && i && not (modular ()) && not (List.mem r to_appear)
-      then optim_se top to_appear s lse
-      else 
-	let d = match optimize_fix a with 
-	  | MLfix (0, _, [|c|]) -> 
-	      Dfix ([|r|], [|ast_subst (MLglob r) c|], [|t|])
-	  | a -> Dterm (r, a, t)
-	in (l,SEdecl d) :: (optim_se top to_appear s lse)
-  | (l,SEdecl (Dfix (rv,av,tv))) :: lse -> 
-      let av = Array.map (fun a -> normalize (ast_glob_subst !s a)) av in 
-      let all = ref true in 
-      (* This fake body ensures that no fixpoint will be auto-inlined. *)
-      let fake_body = MLfix (0,[||],[||]) in 
-      for i = 0 to Array.length rv - 1 do 
-	if inline rv.(i) fake_body
-	then s := Refmap.add rv.(i) (dfix_to_mlfix rv av i) !s
-	else all := false
-      done; 
-      if !all && top && not (modular ())
-	&& (array_for_all (fun r -> not (List.mem r to_appear)) rv)  
-      then optim_se top to_appear s lse
-      else (l,SEdecl (Dfix (rv, av, tv))) :: (optim_se top to_appear s lse)
-  | (l,SEmodule m) :: lse -> 
-      let m = { m with ml_mod_expr = optim_me to_appear s m.ml_mod_expr}
-      in (l,SEmodule m) :: (optim_se top to_appear s lse)
-  | se :: lse -> se :: (optim_se top to_appear s lse) 
-
-and optim_me to_appear s = function 
-  | MEstruct (msid, lse) -> MEstruct (msid, optim_se false to_appear s lse)
-  | MEident mp as me -> me
-  | MEapply (me, me') -> 
-      MEapply (optim_me to_appear s me, optim_me to_appear s me')
-  | MEfunctor (mbid,mt,me) -> MEfunctor (mbid,mt, optim_me to_appear s me)
-
-(* After these optimisations, some dependencies may not be needed anymore. 
-   For monolithic extraction, we recompute a minimal set of dependencies. *)
-
-exception NoDepCheck
-
-let base_r = function
-  | ConstRef c as r -> r
-  | IndRef (kn,_) -> IndRef (kn,0)
-  | ConstructRef ((kn,_),_) -> IndRef (kn,0)
-  | _ -> assert false
-
-let reset_needed, add_needed, found_needed, is_needed =
-  let needed = ref Refset.empty in
-  ((fun l -> needed := Refset.empty),
-   (fun r -> needed := Refset.add (base_r r) !needed),
-   (fun r -> needed := Refset.remove (base_r r) !needed),
-   (fun r -> Refset.mem (base_r r) !needed))
-
-let declared_refs = function
-  | Dind (kn,_) -> [|IndRef (kn,0)|]
-  | Dtype (r,_,_) -> [|r|]
-  | Dterm (r,_,_) -> [|r|]
-  | Dfix (rv,_,_) -> rv
-
-(* Computes the dependencies of a declaration, except in case 
-   of custom extraction. *)
-
-let compute_deps_decl = function
-  | Dind (kn,ind) ->
-      (* Todo Later : avoid dependencies when Extract Inductive *)
-      ind_iter_references add_needed add_needed add_needed kn ind
-  | Dtype (r,ids,t) ->
-      if not (is_custom r) then type_iter_references add_needed t
-  | Dterm (r,u,t) ->
-      type_iter_references add_needed t;
-      if not (is_custom r) then
-	ast_iter_references add_needed add_needed add_needed u
-  | Dfix _ as d ->
-      (* Todo Later : avoid dependencies when Extract Constant *)
-      decl_iter_references add_needed add_needed add_needed d
-
-let rec depcheck_se = function
-  | [] -> []
-  | ((l,SEdecl d) as t)::se ->
-      let se' = depcheck_se se in
-      let rv = declared_refs d in
-      if not (array_exists is_needed rv) then
-	(Array.iter remove_info_axiom rv; se')
-      else
-	(Array.iter found_needed rv; compute_deps_decl d; t::se')
-  | _ -> raise NoDepCheck
-
-let rec depcheck_struct = function
-  | [] -> []
-  | (mp,lse)::struc ->
-      let struc' = depcheck_struct struc in
-      let lse' = depcheck_se lse in
-      (mp,lse')::struc'
-
-let optimize_struct to_appear struc =
-  let subst = ref (Refmap.empty : ml_ast Refmap.t) in
-  let opt_struc =
-    List.map (fun (mp,lse) -> (mp, optim_se true to_appear subst lse)) struc
-  in
-  let opt_struc = List.filter (fun (_,lse) -> lse<>[]) opt_struc in
-  try
-    if modular () then raise NoDepCheck;
-    reset_needed ();
-    List.iter add_needed to_appear;
-    depcheck_struct opt_struc
-  with NoDepCheck -> opt_struc
diff --git a/contrib/extraction/modutil.mli b/contrib/extraction/modutil.mli
deleted file mode 100644
index e279261d..00000000
--- a/contrib/extraction/modutil.mli
+++ /dev/null
@@ -1,41 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(*i $Id: modutil.mli 11602 2008-11-18 00:08:33Z letouzey $ i*)
-
-open Names
-open Declarations
-open Environ
-open Libnames
-open Miniml
-open Mod_subst
-
-(*s Functions upon ML modules. *)
-
-val struct_ast_search : (ml_ast -> bool) -> ml_structure -> bool
-val struct_type_search : (ml_type -> bool) -> ml_structure -> bool
-
-type do_ref = global_reference -> unit 
-
-val decl_iter_references : do_ref -> do_ref -> do_ref -> ml_decl -> unit
-val spec_iter_references : do_ref -> do_ref -> do_ref -> ml_spec -> unit
-
-val signature_of_structure : ml_structure -> ml_signature
-
-val msid_of_mt : ml_module_type -> module_path
-
-val get_decl_in_structure : global_reference -> ml_structure -> ml_decl
-
-(* Some transformations of ML terms. [optimize_struct] simplify
-   all beta redexes (when the argument does not occur, it is just
-   thrown away; when it occurs exactly once it is substituted; otherwise
-   a let-in redex is created for clarity) and iota redexes, plus some other
-   optimizations. The first argument is the list of objects we want to appear.
-*)
-
-val optimize_struct : global_reference list -> ml_structure -> ml_structure
diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml
deleted file mode 100644
index 0166d854..00000000
--- a/contrib/extraction/ocaml.ml
+++ /dev/null
@@ -1,731 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(*i $Id: ocaml.ml 11559 2008-11-07 22:03:34Z letouzey $ i*)
-
-(*s Production of Ocaml syntax. *)
-
-open Pp
-open Util
-open Names
-open Nameops
-open Libnames
-open Table
-open Miniml
-open Mlutil
-open Modutil
-open Common
-open Declarations
-
-
-(*s Some utility functions. *)
-
-let pp_tvar id = 
-  let s = string_of_id id in 
-  if String.length s < 2 || s.[1]<>'\'' 
-  then str ("'"^s)
-  else str ("' "^s)
-
-let pp_tuple_light f = function
-  | [] -> mt ()
-  | [x] -> f true x
-  | l -> 
-      pp_par true (prlist_with_sep (fun () -> str "," ++ spc ()) (f false) l)
-
-let pp_tuple f = function
-  | [] -> mt ()
-  | [x] -> f x
-  | l -> pp_par true (prlist_with_sep (fun () -> str "," ++ spc ()) f l)
-
-let pp_boxed_tuple f = function
-  | [] -> mt ()
-  | [x] -> f x
-  | l -> pp_par true (hov 0 (prlist_with_sep (fun () -> str "," ++ spc ()) f l))
-
-let pp_abst = function
-  | [] -> mt ()
-  | l  -> 
-      str "fun " ++ prlist_with_sep (fun () -> str " ") pr_id l ++ 
-      str " ->" ++ spc ()
-
-let pp_parameters l = 
-  (pp_boxed_tuple pp_tvar l ++ space_if (l<>[]))
-
-let pp_string_parameters l = 
-  (pp_boxed_tuple str l ++ space_if (l<>[])) 
-
-(*s Ocaml renaming issues. *)
-
-let keywords =     
-  List.fold_right (fun s -> Idset.add (id_of_string s))
-  [ "and"; "as"; "assert"; "begin"; "class"; "constraint"; "do";
-    "done"; "downto"; "else"; "end"; "exception"; "external"; "false";
-    "for"; "fun"; "function"; "functor"; "if"; "in"; "include";
-    "inherit"; "initializer"; "lazy"; "let"; "match"; "method";
-    "module"; "mutable"; "new"; "object"; "of"; "open"; "or";
-    "parser"; "private"; "rec"; "sig"; "struct"; "then"; "to"; "true";
-    "try"; "type"; "val"; "virtual"; "when"; "while"; "with"; "mod";
-    "land"; "lor"; "lxor"; "lsl"; "lsr"; "asr" ; "unit" ; "_" ; "__" ] 
-  Idset.empty
-
-let pp_open mp = str ("open "^ string_of_modfile mp ^"\n")
-
-let preamble _ used_modules usf = 
-  prlist pp_open used_modules ++
-  (if used_modules = [] then mt () else fnl ()) ++
-  (if usf.tdummy || usf.tunknown then str "type __ = Obj.t\n" else mt()) ++
-  (if usf.mldummy then 
-     str "let __ = let rec f _ = Obj.repr f in Obj.repr f\n"
-   else mt ()) ++
-  (if usf.tdummy || usf.tunknown || usf.mldummy then fnl () else mt ())
-
-let sig_preamble _ used_modules usf =
-  prlist pp_open used_modules ++
-  (if used_modules = [] then mt () else fnl ()) ++
-  (if usf.tdummy || usf.tunknown then str "type __ = Obj.t\n\n" else mt())
-
-(*s The pretty-printer for Ocaml syntax*)
-
-(* Beware of the side-effects of [pp_global] and [pp_modname].
-   They are used to update table of content for modules. Many [let] 
-   below should not be altered since they force evaluation order. 
-*)
-
-let pp_global k r =
-  if is_inline_custom r then str (find_custom r)
-  else str (Common.pp_global k r)
-
-let pp_modname mp = str (Common.pp_module mp)
-
-
-let is_infix r = 
-  is_inline_custom r && 
-  (let s = find_custom r in 
-   let l = String.length s in 
-   l >= 2 && s.[0] = '(' && s.[l-1] = ')')
-
-let get_infix r = 
-  let s = find_custom r in 
-  String.sub s 1 (String.length s - 2)
-
-exception NoRecord
-
-let find_projections = function Record l -> l | _ -> raise NoRecord
-
-(*s Pretty-printing of types. [par] is a boolean indicating whether parentheses
-    are needed or not. *)
-
-let kn_sig = 
-  let specif = MPfile (dirpath_of_string "Coq.Init.Specif") in 
-  make_kn specif empty_dirpath (mk_label "sig")
-
-let rec pp_type par vl t =
-  let rec pp_rec par = function
-    | Tmeta _ | Tvar' _ | Taxiom -> assert false
-    | Tvar i -> (try pp_tvar (List.nth vl (pred i)) 
-		 with _ -> (str "'a" ++ int i))
-    | Tglob (r,[a1;a2]) when is_infix r -> 
-	pp_par par 
-	  (pp_rec true a1 ++ spc () ++ str (get_infix r) ++ spc () ++ 
-	   pp_rec true a2)
-    | Tglob (r,[]) -> pp_global Type r
-    | Tglob (r,l) -> 
-	if r = IndRef (kn_sig,0) then 
-	  pp_tuple_light pp_rec l
-	else 
-	  pp_tuple_light pp_rec l ++ spc () ++ pp_global Type r
-    | Tarr (t1,t2) ->
-	pp_par par 
-	  (pp_rec true t1 ++ spc () ++ str "->" ++ spc () ++ pp_rec false t2)
-    | Tdummy _ -> str "__"
-    | Tunknown -> str "__"
-  in 
-  hov 0 (pp_rec par t)
-
-(*s Pretty-printing of expressions. [par] indicates whether
-    parentheses are needed or not. [env] is the list of names for the
-    de Bruijn variables. [args] is the list of collected arguments
-    (already pretty-printed). *)
-
-let is_ifthenelse = function 
-  | [|(r1,[],_);(r2,[],_)|] -> 
-      (try (find_custom r1 = "true") && (find_custom r2 = "false") 
-       with Not_found -> false)
-  | _ -> false
-
-let expr_needs_par = function
-  | MLlam _  -> true
-  | MLcase (_,_,[|_|]) -> false 
-  | MLcase (_,_,pv) -> not (is_ifthenelse pv)
-  | _        -> false 
-
-
-let rec pp_expr par env args = 
-  let par' = args <> [] || par
-  and apply st = pp_apply st par args in 
-  function
-    | MLrel n -> 
-	let id = get_db_name n env in apply (pr_id id)
-    | MLapp (f,args') ->
-	let stl = List.map (pp_expr true env []) args' in
-        pp_expr par env (stl @ args) f
-    | MLlam _ as a -> 
-      	let fl,a' = collect_lams a in
-	let fl,env' = push_vars fl env in
-	let st = (pp_abst (List.rev fl) ++ pp_expr false env' [] a') in
-	apply (pp_par par' st)
-    | MLletin (id,a1,a2) ->
-	let i,env' = push_vars [id] env in
-	let pp_id = pr_id (List.hd i)
-	and pp_a1 = pp_expr false env [] a1
-	and pp_a2 = pp_expr (not par && expr_needs_par a2) env' [] a2 in 
-	hv 0 
-	  (apply 
-	     (pp_par par' 
-		(hv 0 
-		   (hov 2 
-		      (str "let " ++ pp_id ++ str " =" ++ spc () ++ pp_a1) ++ 
-		    spc () ++ str "in") ++ 
-		 spc () ++ hov 0 pp_a2)))
-    | MLglob r -> 
-	(try 
-	   let args = list_skipn (projection_arity r) args in 
-	   let record = List.hd args in 
-	   pp_apply (record ++ str "." ++ pp_global Term r) par (List.tl args)
-	 with _ -> apply (pp_global Term r))
-    | MLcons (Coinductive,r,[]) ->
-	assert (args=[]);
-	pp_par par (str "lazy " ++ pp_global Cons r)
-    | MLcons (Coinductive,r,args') -> 
-	assert (args=[]);
-	let tuple = pp_tuple (pp_expr true env []) args' in 
-	pp_par par (str "lazy (" ++ pp_global Cons r ++ spc() ++ tuple ++str ")")
-    | MLcons (_,r,[]) -> 
-	assert (args=[]);
-	pp_global Cons r
-    | MLcons (Record projs, r, args') -> 
-	assert (args=[]); 
-	pp_record_pat (projs, List.map (pp_expr true env []) args')
-    | MLcons (_,r,[arg1;arg2]) when is_infix r -> 
-	assert (args=[]); 
-	pp_par par
-	  ((pp_expr true env [] arg1) ++ spc () ++ str (get_infix r) ++
-	   spc () ++ (pp_expr true env [] arg2))
-    | MLcons (_,r,args') -> 
-	assert (args=[]);
-	let tuple = pp_tuple (pp_expr true env []) args' in 
-	pp_par par (pp_global Cons r ++ spc () ++ tuple)
-    | MLcase ((i,factors), t, pv) ->
-	let expr = if i = Coinductive then 
-	  (str "Lazy.force" ++ spc () ++ pp_expr true env [] t)
-	else 
-	  (pp_expr false env [] t) 
-	in 
-	(try 
-	   let projs = find_projections i in 
-	   let (_, ids, c) = pv.(0) in 
-	   let n = List.length ids in 
-	   match c with 
-	     | MLrel i when i <= n -> 
-		 apply (pp_par par' (pp_expr true env [] t ++ str "." ++ 
-				     pp_global Term (List.nth projs (n-i))))
-	     | MLapp (MLrel i, a) when i <= n -> 
-		 if List.exists (ast_occurs_itvl 1 n) a 
-		 then raise NoRecord
-		 else
-		   let ids,env' = push_vars (List.rev ids) env in
-		   (pp_apply 
-		      (pp_expr true env [] t ++ str "." ++ 
-		       pp_global Term (List.nth projs (n-i)))
-		      par ((List.map (pp_expr true env' []) a) @ args))
-	     | _ -> raise NoRecord
-	 with NoRecord -> 
-	   if Array.length pv = 1 then 
-	     let s1,s2 = pp_one_pat env i pv.(0) in 
-	     apply 
-	       (hv 0 
-		  (pp_par par' 
-		     (hv 0 
-			(hov 2 (str "let " ++ s1 ++ str " =" ++ spc () ++ expr) 
-			 ++ spc () ++ str "in") ++ 
-		      spc () ++ hov 0 s2)))
-	   else 
- 	     apply
-      	       (pp_par par' 
-		  (try pp_ifthenelse par' env expr pv 
-		   with Not_found -> 
-		     v 0 (str "match " ++ expr ++ str " with" ++ fnl () ++
-			  str "  | " ++ pp_pat env (i,factors) pv))))
-    | MLfix (i,ids,defs) ->
-	let ids',env' = push_vars (List.rev (Array.to_list ids)) env in
-      	pp_fix par env' i (Array.of_list (List.rev ids'),defs) args
-    | MLexn s -> 
-	(* An [MLexn] may be applied, but I don't really care. *)
-	pp_par par (str "assert false" ++ spc () ++ str ("(* "^s^" *)"))
-    | MLdummy ->
-	str "__" (* An [MLdummy] may be applied, but I don't really care. *)
-    | MLmagic a ->
-	pp_apply (str "Obj.magic") par (pp_expr true env [] a :: args)
-    | MLaxiom -> 
-	pp_par par (str "failwith \"AXIOM TO BE REALIZED\"")
-
-	  
-and pp_record_pat (projs, args) =
-   str "{ " ++
-   prlist_with_sep (fun () -> str ";" ++ spc ()) 
-     (fun (r,a) -> pp_global Term r ++ str " =" ++ spc () ++ a)
-     (List.combine projs args) ++
-   str " }"
-
-and pp_ifthenelse par env expr pv = match pv with 
-  | [|(tru,[],the);(fal,[],els)|] when 
-      (find_custom tru = "true") && (find_custom fal = "false")
-      -> 
-      hv 0 (hov 2 (str "if " ++ expr) ++ spc () ++ 
-            hov 2 (str "then " ++
-		   hov 2 (pp_expr (expr_needs_par the) env [] the)) ++ spc () ++ 
-	    hov 2 (str "else " ++
-	           hov 2 (pp_expr (expr_needs_par els) env [] els)))
-  | _ -> raise Not_found
-
-and pp_one_pat env i (r,ids,t) = 
-  let ids,env' = push_vars (List.rev ids) env in
-  let expr = pp_expr (expr_needs_par t) env' [] t in 
-  try 
-    let projs = find_projections i in 
-    pp_record_pat (projs, List.rev_map pr_id ids), expr
-  with NoRecord -> 
-    (match List.rev ids with 
-      | [i1;i2] when is_infix r -> 
-	  pr_id i1 ++ str " " ++ str (get_infix r) ++ str " " ++ pr_id i2
-      | [] -> pp_global Cons r
-      | ids -> pp_global Cons r ++ str " " ++ pp_boxed_tuple pr_id ids), 
-    expr
-  
-and pp_pat env (info,factors) pv = 
-  prvecti 
-    (fun i x -> if List.mem i factors then mt () else 
-       let s1,s2 = pp_one_pat env info x in 
-       hov 2 (s1 ++ str " ->" ++ spc () ++ s2) ++
-       (if factors = [] && i = Array.length pv-1 then mt () 
-	else fnl () ++ str "  | ")) pv 
-  ++ 
-  match factors with 
-     | [] -> mt ()
-     | i::_ -> 
-	 let (_,ids,t) = pv.(i) in 
-	 let t = ast_lift (-List.length ids) t in 
-	 hov 2 (str "_ ->" ++ spc () ++ pp_expr (expr_needs_par t) env [] t)
-
-and pp_function env t =
-  let bl,t' = collect_lams t in
-  let bl,env' = push_vars bl env in
-  match t' with 
-    | MLcase(i,MLrel 1,pv) when fst i=Standard -> 
-	if not (ast_occurs 1 (MLcase(i,MLdummy,pv))) then 
-	  pr_binding (List.rev (List.tl bl)) ++
-       	  str " = function" ++ fnl () ++
-	  v 0 (str "  | " ++ pp_pat env' i pv)
-	else
-          pr_binding (List.rev bl) ++ 
-          str " = match " ++ pr_id (List.hd bl) ++ str " with" ++ fnl () ++
-	  v 0 (str "  | " ++ pp_pat env' i pv)
-    | _ -> 
-          pr_binding (List.rev bl) ++
-	  str " =" ++ fnl () ++ str "  " ++
-	  hov 2 (pp_expr false env' [] t')
-
-(*s names of the functions ([ids]) are already pushed in [env],
-    and passed here just for convenience. *)
-
-and pp_fix par env i (ids,bl) args =
-  pp_par par 
-    (v 0 (str "let rec " ++
-	  prvect_with_sep
-      	    (fun () -> fnl () ++ str "and ")
-	    (fun (fi,ti) -> pr_id fi ++ pp_function env ti)
-	    (array_map2 (fun id b -> (id,b)) ids bl) ++
-	  fnl () ++
-	  hov 2 (str "in " ++ pp_apply (pr_id ids.(i)) false args)))
-
-let pp_val e typ = 
-  hov 4 (str "(** val " ++ e ++ str " :" ++ spc () ++ pp_type false [] typ ++ 
-  str " **)")  ++ fnl2 ()
-
-(*s Pretty-printing of [Dfix] *)
-
-let pp_Dfix (rv,c,t) = 
-  let names = Array.map 
-    (fun r -> if is_inline_custom r then mt () else pp_global Term r) rv
-  in 
-  let rec pp sep letand i = 
-    if i >= Array.length rv then mt ()
-    else if is_inline_custom rv.(i) then pp sep letand (i+1)
-    else 
-      let def = 
-	if is_custom rv.(i) then str " = " ++ str (find_custom rv.(i))
-	else pp_function (empty_env ()) c.(i)
-      in 
-      sep () ++ pp_val names.(i) t.(i) ++ 
-      str letand ++ names.(i) ++ def ++ pp fnl2 "and " (i+1) 
-  in pp mt "let rec " 0
-
-(*s Pretty-printing of inductive types declaration. *)
-
-let pp_equiv param_list name = function 
-  | NoEquiv, _ -> mt ()
-  | Equiv kn, i -> 
-      str " = " ++ pp_parameters param_list ++ pp_global Type (IndRef (kn,i))
-  | RenEquiv ren, _  ->
-      str " = " ++ pp_parameters param_list ++ str (ren^".") ++ name
-
-let pp_comment s = str "(* " ++ s ++ str " *)"
-
-let pp_one_ind prefix ip_equiv pl name cnames ctyps =
-  let pl = rename_tvars keywords pl in
-  let pp_constructor i typs =
-    (if i=0 then mt () else fnl ()) ++ 
-    hov 5 (str "  | " ++ cnames.(i) ++
-	   (if typs = [] then mt () else str " of ") ++
-	   prlist_with_sep 
-	    (fun () -> spc () ++ str "* ") (pp_type true pl) typs)
-  in
-  pp_parameters pl ++ str prefix ++ name ++
-  pp_equiv pl name ip_equiv ++ str " =" ++
-  if Array.length ctyps = 0 then str " unit (* empty inductive *)" 
-  else fnl () ++ v 0 (prvecti pp_constructor ctyps)
-
-let pp_logical_ind packet = 
-  pp_comment (pr_id packet.ip_typename ++ str " : logical inductive") ++ 
-  fnl () ++
-  pp_comment (str "with constructors : " ++ 
-	      prvect_with_sep spc pr_id packet.ip_consnames) ++
-  fnl ()
-
-let pp_singleton kn packet = 
-  let name = pp_global Type (IndRef (kn,0)) in 
-  let l = rename_tvars keywords packet.ip_vars in 
-  hov 2 (str "type " ++ pp_parameters l ++ name ++ str " =" ++ spc () ++
-	 pp_type false l (List.hd packet.ip_types.(0)) ++ fnl () ++
-	 pp_comment (str "singleton inductive, whose constructor was " ++ 
-		     pr_id packet.ip_consnames.(0)))
-
-let pp_record kn projs ip_equiv packet = 
-  let name = pp_global Type (IndRef (kn,0)) in
-  let projnames = List.map (pp_global Term) projs in 
-  let l = List.combine projnames packet.ip_types.(0) in 
-  let pl = rename_tvars keywords packet.ip_vars in 
-  str "type " ++ pp_parameters pl ++ name ++ 
-  pp_equiv pl name ip_equiv ++ str " = { "++
-  hov 0 (prlist_with_sep (fun () -> str ";" ++ spc ()) 
-	   (fun (p,t) -> p ++ str " : " ++ pp_type true pl t) l) 
-  ++ str " }"
-
-let pp_coind pl name = 
-  let pl = rename_tvars keywords pl in
-  pp_parameters pl ++ name ++ str " = " ++ 
-  pp_parameters pl ++ str "__" ++ name ++ str " Lazy.t" ++ 
-  fnl() ++ str "and "
-
-let pp_ind co kn ind =
-  let prefix = if co then "__" else "" in 
-  let some = ref false in 
-  let init= ref (str "type ") in 
-  let names = 
-    Array.mapi (fun i p -> if p.ip_logical then mt () else 
-		  pp_global Type (IndRef (kn,i)))
-      ind.ind_packets
-  in 
-  let cnames = 
-    Array.mapi 
-      (fun i p -> if p.ip_logical then [||] else 
-	 Array.mapi (fun j _ -> pp_global Cons (ConstructRef ((kn,i),j+1)))
-	   p.ip_types)
-      ind.ind_packets
-  in 
-  let rec pp i =  
-    if i >= Array.length ind.ind_packets then mt () 
-    else 
-      let ip = (kn,i) in 
-      let ip_equiv = ind.ind_equiv, i in 
-      let p = ind.ind_packets.(i) in 
-      if is_custom (IndRef ip) then pp (i+1)
-      else begin 
-	some := true; 
-	if p.ip_logical then pp_logical_ind p ++ pp (i+1)
-	else 
-	  let s = !init in 
-	  begin 
-	    init := (fnl () ++ str "and "); 
-	    s ++
-	    (if co then pp_coind p.ip_vars names.(i) else mt ()) ++
-	    pp_one_ind 
-	      prefix ip_equiv p.ip_vars names.(i) cnames.(i) p.ip_types ++
-	    pp (i+1)
-	  end
-      end
-  in 
-  let st = pp 0 in if !some then st else failwith "empty phrase"
-	     
-
-(*s Pretty-printing of a declaration. *)
-
-let pp_mind kn i = 
-  match i.ind_info with 
-    | Singleton -> pp_singleton kn i.ind_packets.(0)
-    | Coinductive -> pp_ind true kn i
-    | Record projs -> 
-	pp_record kn projs (i.ind_equiv,0) i.ind_packets.(0)
-    | Standard -> pp_ind false kn i
-
-let pp_decl = function
-    | Dtype (r,_,_) when is_inline_custom r -> failwith "empty phrase"
-    | Dterm (r,_,_) when is_inline_custom r -> failwith "empty phrase"
-    | Dind (kn,i) -> pp_mind kn i
-    | Dtype (r, l, t) -> 
-        let name = pp_global Type r in 
-	let l = rename_tvars keywords l in 
-        let ids, def = 
-	  try 
-	    let ids,s = find_type_custom r in 
-	    pp_string_parameters ids, str "=" ++ spc () ++ str s 
-	  with Not_found -> 
-	    pp_parameters l, 
-	    if t = Taxiom then str "(* AXIOM TO BE REALIZED *)"
-	    else str "=" ++ spc () ++ pp_type false l t
-	in 
-	hov 2 (str "type " ++ ids ++ name ++ spc () ++ def)
-    | Dterm (r, a, t) -> 
-	let def = 
-	  if is_custom r then str (" = " ^ find_custom r)
-	  else if is_projection r then 
-	    (prvect str (Array.make (projection_arity r) " _")) ++ 
-	    str " x = x."
-	  else pp_function (empty_env ()) a
-	in 
-	let name = pp_global Term r in 
-	let postdef = if is_projection r then name else mt () in 
-	pp_val name t ++ hov 0 (str "let " ++ name ++ def ++ postdef)
-    | Dfix (rv,defs,typs) ->
-	pp_Dfix (rv,defs,typs)
-
-let pp_alias_decl ren = function 
-  | Dind (kn,i) -> pp_mind kn { i with ind_equiv = RenEquiv ren }
-  | Dtype (r, l, _) -> 
-      let name = pp_global Type r in 
-      let l = rename_tvars keywords l in 
-      let ids = pp_parameters l in 
-      hov 2 (str "type " ++ ids ++ name ++ str " =" ++ spc () ++ ids ++ 
-	     str (ren^".") ++ name)
-  | Dterm (r, a, t) -> 
-      let name = pp_global Term r in
-      hov 2 (str "let " ++ name ++ str (" = "^ren^".") ++ name)
-  | Dfix (rv, _, _) ->
-      prvecti (fun i r -> if is_inline_custom r then mt () else 
-		 let name = pp_global Term r in 
-		 hov 2 (str "let " ++ name ++ str (" = "^ren^".") ++ name) ++
-		 fnl ()) 
-	rv
-
-let pp_spec = function 
-  | Sval (r,_) when is_inline_custom r -> failwith "empty phrase"
-  | Stype (r,_,_) when is_inline_custom r -> failwith "empty phrase"
-  | Sind (kn,i) -> pp_mind kn i
-  | Sval (r,t) -> 
-      let def = pp_type false [] t in 
-      let name = pp_global Term r in 
-      hov 2 (str "val " ++ name ++ str " :" ++ spc () ++ def)
-  | Stype (r,vl,ot) -> 
-      let name = pp_global Type r in
-      let l = rename_tvars keywords vl in 
-      let ids, def = 
-	try 
-	  let ids, s = find_type_custom r in 
-	  pp_string_parameters ids,  str "= " ++ str s 
-	with Not_found -> 
-	  let ids = pp_parameters l in 
-	  match ot with 
-	    | None -> ids, mt ()
-	    | Some Taxiom -> ids, str "(* AXIOM TO BE REALIZED *)" 
-	    | Some t -> ids, str "=" ++ spc () ++ pp_type false l t 
-      in 
-      hov 2 (str "type " ++ ids ++ name ++ spc () ++ def)
-
-let pp_alias_spec ren = function 
-  | Sind (kn,i) -> pp_mind kn { i with ind_equiv = RenEquiv ren }
-  | Stype (r,l,_) ->       
-      let name = pp_global Type r in 
-      let l = rename_tvars keywords l in 
-      let ids = pp_parameters l in 
-      hov 2 (str "type " ++ ids ++ name ++ str " =" ++ spc () ++ ids ++ 
-	     str (ren^".") ++ name)
-  | Sval _ -> assert false
-	  
-let rec pp_specif = function 
-  | (_,Spec (Sval _ as s)) -> pp_spec s
-  | (l,Spec s) -> 
-      (try 
-	 let ren = Common.check_duplicate (top_visible_mp ()) l in 
-	 hov 1 (str ("module "^ren^" : sig ") ++ fnl () ++ pp_spec s) ++
-	 fnl () ++ str "end" ++ fnl () ++
-	 pp_alias_spec ren s
-       with Not_found -> pp_spec s)
-  | (l,Smodule mt) -> 
-      let def = pp_module_type (Some l) mt in 
-      let def' = pp_module_type (Some l) mt in 
-      let name = pp_modname (MPdot (top_visible_mp (), l)) in 
-      hov 1 (str "module " ++ name ++ str " : " ++ fnl () ++ def) ++
-      (try 
-	 let ren = Common.check_duplicate (top_visible_mp ()) l in
-	 fnl () ++ hov 1 (str ("module "^ren^" : ") ++ fnl () ++ def')
-       with Not_found -> Pp.mt ())
-  | (l,Smodtype mt) -> 
-      let def = pp_module_type None mt in 
-      let name = pp_modname (MPdot (top_visible_mp (), l)) in
-      hov 1 (str "module type " ++ name ++ str " = " ++ fnl () ++ def) ++
-      (try 
-	 let ren = Common.check_duplicate (top_visible_mp ()) l in 
-	 fnl () ++ str ("module type "^ren^" = ") ++ name
-       with Not_found -> Pp.mt ())
-
-and pp_module_type ol = function 
-  | MTident kn -> 
-      pp_modname kn
-  | MTfunsig (mbid, mt, mt') -> 
-      let typ = pp_module_type None mt in 
-      let name = pp_modname (MPbound mbid) in 
-      let def = pp_module_type None mt' in 
-      str "functor (" ++ name ++ str ":" ++ typ ++ str ") ->" ++ fnl () ++ def
-  | MTsig (msid, sign) ->
-      let tvm = top_visible_mp () in
-      let mp = match ol with None -> MPself msid | Some l -> MPdot (tvm,l) in
-      (* References in [sign] are in short form (relative to [msid]).
-	 In push_visible, [msid-->mp] is added to the current subst. *)
-      push_visible mp (Some msid);
-      let l = map_succeed pp_specif sign in 
-      pop_visible (); 
-      str "sig " ++ fnl () ++ 
-      v 1 (str " " ++ prlist_with_sep fnl2 identity l) ++
-	fnl () ++ str "end"
-  | MTwith(mt,ML_With_type(idl,vl,typ)) ->
-      let ids = pp_parameters (rename_tvars keywords vl) in
-      let mp_mt = msid_of_mt mt in
-      let l,idl' = list_sep_last idl in
-      let mp_w =
-	List.fold_left (fun mp l -> MPdot(mp,label_of_id l)) mp_mt idl'
-      in
-      let r = ConstRef (make_con mp_w empty_dirpath (label_of_id l))
-      in
-      push_visible mp_mt None;
-      let s =
-	pp_module_type None mt ++ str " with type " ++
-	  pp_global Type r ++ ids
-      in
-      pop_visible();
-      s ++ str "=" ++ spc () ++ pp_type false vl typ
-  | MTwith(mt,ML_With_module(idl,mp)) ->
-      let mp_mt = msid_of_mt mt in
-      let mp_w =
-	List.fold_left (fun mp id -> MPdot(mp,label_of_id id)) mp_mt idl
-      in
-      push_visible mp_mt None;
-      let s =
-	pp_module_type None mt ++ str " with module " ++ pp_modname mp_w
-      in
-      pop_visible ();
-      s ++ str " = " ++ pp_modname mp
-
-let is_short = function MEident _ | MEapply _ -> true | _ -> false
-  
-let rec pp_structure_elem = function 
-  | (l,SEdecl d) -> 
-       (try 
-	 let ren = Common.check_duplicate (top_visible_mp ()) l in 
-	 hov 1 (str ("module "^ren^" = struct ") ++ fnl () ++ pp_decl d) ++
-	 fnl () ++ str "end" ++ fnl () ++
-	 pp_alias_decl ren d 
-	with Not_found -> pp_decl d)
-  | (l,SEmodule m) ->
-      let typ =
-        (* virtual printing of the type, in order to have a correct mli later*)
-	if Common.get_phase () = Pre then
-	  str ": " ++ pp_module_type (Some l) m.ml_mod_type
-	else mt ()
-      in
-      let def = pp_module_expr (Some l) m.ml_mod_expr in 
-      let name = pp_modname (MPdot (top_visible_mp (), l)) in 
-      hov 1 
-	(str "module " ++ name ++ typ ++ str " = " ++ 
-	 (if (is_short m.ml_mod_expr) then mt () else fnl ()) ++ def) ++ 
-      (try 
-	 let ren = Common.check_duplicate (top_visible_mp ()) l in 
-	 fnl () ++ str ("module "^ren^" = ") ++ name
-       with Not_found -> mt ())
-  | (l,SEmodtype m) -> 
-      let def = pp_module_type None m in 
-      let name = pp_modname (MPdot (top_visible_mp (), l)) in 
-      hov 1 (str "module type " ++ name ++ str " = " ++ fnl () ++ def) ++
-      (try 
-	 let ren = Common.check_duplicate (top_visible_mp ()) l in 
-         fnl () ++ str ("module type "^ren^" = ") ++ name
-       with Not_found -> mt ())
-
-and pp_module_expr ol = function 
-  | MEident mp' -> pp_modname mp'
-  | MEfunctor (mbid, mt, me) -> 
-      let name = pp_modname (MPbound mbid) in
-      let typ = pp_module_type None mt in 
-      let def = pp_module_expr None me in 
-      str "functor (" ++ name ++ str ":" ++ typ ++ str ") ->" ++ fnl () ++ def
-  | MEapply (me, me') -> 
-      pp_module_expr None me ++ str "(" ++ pp_module_expr None me' ++ str ")"
-  | MEstruct (msid, sel) -> 
-      let tvm = top_visible_mp () in 
-      let mp = match ol with None -> MPself msid | Some l -> MPdot (tvm,l) in
-      (* No need to update the subst with [Some msid] below : names are
-	 already in long form (see [subst_structure] in [Extract_env]). *)
-      push_visible mp None; 
-      let l = map_succeed pp_structure_elem sel in 
-      pop_visible (); 
-      str "struct " ++ fnl () ++
-      v 1 (str " " ++ prlist_with_sep fnl2 identity l) ++ 
-      fnl () ++ str "end" 
-
-let do_struct f s =
-  let pp s = try f s ++ fnl2 () with Failure "empty phrase" -> mt ()
-  in
-  let ppl (mp,sel) =
-    push_visible mp None;
-    let p = prlist_strict pp sel in
-    (* for monolithic extraction, we try to simulate the unavailability
-       of [MPfile] in names by artificially nesting these [MPfile] *)
-    (if modular () then pop_visible ()); p
-  in
-  let p = prlist_strict ppl s in
-  (if not (modular ()) then repeat (List.length s) pop_visible ());
-  p
-
-let pp_struct s = do_struct pp_structure_elem s
-
-let pp_signature s = do_struct pp_specif s
-
-let pp_decl d = try pp_decl d with Failure "empty phrase" -> mt ()
-
-let ocaml_descr = {
-  keywords = keywords;  
-  file_suffix = ".ml"; 
-  capital_file = false;  
-  preamble = preamble; 
-  pp_struct = pp_struct; 
-  sig_suffix = Some ".mli";  
-  sig_preamble = sig_preamble; 
-  pp_sig = pp_signature;
-  pp_decl = pp_decl; 
-}
-
-
diff --git a/contrib/extraction/ocaml.mli b/contrib/extraction/ocaml.mli
deleted file mode 100644
index 3d90e74c..00000000
--- a/contrib/extraction/ocaml.mli
+++ /dev/null
@@ -1,12 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(*i $Id: ocaml.mli 10232 2007-10-17 12:32:10Z letouzey $ i*)
-
-val ocaml_descr : Miniml.language_descr 
-
diff --git a/contrib/extraction/scheme.ml b/contrib/extraction/scheme.ml
deleted file mode 100644
index f4941a9c..00000000
--- a/contrib/extraction/scheme.ml
+++ /dev/null
@@ -1,202 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(*i $Id: scheme.ml 11559 2008-11-07 22:03:34Z letouzey $ i*)
-
-(*s Production of Scheme syntax. *)
-
-open Pp
-open Util
-open Names
-open Nameops
-open Libnames
-open Miniml
-open Mlutil
-open Table
-open Common
-
-(*s Scheme renaming issues. *)
-
-let keywords =     
-  List.fold_right (fun s -> Idset.add (id_of_string s))
-    [ "define"; "let"; "lambda"; "lambdas"; "match"; 
-      "apply"; "car"; "cdr"; 
-      "error"; "delay"; "force"; "_"; "__"] 
-    Idset.empty
-
-let preamble _ _ usf = 
-  str ";; This extracted scheme code relies on some additional macros\n" ++ 
-  str ";; available at http://www.pps.jussieu.fr/~letouzey/scheme\n" ++
-  str "(load \"macros_extr.scm\")\n\n" ++
-  (if usf.mldummy then str "(define __ (lambda (_) __))\n\n" else mt ())
-
-let pr_id id = 
-  let s = string_of_id id in
-  for i = 0 to String.length s - 1 do 
-    if s.[i] = '\'' then s.[i] <- '~'
-  done; 
-  str s
-
-let paren = pp_par true
-
-let pp_abst st = function 
-  | [] -> assert false
-  | [id] -> paren (str "lambda " ++ paren (pr_id id) ++ spc () ++ st)
-  | l -> paren 
-	(str "lambdas " ++ paren (prlist_with_sep spc pr_id l) ++ spc () ++ st)
-
-let pp_apply st _ = function 
-  | [] -> st 
-  | [a] -> hov 2 (paren (st ++ spc () ++ a))
-  | args -> hov 2 (paren (str "@ " ++ st ++ 
-			  (prlist_strict (fun x -> spc () ++ x) args)))
-
-(*s The pretty-printer for Scheme syntax *)
-
-let pp_global k r = str (Common.pp_global k r)
-
-(*s Pretty-printing of expressions.  *)
-
-let rec pp_expr env args = 
-  let apply st = pp_apply st true args in 
-  function
-    | MLrel n -> 
-	let id = get_db_name n env in apply (pr_id id)
-    | MLapp (f,args') ->
-	let stl = List.map (pp_expr env []) args' in
-        pp_expr env (stl @ args) f
-    | MLlam _ as a -> 
-      	let fl,a' = collect_lams a in
-	let fl,env' = push_vars fl env in
-	apply (pp_abst (pp_expr env' [] a') (List.rev fl))
-    | MLletin (id,a1,a2) ->
-	let i,env' = push_vars [id] env in
-	apply 
-	  (hv 0 
-	     (hov 2 
-		(paren 
-		   (str "let " ++ 
-		    paren 
-		      (paren 
-			 (pr_id (List.hd i) ++ spc () ++ pp_expr env [] a1)) 
-		    ++ spc () ++ hov 0 (pp_expr env' [] a2)))))
-    | MLglob r -> 
-	apply (pp_global Term r)
-    | MLcons (i,r,args') ->
-	assert (args=[]);
-	let st = 
-	  str "`" ++ 
-	  paren (pp_global Cons r ++ 
-		 (if args' = [] then mt () else spc ()) ++
-		 prlist_with_sep spc (pp_cons_args env) args')
-	in 
-	if i = Coinductive then paren (str "delay " ++ st) else st 
-    | MLcase ((i,_),t, pv) ->
-	let e = 
-	  if i <> Coinductive then pp_expr env [] t 	
-	  else paren (str "force" ++ spc () ++ pp_expr env [] t)
-	in 
-	apply (v 3 (paren (str "match " ++ e ++ fnl () ++ pp_pat env pv)))
-    | MLfix (i,ids,defs) ->
-	let ids',env' = push_vars (List.rev (Array.to_list ids)) env in
-      	pp_fix env' i (Array.of_list (List.rev ids'),defs) args
-    | MLexn s -> 
-	(* An [MLexn] may be applied, but I don't really care. *)
-	paren (str "error" ++ spc () ++ qs s)
-    | MLdummy ->
-	str "__" (* An [MLdummy] may be applied, but I don't really care. *)
-    | MLmagic a ->
-	pp_expr env args a
-    | MLaxiom -> paren (str "error \"AXIOM TO BE REALIZED\"")
-
-and pp_cons_args env = function 
-  | MLcons (i,r,args) when i<>Coinductive -> 
-      paren (pp_global Cons r ++ 
-	     (if args = [] then mt () else spc ()) ++
-	     prlist_with_sep spc (pp_cons_args env) args)
-  | e -> str "," ++ pp_expr env [] e
-	
-
-and pp_one_pat env (r,ids,t) = 
-  let ids,env' = push_vars (List.rev ids) env in
-  let args = 
-    if ids = [] then mt () 
-    else (str " " ++ prlist_with_sep spc pr_id (List.rev ids))
-  in 
-  (pp_global Cons r ++ args), (pp_expr env' [] t)
-  
-and pp_pat env pv = 
-  prvect_with_sep fnl  
-    (fun x -> let s1,s2 = pp_one_pat env x in 
-     hov 2 (str "((" ++ s1 ++ str ")" ++ spc () ++ s2 ++ str ")")) pv
-
-(*s names of the functions ([ids]) are already pushed in [env],
-    and passed here just for convenience. *)
-
-and pp_fix env j (ids,bl) args =
-    paren 
-      (str "letrec " ++
-       (v 0 (paren 
-	       (prvect_with_sep fnl
-		  (fun (fi,ti) -> 
-		     paren ((pr_id fi) ++ spc () ++ (pp_expr env [] ti)))
-		  (array_map2 (fun id b -> (id,b)) ids bl)) ++
-	     fnl () ++
-      	     hov 2 (pp_apply (pr_id (ids.(j))) true args))))
-
-(*s Pretty-printing of a declaration. *)
-
-let pp_decl = function
-  | Dind _ -> mt ()
-  | Dtype _ -> mt () 
-  | Dfix (rv, defs,_) ->
-      let ppv = Array.map (pp_global Term) rv in 
-      prvect_with_sep fnl 
-	(fun (pi,ti) -> 
-	   hov 2 
-	     (paren (str "define " ++ pi ++ spc () ++ 
-		     (pp_expr (empty_env ()) [] ti)) 
-	      ++ fnl ()))
-	(array_map2 (fun p b -> (p,b)) ppv defs) ++
-      fnl ()
-  | Dterm (r, a, _) ->
-      if is_inline_custom r then mt () 
-      else 
-	if is_custom r then 
-	  hov 2 (paren (str "define " ++ pp_global Term r ++ spc () ++ 
-			  str (find_custom r))) ++ fnl () ++ fnl () 
-	else 
-	  hov 2 (paren (str "define " ++ pp_global Term r ++ spc () ++
-			  pp_expr (empty_env ()) [] a)) ++ fnl () ++ fnl ()
-
-let pp_structure_elem = function 
-  | (l,SEdecl d) -> pp_decl d
-  | (l,SEmodule m) -> 
-      failwith "TODO: Scheme extraction of modules not implemented yet"
-  | (l,SEmodtype m) -> 
-      failwith "TODO: Scheme extraction of modules not implemented yet"
-
-let pp_struct = 
-  let pp_sel (mp,sel) = 
-    push_visible mp None; 
-    let p = prlist_strict pp_structure_elem sel in 
-    pop_visible (); p
-  in
-  prlist_strict pp_sel
-
-let scheme_descr = {
-  keywords = keywords;  
-  file_suffix = ".scm"; 
-  capital_file = false;  
-  preamble = preamble; 
-  pp_struct = pp_struct; 
-  sig_suffix = None;
-  sig_preamble = (fun _ _ _ -> mt ()); 
-  pp_sig = (fun _ -> mt ()); 
-  pp_decl = pp_decl; 
-}
diff --git a/contrib/extraction/scheme.mli b/contrib/extraction/scheme.mli
deleted file mode 100644
index a88bb6db..00000000
--- a/contrib/extraction/scheme.mli
+++ /dev/null
@@ -1,11 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(*i $Id: scheme.mli 10232 2007-10-17 12:32:10Z letouzey $ i*)
-
-val scheme_descr : Miniml.language_descr 
diff --git a/contrib/extraction/table.ml b/contrib/extraction/table.ml
deleted file mode 100644
index c675a744..00000000
--- a/contrib/extraction/table.ml
+++ /dev/null
@@ -1,653 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(*i $Id: table.ml 11844 2009-01-22 16:45:06Z letouzey $ i*)
-
-open Names
-open Term
-open Declarations
-open Nameops
-open Summary
-open Libobject
-open Goptions
-open Libnames
-open Util
-open Pp
-open Miniml
-
-(*S Utilities about [module_path] and [kernel_names] and [global_reference] *)
-
-let occur_kn_in_ref kn = function
-  | IndRef (kn',_)
-  | ConstructRef ((kn',_),_) -> kn = kn'
-  | ConstRef _ -> false
-  | VarRef _ -> assert false
-      
-let modpath_of_r = function 
-  | ConstRef kn -> con_modpath kn
-  | IndRef (kn,_)
-  | ConstructRef ((kn,_),_) -> modpath kn
-  | VarRef _ -> assert false
-      
-let label_of_r = function 
-  | ConstRef kn -> con_label kn
-  | IndRef (kn,_)
-  | ConstructRef ((kn,_),_) -> label kn
-  | VarRef _ -> assert false
-
-let rec base_mp = function 
-  | MPdot (mp,l) -> base_mp mp 
-  | mp -> mp 
-
-let rec mp_length = function
-  | MPdot (mp, _) -> 1 + (mp_length mp)
-  | _ -> 1
-
-let is_modfile = function 
-  | MPfile _ -> true 
-  | _ -> false
-
-let raw_string_of_modfile = function
-  | MPfile f -> String.capitalize (string_of_id (List.hd (repr_dirpath f)))
-  | _ -> assert false
-
-let rec modfile_of_mp = function 
-  | (MPfile _) as mp -> mp
-  | MPdot (mp,_) -> modfile_of_mp mp 
-  | _ -> raise Not_found
-
-let current_toplevel () = fst (Lib.current_prefix ())
-
-let is_toplevel mp = 
-  mp = initial_path || mp = current_toplevel ()
-
-let at_toplevel mp = 
-  is_modfile mp || is_toplevel mp
-
-let visible_kn kn = at_toplevel (base_mp (modpath kn))
-let visible_con kn = at_toplevel (base_mp (con_modpath kn))
-
-let rec prefixes_mp mp = match mp with 
-  | MPdot (mp',_) -> MPset.add mp (prefixes_mp mp')
-  | _ -> MPset.singleton mp 
-
-let rec get_nth_label_mp n = function
-  | MPdot (mp,l) -> if n=1 then l else get_nth_label_mp (n-1) mp
-  | _ -> failwith "get_nth_label: not enough MPdot"
-
-let common_prefix_from_list mp0 mpl = 
-  let prefixes = prefixes_mp mp0 in 
-  let rec f = function 
-    | [] -> raise Not_found
-    | mp :: l -> if MPset.mem mp prefixes then mp else f l 
-  in f mpl
-
-let rec parse_labels ll = function 
-  | MPdot (mp,l) -> parse_labels (l::ll) mp 
-  | mp -> mp,ll
-
-let labels_of_mp mp = parse_labels [] mp 
-
-let labels_of_ref r = 
- let mp,_,l =
-  match r with
-     ConstRef con -> repr_con con
-   | IndRef (kn,_)
-   | ConstructRef ((kn,_),_) -> repr_kn kn
-   | VarRef _ -> assert false
- in
-  parse_labels [l] mp
-
-let rec add_labels_mp mp = function 
-  | [] -> mp 
-  | l :: ll -> add_labels_mp (MPdot (mp,l)) ll
-
-
-(*S The main tables: constants, inductives, records, ... *)
-
-(* Theses tables are not registered within coq save/undo mechanism 
-   since we reset their contents at each run of Extraction *)
-
-(*s Constants tables. *) 
-
-let terms = ref (Cmap.empty : ml_decl Cmap.t)
-let init_terms () = terms := Cmap.empty
-let add_term kn d = terms := Cmap.add kn d !terms
-let lookup_term kn = Cmap.find kn !terms
-
-let types = ref (Cmap.empty : ml_schema Cmap.t)
-let init_types () = types := Cmap.empty
-let add_type kn s = types := Cmap.add kn s !types
-let lookup_type kn = Cmap.find kn !types 
-
-(*s Inductives table. *)
-
-let inductives = ref (KNmap.empty : (mutual_inductive_body * ml_ind) KNmap.t)
-let init_inductives () = inductives := KNmap.empty
-let add_ind kn mib ml_ind = inductives := KNmap.add kn (mib,ml_ind) !inductives
-let lookup_ind kn = KNmap.find kn !inductives
-
-(*s Recursors table. *)
-
-let recursors = ref Cset.empty
-let init_recursors () = recursors := Cset.empty
-
-let add_recursors env kn = 
-  let make_kn id = make_con (modpath kn) empty_dirpath (label_of_id id) in 
-  let mib = Environ.lookup_mind kn env in 
-  Array.iter 
-    (fun mip -> 
-       let id = mip.mind_typename in 
-       let kn_rec = make_kn (Nameops.add_suffix id "_rec")
-       and kn_rect = make_kn (Nameops.add_suffix id "_rect") in 
-       recursors := Cset.add kn_rec (Cset.add kn_rect !recursors))
-    mib.mind_packets
-
-let is_recursor = function 
-  | ConstRef kn -> Cset.mem kn !recursors
-  | _ -> false
-
-(*s Record tables. *)
-
-let projs = ref (Refmap.empty : int Refmap.t)
-let init_projs () = projs := Refmap.empty
-let add_projection n kn = projs := Refmap.add (ConstRef kn) n !projs
-let is_projection r = Refmap.mem r !projs
-let projection_arity r = Refmap.find r !projs
-
-(*s Table of used axioms *)
-
-let info_axioms = ref Refset.empty
-let log_axioms = ref Refset.empty
-let init_axioms () = info_axioms := Refset.empty; log_axioms := Refset.empty
-let add_info_axiom r = info_axioms := Refset.add r !info_axioms
-let remove_info_axiom r = info_axioms := Refset.remove r !info_axioms
-let add_log_axiom r = log_axioms := Refset.add r !log_axioms
-
-(*s Extraction mode: modular or monolithic *)
-
-let modular_ref = ref false
-
-let set_modular b = modular_ref := b
-let modular () = !modular_ref
-
-(*s Printing. *)
-
-(* The following functions work even on objects not in [Global.env ()].
-   WARNING: for inductive objects, an extract_inductive must have been 
-   done before. *)
-
-let safe_id_of_global = function 
-  | ConstRef kn -> let _,_,l = repr_con kn in id_of_label l
-  | IndRef (kn,i) -> (snd (lookup_ind kn)).ind_packets.(i).ip_typename
-  | ConstructRef ((kn,i),j) -> 
-      (snd (lookup_ind kn)).ind_packets.(i).ip_consnames.(j-1)
-  | _ -> assert false
-
-let safe_pr_global r =
- try Printer.pr_global r
- with _ -> pr_id (safe_id_of_global r)
-
-(* idem, but with qualification, and only for constants. *)
-
-let safe_pr_long_global r =
-  try Printer.pr_global r
-  with _ -> match r with
-    | ConstRef kn ->
-	let mp,_,l = repr_con kn in
-	str ((string_of_mp mp)^"."^(string_of_label l))
-    | _ -> assert false
-
-let pr_long_mp mp =
-  let lid = repr_dirpath (Nametab.dir_of_mp mp) in
-  str (String.concat "." (List.map string_of_id (List.rev lid)))
-
-let pr_long_global ref = pr_sp (Nametab.sp_of_global ref)
-
-(*S Warning and Error messages. *)
-
-let err s = errorlabstrm "Extraction" s
-
-let warning_axioms () = 
-  let info_axioms = Refset.elements !info_axioms in 
-  if info_axioms = [] then () 
-  else begin
-    let s = if List.length info_axioms = 1 then "axiom" else "axioms" in 
-    msg_warning 
-      (str ("The following "^s^" must be realized in the extracted code:")
-       ++ hov 1 (spc () ++ prlist_with_sep spc safe_pr_global info_axioms)
-       ++ str "." ++ fnl ())
-  end;
-  let log_axioms = Refset.elements !log_axioms in 
-  if log_axioms = [] then ()
-  else begin
-    let s = if List.length log_axioms = 1 then "axiom was" else "axioms were" 
-    in 
-    msg_warning
-      (str ("The following logical "^s^" encountered:") ++
-       hov 1
-         (spc () ++ prlist_with_sep spc safe_pr_global log_axioms ++ str ".\n")
-       ++
-       str "Having invalid logical axiom in the environment when extracting" ++
-       spc () ++ str "may lead to incorrect or non-terminating ML terms." ++
-       fnl ())
-  end
-
-let warning_both_mod_and_cst q mp r =
- msg_warning
-   (str "The name " ++ pr_qualid q ++ str " is ambiguous, " ++
-    str "do you mean module " ++
-    pr_long_mp mp ++
-    str " or object " ++
-    pr_long_global r ++ str " ?" ++ fnl () ++
-    str "First choice is assumed, for the second one please use " ++
-    str "fully qualified name." ++ fnl ())
-
-let error_axiom_scheme r i = 
-  err (str "The type scheme axiom " ++ spc () ++
-       safe_pr_global r ++ spc () ++ str "needs " ++ pr_int i ++ 
-       str " type variable(s).") 
-
-let check_inside_module () = 
-  if Lib.is_modtype () then 
-    err (str "You can't do that within a Module Type." ++ fnl () ++
-	 str "Close it and try again.") 
-  else if Lib.is_module () then 
-    msg_warning
-      (str "Extraction inside an opened module is experimental.\n" ++
-       str "In case of problem, close it first.\n")
-
-let check_inside_section () = 
-  if Lib.sections_are_opened () then 
-    err (str "You can't do that within a section." ++ fnl () ++
-	 str "Close it and try again.")
-
-let error_constant r = 
-  err (safe_pr_global r ++ str " is not a constant.") 
-
-let error_inductive r = 
-  err (safe_pr_global r ++ spc () ++ str "is not an inductive type.")
-
-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") ++ 
-       str "This is not supported yet. Please do some renaming first.") 
-
-let error_unknown_module m = 
-  err (str "Module" ++ spc () ++ pr_qualid m ++ spc () ++ str "not found.") 
-
-let error_scheme () = 
-  err (str "No Scheme modular extraction available yet.")
-
-let error_not_visible r = 
-  err (safe_pr_global r ++ str " is not directly visible.\n" ++
-       str "For example, it may be inside an applied functor." ++
-       str "Use Recursive Extraction to get the whole environment.")
-
-let error_MPfile_as_mod mp b = 
-  let s1 = if b then "asked" else "required" in 
-  let s2 = if b then "extract some objects of this module or\n" else "" in
-  err (str ("Extraction of file "^(raw_string_of_modfile mp)^
-	    ".v as a module is "^s1^".\n"^
-	    "Monolithic Extraction cannot deal with this situation.\n"^
-	    "Please "^s2^"use (Recursive) Extraction Library instead.\n"))
-
-let error_record r =
-  err (str "Record " ++ safe_pr_global r ++ str " has an anonymous field." ++
-       fnl () ++ str "To help extraction, please use an explicit name.")
-
-let check_loaded_modfile mp = match base_mp mp with 
-  | MPfile dp -> if not (Library.library_is_loaded dp) then 
-      err (str ("Please load library "^(string_of_dirpath dp^" first.")))
-  | _ -> ()
-
-let info_file f =   
-  Flags.if_verbose message 
-    ("The file "^f^" has been created by extraction.")
-
-
-(*S The Extraction auxiliary commands *)
-
-(* The objects defined below should survive an arbitrary time, 
-   so we register them to coq save/undo mechanism. *)
-
-(*s Extraction AutoInline *)
-
-let auto_inline_ref = ref true
-
-let auto_inline () = !auto_inline_ref
-
-let _ = declare_bool_option 
-	  {optsync = true;
-	   optname = "Extraction AutoInline";
-	   optkey = SecondaryTable ("Extraction", "AutoInline");
-	   optread = auto_inline; 
-	   optwrite = (:=) auto_inline_ref}
-
-(*s Extraction TypeExpand *)
-
-let type_expand_ref = ref true
-
-let type_expand () = !type_expand_ref
-
-let _ = declare_bool_option 
-	  {optsync = true;
-	   optname = "Extraction TypeExpand";
-	   optkey = SecondaryTable ("Extraction", "TypeExpand");
-	   optread = type_expand; 
-	   optwrite = (:=) type_expand_ref}
-
-(*s Extraction Optimize *)
-
-type opt_flag = 
-    { opt_kill_dum : bool; (* 1 *) 
-      opt_fix_fun : bool;   (* 2 *)
-      opt_case_iot : bool;  (* 4 *)
-      opt_case_idr : bool;  (* 8 *)
-      opt_case_idg : bool;  (* 16 *)
-      opt_case_cst : bool;  (* 32 *)
-      opt_case_fun : bool;  (* 64 *)
-      opt_case_app : bool;  (* 128 *)
-      opt_let_app : bool;   (* 256 *)
-      opt_lin_let : bool;   (* 512 *)
-      opt_lin_beta : bool } (* 1024 *)
-
-let kth_digit n k = (n land (1 lsl k) <> 0)
-
-let flag_of_int n = 
-    { opt_kill_dum = kth_digit n 0;
-      opt_fix_fun = kth_digit n 1;
-      opt_case_iot = kth_digit n 2;
-      opt_case_idr = kth_digit n 3;
-      opt_case_idg = kth_digit n 4; 
-      opt_case_cst = kth_digit n 5;
-      opt_case_fun = kth_digit n 6;
-      opt_case_app = kth_digit n 7;
-      opt_let_app = kth_digit n 8;
-      opt_lin_let = kth_digit n 9;
-      opt_lin_beta = kth_digit n 10 }
-
-(* For the moment, we allow by default everything except the type-unsafe 
-   optimization [opt_case_idg]. *)
-
-let int_flag_init = 1 + 2 + 4 + 8 + 32 + 64 + 128 + 256 + 512 + 1024
-
-let int_flag_ref = ref int_flag_init
-let opt_flag_ref = ref (flag_of_int int_flag_init)
-
-let chg_flag n = int_flag_ref := n; opt_flag_ref := flag_of_int n
-
-let optims () = !opt_flag_ref
-
-let _ = declare_bool_option 
-	  {optsync = true; 
-	   optname = "Extraction Optimize";
-	   optkey = SecondaryTable ("Extraction", "Optimize");
-	   optread = (fun () -> !int_flag_ref <> 0); 
-	   optwrite = (fun b -> chg_flag (if b then int_flag_init else 0))}
-
-let _ = declare_int_option
-          { optsync = true;
-            optname = "Extraction Flag";
-            optkey = SecondaryTable("Extraction","Flag"); 
-            optread = (fun _ -> Some !int_flag_ref); 
-            optwrite = (function 
-                          | None -> chg_flag 0
-                          | Some i -> chg_flag (max i 0))}
-
-
-(*s Extraction Lang *)
-
-type lang = Ocaml | Haskell | Scheme
-
-let lang_ref = ref Ocaml
-
-let lang () = !lang_ref
-
-let (extr_lang,_) = 
-  declare_object 
-    {(default_object "Extraction Lang") with  
-       cache_function = (fun (_,l) -> lang_ref := l);
-       load_function = (fun _ (_,l) -> lang_ref := l);
-       export_function = (fun x -> Some x)}
-
-let _ = declare_summary "Extraction Lang" 
-	  { freeze_function = (fun () -> !lang_ref);
-	    unfreeze_function = ((:=) lang_ref);
-	    init_function = (fun () -> lang_ref := Ocaml);
-	    survive_module = true;
-	    survive_section = true }  
-	  
-let extraction_language x = Lib.add_anonymous_leaf (extr_lang x)
-
-(*s Extraction Inline/NoInline *)
-
-let empty_inline_table = (Refset.empty,Refset.empty)
-
-let inline_table = ref empty_inline_table
-
-let to_inline r = Refset.mem r (fst !inline_table)
-
-let to_keep r = Refset.mem r (snd !inline_table)
-
-let add_inline_entries b l = 
-  let f b = if b then Refset.add else Refset.remove in 
-  let i,k = !inline_table in 
-  inline_table := 
-  (List.fold_right (f b) l i), 
-  (List.fold_right (f (not b)) l k)
-
-(* Registration of operations for rollback. *)
-
-let (inline_extraction,_) =
-  declare_object 
-    {(default_object "Extraction Inline") with 
-       cache_function = (fun (_,(b,l)) -> add_inline_entries b l);
-       load_function = (fun _ (_,(b,l)) -> add_inline_entries b l);
-       export_function = (fun x -> Some x); 
-       classify_function = (fun (_,o) -> Substitute o); 
-       subst_function =
-        (fun (_,s,(b,l)) -> (b,(List.map (fun x -> fst (subst_global s x)) l)))
-    }
-
-let _ = declare_summary "Extraction Inline"
-	  { freeze_function = (fun () -> !inline_table);
-	    unfreeze_function = ((:=) inline_table);
-	    init_function = (fun () -> inline_table := empty_inline_table);
-	    survive_module = true;
-	    survive_section = true }
-
-(* Grammar entries. *)
-
-let extraction_inline b l =
-  check_inside_section (); 
-  let refs = List.map Nametab.global l in 
-  List.iter 
-    (fun r -> match r with 
-       | ConstRef _ -> ()
-       | _ -> error_constant r) refs; 
-  Lib.add_anonymous_leaf (inline_extraction (b,refs))
-
-(* Printing part *)
-
-let print_extraction_inline () = 
-  let (i,n)= !inline_table in 
-  let i'= Refset.filter (function ConstRef _ -> true | _ -> false) i in 
-  msg 
-    (str "Extraction Inline:" ++ fnl () ++ 
-     Refset.fold
-       (fun r p -> 
-	  (p ++ str "  " ++ safe_pr_long_global r ++ fnl ())) i' (mt ()) ++
-     str "Extraction NoInline:" ++ fnl () ++ 
-     Refset.fold
-       (fun r p -> 
-	  (p ++ str "  " ++ safe_pr_long_global r ++ fnl ())) n (mt ()))
-
-(* Reset part *)
-
-let (reset_inline,_) = 
-  declare_object
-    {(default_object "Reset Extraction Inline") with  
-       cache_function = (fun (_,_)-> inline_table :=  empty_inline_table);
-       load_function = (fun _ (_,_)-> inline_table :=  empty_inline_table); 
-       export_function = (fun x -> Some x)}
-
-let reset_extraction_inline () = Lib.add_anonymous_leaf (reset_inline ())
-
-(*s Extraction Blacklist of filenames not to use while extracting *)
-
-let blacklist_table = ref Idset.empty
-
-let modfile_ids = ref []
-let modfile_mps = ref MPmap.empty
-
-let reset_modfile () =
-  modfile_ids := Idset.elements !blacklist_table;
-  modfile_mps := MPmap.empty
-
-let string_of_modfile mp =
-  try MPmap.find mp !modfile_mps
-  with Not_found ->
-    let id = id_of_string (raw_string_of_modfile mp) in
-    let id' = next_ident_away id !modfile_ids in
-    let s' = string_of_id id' in
-    modfile_ids := id' :: !modfile_ids;
-    modfile_mps := MPmap.add mp s' !modfile_mps;
-    s'
-
-let add_blacklist_entries l =
-  blacklist_table :=
-    List.fold_right (fun s -> Idset.add (id_of_string (String.capitalize s)))
-      l !blacklist_table
-
-(* Registration of operations for rollback. *)
-
-let (blacklist_extraction,_) =
-  declare_object
-    {(default_object "Extraction Blacklist") with
-       cache_function = (fun (_,l) -> add_blacklist_entries l);
-       load_function = (fun _ (_,l) -> add_blacklist_entries l);
-       export_function = (fun x -> Some x);
-       classify_function = (fun (_,o) -> Libobject.Keep o);
-       subst_function = (fun (_,_,x) -> x)
-    }
-
-let _ = declare_summary "Extraction Blacklist"
-	  { freeze_function = (fun () -> !blacklist_table);
-	    unfreeze_function = ((:=) blacklist_table);
-	    init_function = (fun () -> blacklist_table := Idset.empty);
-	    survive_module = true;
-	    survive_section = true }
-
-(* Grammar entries. *)
-
-let extraction_blacklist l =
-  let l = List.rev_map string_of_id l in
-  Lib.add_anonymous_leaf (blacklist_extraction l)
-
-(* Printing part *)
-
-let print_extraction_blacklist () =
-  msgnl
-    (prlist_with_sep fnl pr_id (Idset.elements !blacklist_table))
-
-(* Reset part *)
-
-let (reset_blacklist,_) =
-  declare_object
-    {(default_object "Reset Extraction Blacklist") with
-       cache_function = (fun (_,_)-> blacklist_table := Idset.empty);
-       load_function = (fun _ (_,_)-> blacklist_table := Idset.empty);
-       export_function = (fun x -> Some x)}
-
-let reset_extraction_blacklist () = Lib.add_anonymous_leaf (reset_blacklist ())
-
-(*s Extract Constant/Inductive. *)
-
-(* UGLY HACK: to be defined in [extraction.ml] *)
-let use_type_scheme_nb_args, register_type_scheme_nb_args = 
-  let r = ref (fun _ _ -> 0) in (fun x y -> !r x y), (:=) r 
-
-let customs = ref Refmap.empty
-
-let add_custom r ids s = customs := Refmap.add r (ids,s) !customs
-
-let is_custom r = Refmap.mem r !customs
-
-let is_inline_custom r = (is_custom r) && (to_inline r) 
-
-let find_custom r = snd (Refmap.find r !customs)
-
-let find_type_custom r = Refmap.find r !customs
-
-(* Registration of operations for rollback. *)
-
-let (in_customs,_) = 
-  declare_object 
-    {(default_object "ML extractions") with 
-       cache_function = (fun (_,(r,ids,s)) -> add_custom r ids s);
-       load_function = (fun _ (_,(r,ids,s)) -> add_custom r ids s);
-       export_function = (fun x -> Some x); 
-       classify_function = (fun (_,o) -> Substitute o); 
-       subst_function =
-        (fun (_,s,(r,ids,str)) -> (fst (subst_global s r), ids, str))
-    }
-
-let _ = declare_summary "ML extractions"
-	  { freeze_function = (fun () -> !customs);
-	    unfreeze_function = ((:=) customs);
-	    init_function = (fun () -> customs := Refmap.empty);
-	    survive_module = true;
-	    survive_section = true }
-
-(* Grammar entries. *)
-
-let extract_constant_inline inline r ids s =
-  check_inside_section ();
-  let g = Nametab.global r in 
-  match g with 
-    | ConstRef kn -> 
-	let env = Global.env () in 
-	let typ = Typeops.type_of_constant env kn in 
-	let typ = Reduction.whd_betadeltaiota env typ in
-	if Reduction.is_arity env typ 
-	  then begin 
-	    let nargs = use_type_scheme_nb_args env typ in 
-	    if List.length ids <> nargs then error_axiom_scheme g nargs
-	  end; 
-	Lib.add_anonymous_leaf (inline_extraction (inline,[g]));
-	Lib.add_anonymous_leaf (in_customs (g,ids,s))
-    | _ -> error_constant g
-
-
-let extract_inductive r (s,l) =
-  check_inside_section ();
-  let g = Nametab.global r in 
-  match g with
-    | IndRef ((kn,i) as ip) ->
-	let mib = Global.lookup_mind kn in
-	let n = Array.length mib.mind_packets.(i).mind_consnames in
-	if n <> List.length l then error_nb_cons (); 
-	Lib.add_anonymous_leaf (inline_extraction (true,[g]));
-	Lib.add_anonymous_leaf (in_customs (g,[],s));
-	list_iter_i
-	  (fun j s -> 
-	     let g = ConstructRef (ip,succ j) in 
-	     Lib.add_anonymous_leaf (inline_extraction (true,[g]));
-	     Lib.add_anonymous_leaf (in_customs (g,[],s))) l
-    | _ -> error_inductive g 
-
-
-
-(*s Tables synchronization. *)
-
-let reset_tables () =
-  init_terms (); init_types (); init_inductives (); init_recursors ();
-  init_projs (); init_axioms (); reset_modfile ()
diff --git a/contrib/extraction/table.mli b/contrib/extraction/table.mli
deleted file mode 100644
index 5ef7139e..00000000
--- a/contrib/extraction/table.mli
+++ /dev/null
@@ -1,151 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(*i $Id: table.mli 11844 2009-01-22 16:45:06Z letouzey $ i*)
-
-open Names
-open Libnames
-open Miniml
-open Declarations
-
-val safe_id_of_global : global_reference -> identifier
-
-(*s Warning and Error messages. *)
-
-val warning_axioms : unit -> unit
-val warning_both_mod_and_cst :
- qualid -> module_path -> global_reference -> 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_unknown_module : qualid -> 'a
-val error_scheme : unit -> 'a
-val error_not_visible : global_reference -> 'a
-val error_MPfile_as_mod : module_path -> bool -> 'a
-val error_record : global_reference -> 'a 
-val check_inside_module : unit -> unit
-val check_inside_section : unit -> unit
-val check_loaded_modfile : module_path -> unit
-
-val info_file : string -> unit
-
-(*s utilities about [module_path] and [kernel_names] and [global_reference] *)
-
-val occur_kn_in_ref : kernel_name -> global_reference -> bool
-val modpath_of_r : global_reference -> module_path
-val label_of_r : global_reference -> label
-val current_toplevel : unit -> module_path
-val base_mp : module_path -> module_path
-val is_modfile : module_path -> bool
-val string_of_modfile : module_path -> string 
-val is_toplevel : module_path -> bool
-val at_toplevel : module_path -> bool 
-val visible_kn : kernel_name -> bool
-val visible_con : constant -> bool
-val mp_length : module_path -> int
-val prefixes_mp : module_path -> MPset.t
-val modfile_of_mp : module_path -> module_path
-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
-
-(*s Some table-related operations *)
-
-val add_term : constant -> ml_decl -> unit
-val lookup_term : constant -> ml_decl
-
-val add_type : constant -> ml_schema -> unit
-val lookup_type : constant -> ml_schema
-
-val add_ind : kernel_name -> mutual_inductive_body -> ml_ind -> unit
-val lookup_ind : kernel_name -> mutual_inductive_body * ml_ind
-
-val add_recursors : Environ.env -> kernel_name -> unit
-val is_recursor : global_reference -> bool 
-
-val add_projection : int -> constant -> unit
-val is_projection : global_reference -> bool 
-val projection_arity : global_reference -> int
-
-val add_info_axiom : global_reference -> unit
-val remove_info_axiom : global_reference -> unit
-val add_log_axiom : global_reference -> unit
-
-val reset_tables : unit -> unit
-
-(*s AutoInline parameter *) 
-
-val auto_inline : unit -> bool
-
-(*s TypeExpand parameter *) 
-
-val type_expand : unit -> bool
-
-(*s Optimize parameter *) 
-
-type opt_flag = 
-    { opt_kill_dum : bool; (* 1 *) 
-      opt_fix_fun : bool;   (* 2 *)
-      opt_case_iot : bool;  (* 4 *)
-      opt_case_idr : bool;  (* 8 *)
-      opt_case_idg : bool;  (* 16 *)
-      opt_case_cst : bool;  (* 32 *)
-      opt_case_fun : bool;  (* 64 *)
-      opt_case_app : bool;  (* 128 *)
-      opt_let_app : bool;   (* 256 *)
-      opt_lin_let : bool;   (* 512 *)
-      opt_lin_beta : bool } (* 1024 *)
-
-val optims :  unit -> opt_flag
-
-(*s Target language. *)
-
-type lang = Ocaml | Haskell | Scheme
-val lang : unit -> lang 
-
-(*s Extraction mode: modular or monolithic *)
-
-val set_modular : bool -> unit
-val modular : unit -> bool 
-
-(*s Table for custom inlining *) 
-
-val to_inline : global_reference -> bool
-val to_keep : global_reference -> bool
-
-(*s Table for user-given custom ML extractions. *)
-
-(* UGLY HACK: registration of a function defined in [extraction.ml] *)
-val register_type_scheme_nb_args : (Environ.env -> Term.constr -> int) -> unit
-
-val is_custom : global_reference -> bool
-val is_inline_custom : global_reference -> bool
-val find_custom : global_reference -> string
-val find_type_custom : global_reference -> string list * string
-
-(*s Extraction commands. *)
-
-val extraction_language : lang -> unit
-val extraction_inline : bool -> reference list -> unit
-val print_extraction_inline : unit -> unit
-val reset_extraction_inline : unit -> unit
-val extract_constant_inline : 
-  bool -> reference -> string list -> string -> unit
-val extract_inductive : reference -> string * string list -> unit
-
-(*s Table of blacklisted filenames *)
-
-val extraction_blacklist : identifier list -> unit
-val reset_extraction_blacklist : unit -> unit
-val print_extraction_blacklist : unit -> unit
-
-
-