Imported Upstream version 8.3.pl2upstream/8.3.pl2

13 files changed, 267 insertions, 164 deletions

diff --git a/plugins/dp/dp_why.ml b/plugins/dp/dp_why.ml
index 9a62f39d..199c3087 100644
--- a/plugins/dp/dp_why.ml
+++ b/plugins/dp/dp_why.ml
@@ -181,6 +181,5 @@ let print_query fmt (decls,concl) =
 let output_file f q =
   let c = open_out f in
   let fmt = formatter_of_out_channel c in
-  fprintf fmt "include \"real.why\"@.";
   fprintf fmt "@[%a@]@." print_query q;
   close_out c
diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml
index 8dc512fa..9cea0562 100644
--- a/plugins/extraction/common.ml
+++ b/plugins/extraction/common.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: common.ml 13420 2010-09-16 15:47:08Z letouzey $ i*)
+(*i $Id: common.ml 14010 2011-04-15 16:05:07Z letouzey $ i*)
 
 open Pp
 open Util
@@ -43,6 +43,13 @@ let pr_binding = function
   | [] -> mt ()
   | l  -> str " " ++ prlist_with_sep (fun () -> str " ") pr_id l
 
+(** By default, in module Format, you can do horizontal placing of blocks
+    even if they include newlines, as long as the number of chars in the
+    blocks are less that a line length. To avoid this awkward situation,
+    we attach a big virtual size to [fnl] newlines. *)
+
+let fnl () = stras (1000000,"") ++ fnl ()
+
 let fnl2 () = fnl () ++ fnl ()
 
 let space_if = function true -> str " " | false -> mt ()
@@ -509,8 +516,10 @@ let pp_ocaml_gen k mp rls olab =
 let pp_haskell_gen k mp rls = match rls with
   | [] -> assert false
   | s::rls' ->
-      (if base_mp mp <> top_visible_mp () then s ^ "." else "") ^
-	(if upperkind k then "" else "_") ^ pseudo_qualify rls'
+    let str = pseudo_qualify rls' in
+    let str = if is_upper str && not (upperkind k) then ("_"^str) else str in
+    let prf = if base_mp mp <> top_visible_mp () then s ^ "." else "" in
+    prf ^ str
 
 (* Main name printing function for a reference *)
 
@@ -542,4 +551,38 @@ let pp_module mp =
 	add_visible (Mod,s) l; s
     | _ -> pp_ocaml_gen Mod mp (List.rev ls) None
 
+(** Special hack for constants of type Ascii.ascii : if an
+    [Extract Inductive ascii => char] has been declared, then
+    the constants are directly turned into chars *)
+
+let mk_ind path s =
+  make_mind (MPfile (dirpath_of_string path)) empty_dirpath (mk_label s)
 
+let ind_ascii = mk_ind "Coq.Strings.Ascii" "ascii"
+
+let check_extract_ascii () =
+  try
+    let char_type = match lang () with
+      | Ocaml -> "char"
+      | Haskell -> "Char"
+      | _ -> raise Not_found
+    in
+    find_custom (IndRef (ind_ascii,0)) = char_type
+  with Not_found -> false
+
+let is_list_cons l =
+ List.for_all (function MLcons (_,ConstructRef(_,_),[]) -> true | _ -> false) l
+
+let is_native_char = function
+  | MLcons(_,ConstructRef ((kn,0),1),l) ->
+    kn = ind_ascii && check_extract_ascii () && is_list_cons l
+  | _ -> false
+
+let pp_native_char c =
+  let rec cumul = function
+    | [] -> 0
+    | MLcons(_,ConstructRef(_,j),[])::l -> (2-j) + 2 * (cumul l)
+    | _ -> assert false
+  in
+  let l = match c with MLcons(_,_,l) -> l | _ -> assert false in
+  str ("'"^Char.escaped (Char.chr (cumul l))^"'")
diff --git a/plugins/extraction/common.mli b/plugins/extraction/common.mli
index 619cddfb..f6ff76ba 100644
--- a/plugins/extraction/common.mli
+++ b/plugins/extraction/common.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: common.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: common.mli 14010 2011-04-15 16:05:07Z letouzey $ i*)
 
 open Names
 open Libnames
@@ -14,6 +14,12 @@ open Miniml
 open Mlutil
 open Pp
 
+(** By default, in module Format, you can do horizontal placing of blocks
+    even if they include newlines, as long as the number of chars in the
+    blocks are less that a line length. To avoid this awkward situation,
+    we attach a big virtual size to [fnl] newlines. *)
+
+val fnl : unit -> std_ppcmds
 val fnl2 : unit -> std_ppcmds
 val space_if : bool -> std_ppcmds
 val sec_space_if : bool -> std_ppcmds
@@ -57,3 +63,14 @@ type reset_kind = AllButExternal | Everything
 val reset_renaming_tables : reset_kind -> unit
 
 val set_keywords : Idset.t -> unit
+
+(** For instance: [mk_ind "Coq.Init.Datatypes" "nat"] *)
+
+val mk_ind : string -> string -> mutual_inductive
+
+(** Special hack for constants of type Ascii.ascii : if an
+    [Extract Inductive ascii => char] has been declared, then
+    the constants are directly turned into chars *)
+
+val is_native_char : ml_ast -> bool
+val pp_native_char : ml_ast -> std_ppcmds
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index c5929392..7d4cd770 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: extract_env.ml 13420 2010-09-16 15:47:08Z letouzey $ i*)
+(*i $Id: extract_env.ml 14012 2011-04-15 16:45:27Z letouzey $ i*)
 
 open Term
 open Declarations
@@ -49,11 +49,12 @@ let environment_until dir_opt =
     | [] 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
+      let mb = Global.lookup_module (MPfile d) in
+      (* If -dont-load-proof has been used, mod_expr is None,
+         we try with mod_type *)
+      let meb = Option.default mb.mod_type mb.mod_expr in
+      if dir_opt = Some d then [MPfile d, meb]
+      else (MPfile d, meb) :: (parse l)
   in parse (Library.loaded_libraries ())
 
 
@@ -327,10 +328,17 @@ and extract_seb env mp all = function
   | 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 mp all (Option.get mb.mod_expr);
-    ml_mod_type = extract_seb_spec env mp (my_type_of_mb mb) }
+  (* A module has an empty [mod_expr] when :
+     - it is a module variable (for instance X inside a Module F [X:SIG])
+     - it is a module assumption (Declare Module).
+     Since we look at modules from outside, we shouldn't have variables.
+     But a Declare Module at toplevel seems legal (cf #2525). For the
+     moment we don't support this situation. *)
+  match mb.mod_expr with
+    | None -> error_no_module_expr mp
+    | Some me ->
+      { ml_mod_expr = extract_seb env mp all me;
+	ml_mod_type = extract_seb_spec env mp (my_type_of_mb mb) }
 
 
 let unpack = function MEstruct (_,sel) -> sel | _ -> assert false
@@ -397,13 +405,20 @@ let print_one_decl struc mp decl =
 (*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 ft =
+    if dry then Format.make_formatter (fun _ _ _ -> ()) (fun _ -> ())
+    else Pp_control.with_output_to (Option.default stdout file)
+  in
+  (* We never want to see ellipsis ... in extracted code *)
+  Format.pp_set_max_boxes ft max_int;
+  (* We reuse the width information given via "Set Printing Width" *)
+  (match Pp_control.get_margin () with
+    | None -> ()
+    | Some i ->
+      Format.pp_set_margin ft i;
+      Format.pp_set_max_indent ft (i-10));
+      (* note: max_indent should be < margin above, otherwise it's ignored *)
+  ft
 
 let print_structure_to_file (fn,si,mo) dry struc =
   let d = descr () in
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 5329c675..b9a3a736 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: extraction.ml 13733 2010-12-21 13:08:53Z letouzey $ i*)
+(*i $Id: extraction.ml 13795 2011-01-22 14:43:06Z glondu $ i*)
 
 (*i*)
 open Util
@@ -394,6 +394,9 @@ and extract_ind env kn = (* kn is supposed to be in long form *)
     (* Third pass: we determine special cases. *)
     let ind_info =
       try
+	let ip = (kn, 0) in
+	let r = IndRef ip in
+	if is_custom r then raise (I Standard);
 	if not mib.mind_finite then raise (I Coinductive);
 	if mib.mind_ntypes <> 1 then raise (I Standard);
 	let p = packets.(0) in
@@ -405,9 +408,6 @@ and extract_ind env kn = (* kn is supposed to be in long form *)
 	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
diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml
index 1c47ad81..17a38136 100644
--- a/plugins/extraction/haskell.ml
+++ b/plugins/extraction/haskell.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: haskell.ml 13733 2010-12-21 13:08:53Z letouzey $ i*)
+(*i $Id: haskell.ml 14010 2011-04-15 16:05:07Z letouzey $ i*)
 
 (*s Production of Haskell syntax. *)
 
@@ -106,7 +106,7 @@ let rec pp_type par vl t =
 
 let expr_needs_par = function
   | MLlam _  -> true
-  | MLcase _ -> true
+  | MLcase _ -> false (* now that we use the case ... of { ... } syntax *)
   | _        -> false
 
 
@@ -129,16 +129,17 @@ let rec pp_expr par env args =
 	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)))
+	let pp_def =
+	  str "let {" ++ cut () ++
+	  hov 1 (pp_id ++ str " = " ++ pp_a1 ++ str "}")
+	in
+	apply
+	  (pp_par par'
+	     (hv 0 (hv 0 (hv 1 pp_def ++ spc () ++ str "in") ++
+		    spc () ++ hov 0 pp_a2)))
     | MLglob r ->
 	apply (pp_global Term r)
+    | MLcons _ as c when is_native_char c -> assert (args=[]); pp_native_char c
     | MLcons (_,r,[]) ->
 	assert (args=[]); pp_global Cons r
     | MLcons (_,r,[a]) ->
@@ -153,13 +154,16 @@ let rec pp_expr par env args =
 	  if ids <> [] then named_lams (List.rev ids) e
 	  else dummy_lams (ast_lift 1 e) 1
 	in
-	hov 2 (str (find_custom_match pv) ++ fnl () ++
+	apply
+	  (pp_par par'
+	     (hov 2
+		(str (find_custom_match pv) ++ fnl () ++
 		 prvect (fun tr -> pp_expr true env [] (mkfun tr) ++ fnl ()) pv
-	       ++ pp_expr true env [] t)
+		 ++ pp_expr true env [] t)))
     | MLcase (info,t, pv) ->
       	apply (pp_par par'
-		 (v 0 (str "case " ++ pp_expr false env [] t ++ str " of" ++
-		       fnl () ++ str "  " ++ pp_pat env info pv)))
+		 (v 0 (str "case " ++ pp_expr false env [] t ++ str " of {" ++
+		       fnl () ++ pp_pat env info 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
@@ -176,12 +180,11 @@ and pp_pat env info pv =
   let pp_one_pat (name,ids,t) =
     let ids,env' = push_vars (List.rev_map id_of_mlid ids) env in
     let par = expr_needs_par t in
-    hov 2 (pp_global Cons name ++
+    hov 2 (str " " ++ pp_global Cons name ++
 	   (match ids with
 	      | [] -> mt ()
 	      | _  -> (str " " ++
-		       prlist_with_sep
-			 (fun () -> (spc ())) pr_id (List.rev ids))) ++
+		       prlist_with_sep spc pr_id (List.rev ids))) ++
 	   str " ->" ++ spc () ++ pp_expr par env' [] t)
   in
   let factor_br, factor_set = try match info.m_same with
@@ -198,18 +201,18 @@ and pp_pat env info pv =
   prvecti
     (fun i x -> if Intset.mem i factor_set then mt () else
        (pp_one_pat pv.(i) ++
-       if i = last && Intset.is_empty factor_set then mt () else
-       fnl () ++ str "  ")) pv
+       if i = last && Intset.is_empty factor_set then str "}" else
+	 (str ";" ++ fnl ()))) pv
   ++
   if Intset.is_empty factor_set then mt () else
   let par = expr_needs_par factor_br in
   match info.m_same with
     | BranchFun _ ->
         let ids, env' = push_vars [anonymous_name] env in
-        pr_id (List.hd ids) ++ str " ->" ++ spc () ++
-	  pp_expr par env' [] factor_br
+        hov 2 (str " " ++ pr_id (List.hd ids) ++ str " ->" ++ spc () ++
+	       pp_expr par env' [] factor_br ++ str "}")
     | BranchCst _ ->
-        str "_ ->" ++ spc () ++ pp_expr par env [] factor_br
+        hov 2 (str " _ ->" ++ spc () ++ pp_expr par env [] factor_br ++ str "}")
     | BranchNone -> mt ()
 
 (*s names of the functions ([ids]) are already pushed in [env],
@@ -218,12 +221,12 @@ and pp_pat env info pv =
 and pp_fix par env i (ids,bl) args =
   pp_par par
     (v 0
-       (v 2 (str "let" ++ fnl () ++
-	     prvect_with_sep fnl
+       (v 1 (str "let {" ++ fnl () ++
+	     prvect_with_sep (fun () -> str ";" ++ 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)))
+	       (array_map2 (fun a b -> a,b) ids bl) ++
+	     str "}") ++
+        fnl () ++ str "in " ++ pp_apply (pr_id ids.(i)) false args))
 
 and pp_function env f t =
   let bl,t' = collect_lams t in
@@ -262,12 +265,12 @@ let pp_one_ind ip pl cv =
 		  (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"
+  pp_global Type (IndRef ip) ++
+  prlist_strict (fun id -> str " " ++ pr_lower_id id) pl ++ str " =" ++
+  if Array.length cv = 0 then str " () -- empty inductive"
   else
-    (v 0 (str "= " ++
+    (fnl () ++ str " " ++
+     v 0 (str "  " ++
 	  prvect_with_sep (fun () -> fnl () ++ str "| ") pp_constructor
 	    (Array.mapi (fun i c -> ConstructRef (ip,i+1),c) cv)))
 
@@ -309,15 +312,23 @@ let pp_decl = function
 	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
+      let names = Array.map
+	(fun r -> if is_inline_custom r then mt () else pp_global Term r) rv
+      in
+      prvecti
+	(fun i r ->
+	  let void = is_inline_custom r ||
+	    (not (is_custom r) && defs.(i) = MLexn "UNUSED")
+	  in
+	  if void then mt ()
+	  else
+	    names.(i) ++ str " :: " ++ pp_type false [] typs.(i) ++ fnl () ++
+	    (if is_custom r then
+		(names.(i) ++ str " = " ++ str (find_custom r))
+	     else
+		(pp_function (empty_env ()) names.(i) defs.(i)))
+	    ++ fnl2 ())
+	rv
   | Dterm (r, a, t) ->
       if is_inline_custom r then mt ()
       else
diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml
index d467f508..c242e4ab 100644
--- a/plugins/extraction/mlutil.ml
+++ b/plugins/extraction/mlutil.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: mlutil.ml 13733 2010-12-21 13:08:53Z letouzey $ i*)
+(*i $Id: mlutil.ml 14003 2011-04-14 23:09:41Z letouzey $ i*)
 
 (*i*)
 open Pp
@@ -110,22 +110,17 @@ let rec type_occurs alpha t =
 
 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)
+  | Tmeta m, t | t, Tmeta m ->
+    (match m.contents with
+      | Some u -> mgu (u, t)
+      | None when type_occurs m.id t -> raise Impossible
+      | None -> m.contents <- Some t)
   | 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 -> ()
+  | t, u when t = u -> () (* for Tvar, Tvar', Tunknown, Taxiom *)
   | _ -> raise Impossible
 
 let needs_magic p = try mgu p; false with Impossible -> true
@@ -828,6 +823,23 @@ let is_atomic = function
 
 let is_imm_apply = function MLapp (MLrel 1, _) -> true | _ -> false
 
+(** Program creates a let-in named "program_branch_NN" for each branch of match.
+    Unfolding them leads to more natural code (and more dummy removal) *)
+
+let is_program_branch = function
+  | Id id ->
+    let s = string_of_id id in
+    let br = "program_branch_" in
+    let n = String.length br in
+    (try
+       ignore (int_of_string (String.sub s n (String.length s - n)));
+       String.sub s 0 n = br
+     with _ -> false)
+  | Tmp _ | Dummy -> false
+
+let expand_linear_let o id e =
+   o.opt_lin_let || is_tmp id || is_program_branch id || is_imm_apply e
+
 (*S The main simplification function. *)
 
 (* Some beta-iota reductions + simplifications. *)
@@ -844,7 +856,7 @@ let rec simpl o = function
       if
 	(is_atomic c) || (is_atomic e) ||
 	(let n = nb_occur_match e in
-	 (n = 0 || (n=1 && (is_tmp id || is_imm_apply e || o.opt_lin_let))))
+	 (n = 0 || (n=1 && expand_linear_let o id e)))
       then
 	simpl o (ast_subst c e)
       else
diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml
index 313fc58d..23ec108a 100644
--- a/plugins/extraction/modutil.ml
+++ b/plugins/extraction/modutil.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: modutil.ml 13733 2010-12-21 13:08:53Z letouzey $ i*)
+(*i $Id: modutil.ml 14006 2011-04-14 23:09:56Z letouzey $ i*)
 
 open Names
 open Declarations
@@ -289,10 +289,10 @@ let reset_needed, add_needed, found_needed, is_needed =
    (fun r -> Refset'.mem (base_r r) !needed))
 
 let declared_refs = function
-  | Dind (kn,_) -> [|IndRef (mind_of_kn kn,0)|]
-  | Dtype (r,_,_) -> [|r|]
-  | Dterm (r,_,_) -> [|r|]
-  | Dfix (rv,_,_) -> rv
+  | Dind (kn,_) -> [IndRef (mind_of_kn kn,0)]
+  | Dtype (r,_,_) -> [r]
+  | Dterm (r,_,_) -> [r]
+  | Dfix (rv,_,_) -> Array.to_list rv
 
 (* Computes the dependencies of a declaration, except in case
    of custom extraction. *)
@@ -308,18 +308,25 @@ let compute_deps_decl = function
       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')
+  | ((l,SEdecl d) as t) :: se ->
+    let se' = depcheck_se se in
+    let refs = declared_refs d in
+    let refs' = List.filter is_needed refs in
+    if refs' = [] then
+      (List.iter remove_info_axiom refs; se')
+    else begin
+      List.iter found_needed refs';
+      (* Hack to avoid extracting unused part of a Dfix *)
+      match d with
+	| Dfix (rv,trms,tys) when (List.for_all is_custom refs') ->
+	  let trms' =  Array.create (Array.length rv) (MLexn "UNUSED") in
+	  ((l,SEdecl (Dfix (rv,trms',tys))) :: se')
+	| _ -> (compute_deps_decl d; t::se')
+    end
   | _ -> raise NoDepCheck
 
 let rec depcheck_struct = function
diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml
index f136fab5..81eea9e2 100644
--- a/plugins/extraction/ocaml.ml
+++ b/plugins/extraction/ocaml.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: ocaml.ml 13733 2010-12-21 13:08:53Z letouzey $ i*)
+(*i $Id: ocaml.ml 14010 2011-04-15 16:05:07Z letouzey $ i*)
 
 (*s Production of Ocaml syntax. *)
 
@@ -120,9 +120,6 @@ 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 mk_ind path s =
-  make_mind (MPfile (dirpath_of_string path)) empty_dirpath (mk_label s)
-
 let rec pp_type par vl t =
   let rec pp_rec par = function
     | Tmeta _ | Tvar' _ | Taxiom -> assert false
@@ -160,26 +157,6 @@ let expr_needs_par = function
   | MLcase (_,_,pv) -> not (is_ifthenelse pv)
   | _        -> false
 
-
-(** Special hack for constants of type Ascii.ascii : if an
-    [Extract Inductive ascii => char] has been declared, then
-    the constants are directly turned into chars *)
-
-let ind_ascii = mk_ind "Coq.Strings.Ascii" "ascii"
-
-let check_extract_ascii () =
-  try find_custom (IndRef (ind_ascii,0)) = "char" with Not_found -> false
-
-let is_list_cons l =
- List.for_all (function MLcons (_,ConstructRef(_,_),[]) -> true | _ -> false) l
-
-let pp_char l =
-  let rec cumul = function
-    | [] -> 0
-    | MLcons(_,ConstructRef(_,j),[])::l -> (2-j) + 2 * (cumul l)
-    | _ -> assert false
-  in str ("'"^Char.escaped (Char.chr (cumul l))^"'")
-
 let rec pp_expr par env args =
   let par' = args <> [] || par
   and apply st = pp_apply st par args in
@@ -214,10 +191,7 @@ let rec pp_expr par env args =
 	   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(_,ConstructRef ((kn,0),1),l)
-        when kn = ind_ascii && check_extract_ascii () & is_list_cons l ->
-	assert (args=[]);
-	pp_char l
+    | MLcons _ as c when is_native_char c -> assert (args=[]); pp_native_char c
     | MLcons ({c_kind = Coinductive},r,[]) ->
 	assert (args=[]);
 	pp_par par (str "lazy " ++ pp_global Cons r)
@@ -247,9 +221,12 @@ let rec pp_expr par env args =
 	  if ids <> [] then named_lams (List.rev ids) e
 	  else dummy_lams (ast_lift 1 e) 1
 	in
-	hov 2 (str (find_custom_match pv) ++ fnl () ++
+	apply
+	  (pp_par par'
+	     (hov 2
+		(str (find_custom_match pv) ++ fnl () ++
 		 prvect (fun tr -> pp_expr true env [] (mkfun tr) ++ fnl ()) pv
-	       ++ pp_expr true env [] t)
+		 ++ pp_expr true env [] t)))
     | MLcase (info, t, pv) ->
 	let expr = if info.m_kind = Coinductive then
 	  (str "Lazy.force" ++ spc () ++ pp_expr true env [] t)
@@ -291,7 +268,7 @@ let rec pp_expr par env args =
 		  (try pp_ifthenelse par' env expr pv
 		   with Not_found ->
 		     v 0 (str "match " ++ expr ++ str " with" ++ fnl () ++
-			  str "  | " ++ pp_pat env info pv))))
+			  pp_pat env info 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
@@ -355,19 +332,19 @@ and pp_pat env info pv =
   prvecti
     (fun i x -> if Intset.mem i factor_set then mt () else
        let s1,s2 = pp_one_pat env info x in
-       hov 2 (s1 ++ str " ->" ++ spc () ++ s2) ++
-       if i = last && Intset.is_empty factor_set then mt () else
-       fnl () ++ str "  | ") pv
+       hv 2 (hov 4 (str "| " ++ s1 ++ str " ->") ++ spc () ++ hov 2 s2) ++
+       if i = last && Intset.is_empty factor_set then mt () else fnl ())
+    pv
   ++
   if Intset.is_empty factor_set then mt () else
   let par = expr_needs_par factor_br in
   match info.m_same with
     | BranchFun _ ->
         let ids, env' = push_vars [anonymous_name] env in
-        hov 2 (pr_id (List.hd ids) ++ str " ->" ++ spc () ++
-		 pp_expr par env' [] factor_br)
+        hv 2 (str "| " ++ pr_id (List.hd ids) ++ str " ->" ++ spc () ++
+		 hov 2 (pp_expr par env' [] factor_br))
     | BranchCst _ ->
-        hov 2 (str "_ ->" ++ spc () ++ pp_expr par env [] factor_br)
+        hv 2 (str "| _ ->" ++ spc () ++ hov 2 (pp_expr par env [] factor_br))
     | BranchNone -> mt ()
 
 and pp_function env t =
@@ -379,11 +356,11 @@ and pp_function env t =
 	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)
+	  v 0 (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)
+	  v 0 (pp_pat env' i pv)
     | _ ->
           pr_binding (List.rev bl) ++
 	  str " =" ++ fnl () ++ str "  " ++
@@ -412,17 +389,24 @@ 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)
+  let rec pp init i =
+    if i >= Array.length rv then
+      (if init then failwith "empty phrase" else mt ())
     else
-      let def =
-	if is_custom rv.(i) then str " = " ++ str (find_custom rv.(i))
-	else pp_function (empty_env ()) c.(i)
+      let void = is_inline_custom rv.(i) ||
+	(not (is_custom rv.(i)) && c.(i) = MLexn "UNUSED")
       in
-      sep () ++ pp_val names.(i) t.(i) ++
-      str letand ++ names.(i) ++ def ++ pp fnl2 "and " (i+1)
-  in pp mt "let rec " 0
+      if void then pp init (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
+	(if init then mt () else fnl2 ()) ++
+	pp_val names.(i) t.(i) ++
+	str (if init then "let rec " else "and ") ++ names.(i) ++ def ++
+	pp false (i+1)
+  in pp true 0
 
 (*s Pretty-printing of inductive types declaration. *)
 
@@ -439,7 +423,7 @@ 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) ++
+    hov 3 (str "| " ++ cnames.(i) ++
 	   (if typs = [] then mt () else str " of ") ++
 	   prlist_with_sep
 	    (fun () -> spc () ++ str "* ") (pp_type true pl) typs)
diff --git a/plugins/extraction/scheme.ml b/plugins/extraction/scheme.ml
index 06098591..cb980cba 100644
--- a/plugins/extraction/scheme.ml
+++ b/plugins/extraction/scheme.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: scheme.ml 13733 2010-12-21 13:08:53Z letouzey $ i*)
+(*i $Id: scheme.ml 14006 2011-04-14 23:09:56Z letouzey $ i*)
 
 (*s Production of Scheme syntax. *)
 
@@ -101,9 +101,12 @@ let rec pp_expr env args =
 	  if ids <> [] then named_lams (List.rev ids) e
 	  else dummy_lams (ast_lift 1 e) 1
 	in
-	hov 2 (str (find_custom_match pv) ++ fnl () ++
+	apply
+	  (paren
+	     (hov 2
+		(str (find_custom_match pv) ++ fnl () ++
 		 prvect (fun tr -> pp_expr env [] (mkfun tr) ++ fnl ()) pv
-	       ++ pp_expr env [] t)
+		 ++ pp_expr env [] t)))
      | MLcase (info,t, pv) ->
 	let e =
 	  if info.m_kind <> Coinductive then pp_expr env [] t
@@ -163,24 +166,29 @@ 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 ()
+      let names = Array.map
+	(fun r -> if is_inline_custom r then mt () else pp_global Term r) rv
+      in
+      prvecti
+	(fun i r ->
+	  let void = is_inline_custom r ||
+	    (not (is_custom r) && defs.(i) = MLexn "UNUSED")
+	  in
+	  if void then mt ()
+	  else
+	    hov 2
+	      (paren (str "define " ++ names.(i) ++ spc () ++
+			(if is_custom r then str (find_custom r)
+			 else pp_expr (empty_env ()) [] defs.(i)))
+	       ++ fnl ()) ++ fnl ())
+	rv
   | 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 ()
+	hov 2 (paren (str "define " ++ pp_global Term r ++ spc () ++
+			(if is_custom r then str (find_custom r)
+			 else pp_expr (empty_env ()) [] a)))
+	++ fnl2 ()
 
 let rec pp_structure_elem = function
   | (l,SEdecl d) -> pp_decl d
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index 085c0a44..b2b5e6f5 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: table.ml 13733 2010-12-21 13:08:53Z letouzey $ i*)
+(*i $Id: table.ml 14012 2011-04-15 16:45:27Z letouzey $ i*)
 
 open Names
 open Term
@@ -310,6 +310,12 @@ let error_module_clash mp1 mp2 =
        pr_long_mp mp2 ++ str " have the same ML name.\n" ++
        str "This is not supported yet. Please do some renaming first.")
 
+let error_no_module_expr mp =
+  err (str "The module " ++ pr_long_mp mp
+       ++ str " has no body, it probably comes from\n"
+       ++ str "some Declare Module outside any Module Type.\n"
+       ++ str "This situation is currently unsupported by the extraction.")
+
 let error_unknown_module m =
   err (str "Module" ++ spc () ++ pr_qualid m ++ spc () ++ str "not found.")
 
diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli
index ff4780a1..2eafe1d8 100644
--- a/plugins/extraction/table.mli
+++ b/plugins/extraction/table.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: table.mli 13420 2010-09-16 15:47:08Z letouzey $ i*)
+(*i $Id: table.mli 14012 2011-04-15 16:45:27Z letouzey $ i*)
 
 open Names
 open Libnames
@@ -29,6 +29,7 @@ val error_constant : global_reference -> 'a
 val error_inductive : global_reference -> 'a
 val error_nb_cons : unit -> 'a
 val error_module_clash : module_path -> module_path -> 'a
+val error_no_module_expr : module_path -> 'a
 val error_unknown_module : qualid -> 'a
 val error_scheme : unit -> 'a
 val error_not_visible : global_reference -> 'a
diff --git a/plugins/subtac/subtac_cases.ml b/plugins/subtac/subtac_cases.ml
index f6f8695b..866e6a10 100644
--- a/plugins/subtac/subtac_cases.ml
+++ b/plugins/subtac/subtac_cases.ml
@@ -7,7 +7,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: subtac_cases.ml 13332 2010-07-26 22:12:43Z msozeau $ *)
+(* $Id: subtac_cases.ml 14003 2011-04-14 23:09:41Z letouzey $ *)
 
 open Cases
 open Util
@@ -1741,7 +1741,7 @@ let constrs_of_pats typing_fun env isevars eqns tomatchs sign neqs arity =
 	 let j = typing_fun (mk_tycon tycon) rhs_env eqn.rhs.it in
 	 let bbody = it_mkLambda_or_LetIn j.uj_val rhs_rels'
 	 and btype = it_mkProd_or_LetIn j.uj_type rhs_rels' in
-	 let branch_name = id_of_string ("branch_" ^ (string_of_int !i)) in
+	 let branch_name = id_of_string ("program_branch_" ^ (string_of_int !i)) in
 	 let branch_decl = (Name branch_name, Some (lift !i bbody), (lift !i btype)) in
 	 let branch =
 	   let bref = RVar (dummy_loc, branch_name) in