Imported Upstream version 8.3.pl2upstream/8.3.pl2

64 files changed, 722 insertions, 361 deletions

diff --git a/.gitignore b/.gitignore
index 75324995..031b06b5 100644
--- a/.gitignore
+++ b/.gitignore
@@ -73,6 +73,8 @@ toplevel/mltop.byteml
 coqdoc.sty
 ide/index_urls.txt
 doc/faq/html/
+doc/refman/csdp.cache
+doc/refman/trace
 doc/refman/Reference-Manual.pdf
 doc/refman/Reference-Manual.ps
 doc/refman/cover.html
diff --git a/CHANGES b/CHANGES
index f4caf602..ce0763af 100644
--- a/CHANGES
+++ b/CHANGES
@@ -1,3 +1,43 @@
+Changes from V8.3pl1 to V8.3pl2
+===============================
+
+Coqdoc and documentation bugs
+
+- #2470 (use "membership" instead of "appartness")
+- #2475 (documentation of the "f binders := t" notation for record fields)
+- Documentation of module String on coq.inria.fr/stdlib
+
+Tactics
+
+- #2493 (dependent pairs injection failing because of Type cumulativity missing)
+- Reduction "simpl" sometimes failing in presence of names redefined in modules
+
+Extraction
+
+- #2359 (Some unnecessary unsafe casts are now avoided (bug in the type checker)).
+- #2469 (fix Extract Inlined Constant for Haskell and Scheme)
+- #2476 (Fix indentation of default pattern in haskell case)
+- #2477 (Avoid printing unused mutual fix components)
+- #2478 (Add missing parenthesis around emulated pattern-match)
+- #2482 (Extract Inductive on singleton inductives)
+- #2484 (Avoid an assert failure with -dont-load-proofs)
+- #2497 (malformed Haskell extraction of deeply-nested match expressions)
+- #2515 (Allow extracting Ascii.ascii to native Char in Haskell)
+- #2525 (Nicer error when a toplevel module has no body)
+- Fix printing of haskell modular names
+
+Miscellaneous bug fixes
+
+- #2487 (compilation with camlp5 in strict mode)
+- #2283, #2460 (new option "Set Default Timeout n / Unset Default Timeout")
+- #2524 (In win32, the exit code of coqc should be correct now)
+- Now, vm_compute is responsive to Ctrl-C interruption, as the rest of coqtop
+- Fixed uncaught exception when vmcast used in Check
+- coqdep complies with the -R visibility discipline
+- Fixing printing of f when defined using "Notation f x := ..."
+- Fixing Unset for options setting integer values
+- Excluding admitted subgoals from Search/SearchAbout
+
 Changes from V8.3 to V8.3pl1
 ============================
 
@@ -49,6 +89,10 @@ Miscellaneous bug fixes
 - a few improvements in efficiency
 
 
+Extraction
+
+- The pretty-printer for Haskell now produces layout-independant code
+
 Changes from V8.2 to V8.3
 =========================
 
diff --git a/Coq.bat b/Coq.bat
deleted file mode 100755
index cdd7d50d..00000000
--- a/Coq.bat
+++ /dev/null
@@ -1,8 +0,0 @@
-@echo off
-set COQBIN=%~0\..\bin
-set COQLIB=%~0\..\lib
-echo Using COQBIN= %COQBIN%
-echo and   COQLIB= %COQLIB%
-echo Starting Coq
-%~0\..\bin\coqtop.opt.exe
-pause
\ No newline at end of file
diff --git a/Coqide.bat b/Coqide.bat
deleted file mode 100755
index f955a970..00000000
--- a/Coqide.bat
+++ /dev/null
@@ -1,7 +0,0 @@
-@echo off
-set COQBIN=%~0\..\bin
-set COQLIB=%~0\..\lib
-echo Using COQBIN= %COQBIN%
-echo and   COQLIB= %COQLIB%
-echo Starting Coqide
-%~0\..\bin\coqide.opt.exe
\ No newline at end of file
diff --git a/INSTALL b/INSTALL
index fa3ae5ab..b1cc3af1 100644
--- a/INSTALL
+++ b/INSTALL
@@ -41,7 +41,7 @@ WHAT DO YOU NEED ?
 
    Should you need or prefer to compile Coq V8.3 yourself, you need:
 
-     - Objective Caml version 3.09.3 or later
+     - Objective Caml version 3.10.2 or later
        (available at http://caml.inria.fr/)
 
        For Objective Caml version >= 3.10.0, you also need to install
@@ -88,7 +88,7 @@ QUICK INSTALLATION PROCEDURE.
 INSTALLATION PROCEDURE IN DETAILS (NORMAL USERS).
 =================================================
 
-1- Check that you have the Objective Caml compiler version 3.09.3 (or later)
+1- Check that you have the Objective Caml compiler version 3.10.2 (or later)
    installed on your computer and that "ocamlmktop" and "ocamlc" (or
    its native code version "ocamlc.opt") lie in a directory which is present
    in your $PATH environment variable. 
diff --git a/INSTALL.ide b/INSTALL.ide
index 2c2f86f5..e99002f0 100644
--- a/INSTALL.ide
+++ b/INSTALL.ide
@@ -23,7 +23,7 @@ On Gentoo GNU/Linux, do:
 Else, read the rest of this document to compile your own CoqIde.
 
 REQUIREMENT:
-	- OCaml >= 3.09.3 with native threads support.
+	- OCaml >= 3.10.2 with native threads support.
 	- make world must succeed.
 	- The graphical toolkit GTK+ 2.x. See http://www.gtk.org.
 	  The official supported version is at least 2.10.x.
diff --git a/README.win b/README.win
index a8714f4e..dcbf37b5 100644
--- a/README.win
+++ b/README.win
@@ -9,9 +9,9 @@ INSTALLATION.
     The Coq package for Windows comes with an auto-installer. It will
 install Coq binaries and libraries under any directory you specify
 (C:\Program Files\Coq is the default path). It also creates shortcuts
-in the Windows menus. Alternatively, you can launch Coq using Coq.bat
-and Coqide.bat in the installation directory (C:\Program Files\Coq by
-default).
+in the Windows menus. Alternatively, you can launch Coq using coqide.exe
+or coqtop.exe in the bin sub-directory of the installation
+(C:\Program Files\Coq\bin by default).
 
 COMPILATION.
 ============
@@ -20,7 +20,7 @@ COMPILATION.
     distribution. If you really need to recompile under Windows, here
     are some indications:
 
-    1- Install ocaml for Windows (MinGW port), at least version 3.09.3.
+    1- Install ocaml for Windows (MinGW port), at least version 3.10.2.
        See: http://caml.inria.fr
 
     2- Install a shell environment with at least:
@@ -52,4 +52,8 @@ COMPILATION.
 
     Good luck :-)
 
+    Alternatively, it is now possible (and even recommended ...) to build
+    Windows executables of coq from Linux thanks to a mingw cross-compiler.
+    If interested, please contact us for more details.
+
     The Coq Team.
diff --git a/_tags b/_tags
index 69df3480..96776266 100644
--- a/_tags
+++ b/_tags
@@ -10,6 +10,7 @@
 <tools/coqdoc/main.{native,byte}> : use_str
 <checker/main.{native,byte}> : use_str, use_unix, use_gramlib
 <plugins/micromega/csdpcert.{native,byte}> : use_nums, use_unix
+<tools/mkwinapp.{native,byte}> : use_unix
 
 ## tags for ide
 
diff --git a/configure b/configure
index 9113f1e0..7cff4b97 100755
--- a/configure
+++ b/configure
@@ -6,7 +6,7 @@
 # 
 ##################################
 
-VERSION=8.3pl1
+VERSION=8.3pl2
 VOMAGIC=08300
 STATEMAGIC=58300
 DATE=`LANG=C date +"%B %Y"`
@@ -411,12 +411,12 @@ esac
 CAMLVERSION=`"$bytecamlc" -version`
 
 case $CAMLVERSION in
-    1.*|2.*|3.00|3.01|3.02|3.03|3.03alpha|3.04|3.05beta|3.05|3.06|3.07*|3.08*|3.09.[012])
+    1.*|2.*|3.00|3.01|3.02|3.03|3.03alpha|3.04|3.05beta|3.05|3.06|3.07*|3.08*|3.09*)
 	echo "Your version of Objective-Caml is $CAMLVERSION."
 	if [ "$force_caml_version" = "yes" ]; then
 	    echo "*Warning* You are compiling Coq with an outdated version of Objective-Caml."
 	else
-	    echo "          You need Objective-Caml 3.09.3 or later."
+	    echo "          You need Objective-Caml 3.10.2 or later."
 	    echo "          Configuration script failed!"
 	    exit 1
 	fi;;
@@ -491,11 +491,6 @@ if [ "$camlp5dir" != "" ]; then
 	exit 1
     fi
     camlp4oexec=`echo $camlp4oexec | sed -e 's/4/5/'`
-    if [ `$camlp4oexec -pmode 2>&1` = "strict" ]; then 
-	echo "Error: Camlp5 found, but in strict mode!"
-	echo "Please compile Camlp5 in transitional mode."
-	exit 1
-    fi
 else
     case $CAMLTAG in
         OCAML31*)
@@ -510,11 +505,6 @@ else
             fi
             CAMLP4=camlp5
             camlp4oexec=`echo $camlp4oexec | sed -e 's/4/5/'`
-            if [ `$camlp4oexec -pmode 2>&1` = "strict" ]; then
-	        echo "Error: Camlp5 found, but in strict mode!"
-	        echo "Please compile Camlp5 in transitional mode."
-	        exit 1
-            fi
             ;;
         *)
             CAMLP4=camlp4
@@ -1094,4 +1084,4 @@ echo
 echo "*Warning* To compile the system for a new architecture"
 echo "          don't forget to do a 'make archclean' before './configure'."
 
-# $Id: configure 13740 2010-12-23 12:37:18Z notin $
+# $Id: configure 14025 2011-04-19 07:19:00Z notin $
diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex
index b8a893d5..c0e578fe 100644
--- a/doc/refman/RefMan-ext.tex
+++ b/doc/refman/RefMan-ext.tex
@@ -24,8 +24,8 @@ construction allows to define ``signatures''.
 && ~~~~\zeroone{\ident}
        \verb!{! \zeroone{\nelist{\field}{;}} \verb!}! \verb:.:\\
   & & \\
-{\field} & ::= & {\name} : {\type} [ {\tt where} {\it notation} ] \\
- & $|$ & {\name} {\typecstr} := {\term}
+{\field} & ::= & {\name} \zeroone{\binders} : {\type} [ {\tt where} {\it notation} ] \\
+ & $|$ & {\name} \zeroone{\binders} {\typecstr} := {\term}
 \end{tabular}
 \end{centerframe}
 \caption{Syntax for the definition of {\tt Record}}
@@ -37,9 +37,9 @@ construction allows to define ``signatures''.
 \smallskip
 {\tt Record} {\ident} {\params} \texttt{:} 
    {\sort} := {\ident$_0$} \verb+{+
- {\ident$_1$} \texttt{:} {\term$_1$}; 
+ {\ident$_1$} \binders$_1$ \texttt{:} {\term$_1$}; 
               \dots
-  {\ident$_n$} \texttt{:} {\term$_n$} \verb+}+.
+  {\ident$_n$} \binders$_n$ \texttt{:} {\term$_n$} \verb+}+.
 \smallskip
  
 \noindent the identifier {\ident} is the name of the defined record
@@ -47,7 +47,7 @@ and {\sort} is its type. The identifier {\ident$_0$} is the name of
 its constructor. If {\ident$_0$} is omitted, the default name {\tt
 Build\_{\ident}} is used. If {\sort} is omitted, the default sort is ``{\Type}''.
 The identifiers {\ident$_1$}, ..,
-{\ident$_n$} are the names of fields and {\term$_1$}, .., {\term$_n$}
+{\ident$_n$} are the names of fields and {\tt forall} \binders$_1${\tt ,} {\term$_1$}, ..., {\tt forall} \binders$_n${\tt ,} {\term$_n$}
 their respective types. Remark that the type of {\ident$_i$} may
 depend on the previous {\ident$_j$} (for $j<i$). Thus the order of the
 fields is important. Finally, {\params} are the parameters of the
diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex
index 920e86de..025788f5 100644
--- a/doc/refman/RefMan-oth.tex
+++ b/doc/refman/RefMan-oth.tex
@@ -929,6 +929,21 @@ the command has not terminated after the time specified by the integer
 (time expressed in seconds), then it is interrupted and an error message
 is displayed.
 
+\subsection[\tt Set Default Timeout \textrm{\textsl{int}}.]{\tt Set
+  Default Timeout \textrm{\textsl{int}}.\comindex{Set Default Timeout}}
+
+After using this command, all subsequent commands behave as if they
+were passed to a {\tt Timeout} command. Commands already starting by
+a {\tt Timeout} are unaffected.
+
+\subsection[\tt Unset Default Timeout.]{\tt Unset Default Timeout.\comindex{Unset Default Timeout}}
+
+This command turns off the use of a defaut timeout.
+
+\subsection[\tt Test Default Timeout.]{\tt Test Default Timeout.\comindex{Test Default Timeout}}
+
+This command displays whether some default timeout has be set or not.
+
 \section{Controlling display}
 
 \subsection[\tt Set Silent.]{\tt Set Silent.\comindex{Set Silent}
@@ -1173,7 +1188,7 @@ control the scope of their effect. There are four kinds of commands:
 \end{itemize}
 
 
-% $Id: RefMan-oth.tex 13454 2010-09-23 17:00:29Z aspiwack $ 
+% $Id: RefMan-oth.tex 13923 2011-03-21 16:25:20Z letouzey $ 
 
 %%% Local Variables: 
 %%% mode: latex
diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index 7ee85fe8..541fa1b9 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -452,13 +452,13 @@ through the <tt>Require Import</tt> command.</p>
     theories/FSets/FMapFullAVL.v
   </dd>
 
-<!--  <dt> <b>Strings</b>
+  <dt> <b>Strings</b>
     Implementation of string as list of ascii characters
   </dt>
   <dd>
     theories/Strings/Ascii.v
     theories/Strings/String.v
-  </dd> -->
+  </dd>
     
   <dt> <b>Reals</b>:
     Formalization of real numbers
diff --git a/ide/coq.ml b/ide/coq.ml
index 4996661a..bb08e2af 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: coq.ml 13431 2010-09-18 08:15:29Z herbelin $ *)
+(* $Id: coq.ml 13751 2010-12-24 09:56:05Z letouzey $ *)
 
 open Vernac
 open Vernacexpr
@@ -27,10 +27,6 @@ open Termops
 open Namegen
 open Ideutils
 
-let prerr_endline s = if !debug then prerr_endline s else ()
-
-let output = ref (Format.formatter_of_out_channel stdout)
-
 let msg m =
   let b =  Buffer.create 103 in
   Pp.msg_with (Format.formatter_of_buffer b) m;
@@ -394,7 +390,7 @@ let compute_reset_info loc_ast =
   }
 
 let reset_initial () =
-  prerr_endline "Reset initial called"; flush stderr;
+  prerr_endline "Reset initial called";
   Vernacentries.abort_refine Lib.reset_initial ()
 
 let reset_to sp =
@@ -412,7 +408,7 @@ let interp_with_options verbosely options s =
   let pe = Pcoq.Gram.Entry.parse Pcoq.main_entry pa in
   (* Temporary hack to make coqide.byte work (WTF???) - now with less screen
   * pollution *)
-  Pervasives.prerr_string " \r"; Pervasives.flush stderr;
+  (try Pervasives.prerr_string " \r"; Pervasives.flush stderr with _ -> ());
   match pe with
     | None -> assert false
     | Some((loc,vernac) as last) ->
diff --git a/ide/coq_icon.rc b/ide/coq_icon.rc
new file mode 100644
index 00000000..f873e7de
--- /dev/null
+++ b/ide/coq_icon.rc
@@ -0,0 +1 @@
+large   ICON    ide/coq.ico
diff --git a/ide/coqide.ml b/ide/coqide.ml
index fdf33c39..ce4f0666 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: coqide.ml 13708 2010-12-13 14:49:29Z gmelquio $ *)
+(* $Id: coqide.ml 13751 2010-12-24 09:56:05Z letouzey $ *)
 
 open Preferences
 open Vernacexpr
@@ -200,7 +200,7 @@ let signals_to_crash = [Sys.sigabrt; Sys.sigalrm; Sys.sigfpe; Sys.sighup;
 
 let crash_save i =
   (*  ignore (Unix.sigprocmask Unix.SIG_BLOCK signals_to_crash);*)
-  Pervasives.prerr_endline "Trying to save all buffers in .crashcoqide files";
+  safe_prerr_endline "Trying to save all buffers in .crashcoqide files";
   let count = ref 0 in
     List.iter
       (function {script=view; analyzed_view = av } ->
@@ -212,12 +212,12 @@ let crash_save i =
 	  in
 	    try
 	      if try_export filename (view#buffer#get_text ()) then
-		Pervasives.prerr_endline ("Saved "^filename)
-	      else Pervasives.prerr_endline ("Could not save "^filename)
-	    with _ -> Pervasives.prerr_endline ("Could not save "^filename))
+		safe_prerr_endline ("Saved "^filename)
+	      else safe_prerr_endline ("Could not save "^filename)
+	    with _ -> safe_prerr_endline ("Could not save "^filename))
       )
       session_notebook#pages;
-    Pervasives.prerr_endline "Done. Please report.";
+    safe_prerr_endline "Done. Please report.";
     if i <> 127 then exit i
 
 let ignore_break () =
@@ -3202,7 +3202,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
 							      "\nCoq is developed by the Coq Development Team\
        \n(INRIA - CNRS - University Paris 11 and partners)\
        \nWeb site: " ^ Coq_config.wwwcoq ^
-       "\nFeature wish or bug report: http://logical.saclay.inria.fr/coq-bugs\
+       "\nFeature wish or bug report: http://coq.inria.fr/bugs\
        \n\
        \nCredits for CoqIDE, the Integrated Development Environment for Coq:\
        \n\
@@ -3332,10 +3332,10 @@ let start () =
       try
 	GtkThread.main ()
       with
-	| Sys.Break -> prerr_endline "Interrupted." ; flush stderr
+	| Sys.Break -> prerr_endline "Interrupted."
 	| e ->
-	    Pervasives.prerr_endline ("CoqIde unexpected error:" ^ (Printexc.to_string e));
-	    flush stderr;
+	    safe_prerr_endline ("CoqIde unexpected error:" ^ (Printexc.to_string e));
+	    flush_all ();
 	    crash_save 127
     done
 
diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index 138bf5f6..8b7840e3 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: ideutils.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: ideutils.ml 13751 2010-12-24 09:56:05Z letouzey $ *)
 
 
 open Preferences
@@ -31,12 +31,16 @@ let set_location = ref  (function s -> failwith "not ready")
 
 let pbar = GRange.progress_bar ~pulse_step:0.2 ()
 
+(* On a Win32 application with no console, writing to stderr raise
+   a Sys_error "bad file descriptor" *)
+let safe_prerr_endline msg = try prerr_endline msg with _ -> ()
+
 let debug = Flags.debug
 
 let prerr_endline s =
-  if !debug then (prerr_endline s;flush stderr)
+  if !debug then try (prerr_endline s;flush stderr) with _ -> ()
 let prerr_string s =
-  if !debug then (prerr_string s;flush stderr)
+  if !debug then try (prerr_string s;flush stderr) with _ -> ()
 
 let lib_ide_file f =
   let coqlib = Envars.coqlib () in
diff --git a/ide/ideutils.mli b/ide/ideutils.mli
index 9af4fb43..ade460c6 100644
--- a/ide/ideutils.mli
+++ b/ide/ideutils.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: ideutils.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: ideutils.mli 13751 2010-12-24 09:56:05Z letouzey $ i*)
 
 val async : ('a -> unit) -> 'a -> unit
 val sync  : ('a -> 'b) -> 'a -> 'b
@@ -34,6 +34,7 @@ val is_char_start : char -> bool
 val lib_ide_file : string -> string
 val my_stat : string -> Unix.stats option
 
+val safe_prerr_endline : string -> unit
 val prerr_endline : string -> unit
 val prerr_string : string -> unit
 val print_id : 'a -> unit
diff --git a/ide/utils/configwin_messages.ml b/ide/utils/configwin_messages.ml
index f8984462..26f5b61b 100644
--- a/ide/utils/configwin_messages.ml
+++ b/ide/utils/configwin_messages.ml
@@ -30,9 +30,7 @@ let version = "1.2";;
 
 let html_config = "Configwin bindings configurator for html parameters"
 
-let home =
-  try Sys.getenv "HOME"
-  with Not_found -> ""
+let home = System.home
 
 let mCapture = "Capture";;
 let mType_key = "Type key" ;;
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index fd230539..1716cfad 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: constrextern.ml 13492 2010-10-04 21:20:01Z herbelin $ *)
+(* $Id: constrextern.ml 13967 2011-04-08 14:08:43Z herbelin $ *)
 
 (*i*)
 open Pp
@@ -343,6 +343,10 @@ let make_pat_notation loc ntn (terms,termlists as subst) =
     (fun (loc,p) -> CPatPrim (loc,p))
     destPatPrim terms
 
+let mkPat loc qid l =
+  (* Normally irrelevant test with v8 syntax, but let's do it anyway *)
+  if l = [] then CPatAtom (loc,Some qid) else CPatCstr (loc,qid,l)
+
  (* Better to use extern_rawconstr composed with injection/retraction ?? *)
 let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat =
   try
@@ -397,15 +401,9 @@ and extern_symbol_pattern (tmp_scope,scopes as allscopes) vars t = function
 	(match keyrule with
         | NotationRule (sc,ntn) -> raise No_match
         | SynDefRule kn ->
-	    let p =
-	      let qid = Qualid (loc, shortest_qualid_of_syndef vars kn) in
-	      if l = [] then
-		CPatAtom (loc,Some qid)
-	      else
-		let l =
-		  List.map (extern_cases_pattern_in_scope allscopes vars) l in
-		CPatCstr (loc,qid,l) in
-	    insert_pat_alias loc p na)
+	    let qid = Qualid (loc, shortest_qualid_of_syndef vars kn) in
+	    let l = List.map (extern_cases_pattern_in_scope allscopes vars) l in
+	    insert_pat_alias loc (mkPat loc qid l) na)
       | PatCstr (_,f,l,_), Some n when List.length l > n ->
 	  raise No_match
       | PatCstr (loc,_,_,na),_ ->
@@ -432,8 +430,13 @@ and extern_symbol_pattern (tmp_scope,scopes as allscopes) vars t = function
 		  insert_pat_delimiters loc
 		    (make_pat_notation loc ntn (l,ll)) key)
           | SynDefRule kn ->
-	      let qid = shortest_qualid_of_syndef vars kn in
-              CPatAtom (loc,Some (Qualid (loc, qid))) in
+	      let qid = Qualid (loc, shortest_qualid_of_syndef vars kn) in
+	      let l =
+		List.map (fun (c,(scopt,scl)) ->
+                  extern_cases_pattern_in_scope (scopt,scl@scopes) vars c) 
+                  subst in
+              assert (substlist = []);
+	      mkPat loc qid l in
 	insert_pat_alias loc p na
       | PatVar (loc,Anonymous),_ -> CPatAtom (loc, None)
       | PatVar (loc,Name id),_ -> CPatAtom (loc, Some (Ident (loc,id)))
diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index 98ef2791..cce2319b 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -14,6 +14,7 @@
    for fast computation of bounded (31bits) integers */
 
 #include <stdio.h>
+#include <signal.h>
 #include "coq_gc.h"
 #include "coq_instruct.h"
 #include "coq_fix_code.h"
@@ -157,6 +158,12 @@ sp is a local copy of the global variable extern_sp. */
 #endif
 #endif
 
+/* For signal handling, we highjack some code from the caml runtime */
+
+extern intnat caml_signals_are_pending;
+extern intnat caml_pending_signals[];
+extern void caml_process_pending_signals(void);
+
 /* The interpreter itself */
 
 value coq_interprete
@@ -414,8 +421,13 @@ value coq_interprete
 	realloc_coq_stack(Coq_stack_threshold);
 	sp = coq_sp;
       }
+      /* We also check for signals */
+      if (caml_signals_are_pending) {
+	/* If there's a Ctrl-C, we reset the vm */
+	if (caml_pending_signals[SIGINT]) { coq_sp = coq_stack_high; }
+	caml_process_pending_signals();
+      }
       Next;
-      /* Fall through CHECK_SIGNALS */
 
       Instruct(APPTERM) {
 	int nargs = *pc++;
diff --git a/kernel/names.ml b/kernel/names.ml
index 9f1becf7..e5a9f0fc 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: names.ml 13486 2010-10-03 17:01:43Z herbelin $ *)
+(* $Id: names.ml 13804 2011-01-27 00:41:34Z letouzey $ *)
 
 open Pp
 open Util
@@ -223,7 +223,7 @@ type constructor = inductive * int
 
 let constant_of_kn kn = (kn,kn)
 let constant_of_kn_equiv kn1 kn2 = (kn1,kn2)
-let make_con mp dir l = ((mp,dir,l),(mp,dir,l))
+let make_con mp dir l = constant_of_kn (mp,dir,l)
 let make_con_equiv mp1 mp2 dir l = ((mp1,dir,l),(mp2,dir,l))
 let canonical_con con = snd con
 let user_con con = fst con
@@ -235,6 +235,10 @@ let debug_pr_con con = str "("++ pr_kn (fst con) ++ str ","++ pr_kn (snd con)++
 let eq_constant (_,kn1) (_,kn2) = kn1=kn2
 let debug_string_of_con con =  string_of_kn (fst con)^"'"^string_of_kn (snd con)
 
+let con_with_label ((mp1,dp1,l1),(mp2,dp2,l2) as con) lbl =
+  if lbl = l1 && lbl = l2 then con
+  else ((mp1,dp1,lbl),(mp2,dp2,lbl))
+
 let con_modpath con = modpath (fst con)
 
 let mind_modpath mind = modpath (fst mind)
diff --git a/kernel/names.mli b/kernel/names.mli
index f54df6ec..f57116f9 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: names.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: names.mli 13804 2011-01-27 00:41:34Z letouzey $ i*)
 
 (*s Identifiers *)
 
@@ -139,6 +139,7 @@ val user_con : constant -> kernel_name
 val canonical_con : constant -> kernel_name
 val repr_con : constant -> module_path * dir_path * label
 val eq_constant : constant -> constant -> bool
+val con_with_label : constant -> label -> constant
 
 val string_of_con : constant -> string
 val con_label : constant -> label
diff --git a/lib/envars.ml b/lib/envars.ml
index efb2d3fa..b0db1a50 100644
--- a/lib/envars.ml
+++ b/lib/envars.ml
@@ -14,6 +14,13 @@ let coqbin () =
   then Filename.concat Coq_config.coqsrc "bin"
   else System.canonical_path_name (Filename.dirname Sys.executable_name)
 
+(* On win32, we add coqbin to the PATH at launch-time (this used to be
+   done in a .bat script). *)
+
+let _ =
+  if Coq_config.arch = "win32" then
+    Unix.putenv "PATH" (coqbin() ^ ";" ^ System.getenv_else "PATH" "")
+
 let guess_coqlib () =
   let file = "states/initial.coq" in
     if Sys.file_exists (Filename.concat Coq_config.coqlib file)
diff --git a/lib/system.ml b/lib/system.ml
index 17d211f8..7744a79b 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: system.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: system.ml 13750 2010-12-24 09:55:54Z letouzey $ *)
 
 open Pp
 open Util
@@ -19,12 +19,21 @@ let safe_getenv_def var def =
     Sys.getenv var
   with Not_found ->
     warning ("Environment variable "^var^" not found: using '"^def^"' .");
-    flush Pervasives.stdout;
+    flush_all ();
     def
 
 let getenv_else s dft = try Sys.getenv s with Not_found -> dft
 
-let home = (safe_getenv_def "HOME" ".")
+(* On win32, the home directory is probably not in $HOME, but in
+   some other environment variable *)
+
+let home =
+  try Sys.getenv "HOME" with Not_found ->
+    try (Sys.getenv "HOMEDRIVE")^(Sys.getenv "HOMEPATH") with Not_found ->
+      try Sys.getenv "USERPROFILE" with Not_found ->
+	warning ("Cannot determine user home directory, using '.' .");
+	flush_all ();
+	"."
 
 let safe_getenv n = safe_getenv_def n ("$"^n)
 
diff --git a/library/goptions.ml b/library/goptions.ml
index bfd3b272..8cf560d5 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: goptions.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: goptions.ml 13922 2011-03-21 16:25:18Z letouzey $ *)
 
 (* This module manages customization parameters at the vernacular level     *)
 
@@ -305,19 +305,37 @@ let set_option_value locality check_and_cast key v =
 
 let bad_type_error () = error "Bad type of value for this option."
 
-let set_int_option_value_gen locality = set_option_value  locality
-  (fun v -> function
-     | (IntValue _) -> IntValue v
-     | _ -> bad_type_error ())
+let check_int_value v = function
+  | IntValue _ -> IntValue v
+  | _ -> bad_type_error ()
+
+let check_bool_value v = function
+  | BoolValue _ -> BoolValue v
+  | _ -> bad_type_error ()
+
+let check_string_value v = function
+  | StringValue _ -> StringValue v
+  | _ -> bad_type_error ()
+
+let check_unset_value v = function
+  | BoolValue _ -> BoolValue false
+  | IntValue _ -> IntValue None
+  | _ -> bad_type_error ()
+
+(* Nota: For compatibility reasons, some errors are treated as
+   warning. This allows a script to refer to an option that doesn't
+   exist anymore *)
+
+let set_int_option_value_gen locality =
+  set_option_value locality check_int_value
 let set_bool_option_value_gen locality key v =
-  try set_option_value locality (fun v -> function
-     | (BoolValue _) -> BoolValue v
-     | _ -> bad_type_error ()) key v
+  try set_option_value locality check_bool_value key v
+  with UserError (_,s) -> Flags.if_verbose msg_warning s
+let set_string_option_value_gen locality =
+  set_option_value locality check_string_value
+let unset_option_value_gen locality key =
+  try set_option_value locality check_unset_value key ()
   with UserError (_,s) -> Flags.if_verbose msg_warning s
-let set_string_option_value_gen locality = set_option_value locality
- (fun v -> function
-    | (StringValue _) -> StringValue v
-    | _ -> bad_type_error ())
 
 let set_int_option_value = set_int_option_value_gen None
 let set_bool_option_value = set_bool_option_value_gen None
diff --git a/library/goptions.mli b/library/goptions.mli
index d2f98cd2..2962b5ca 100644
--- a/library/goptions.mli
+++ b/library/goptions.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: goptions.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: goptions.mli 13922 2011-03-21 16:25:18Z letouzey $ i*)
 
 (* This module manages customization parameters at the vernacular level     *)
 
@@ -157,6 +157,7 @@ val get_ref_table :
 val set_int_option_value_gen    : bool option -> option_name -> int option -> unit
 val set_bool_option_value_gen   : bool option -> option_name -> bool   -> unit
 val set_string_option_value_gen : bool option -> option_name -> string -> unit
+val unset_option_value_gen : bool option -> option_name -> unit
 
 val set_int_option_value    : option_name -> int option -> unit
 val set_bool_option_value   : option_name -> bool   -> unit
diff --git a/myocamlbuild.ml b/myocamlbuild.ml
index f062b50b..1994efac 100644
--- a/myocamlbuild.ml
+++ b/myocamlbuild.ml
@@ -64,8 +64,10 @@ let w32pref = "i586-mingw32msvc"
 let w32ocamlc = w32pref^"-ocamlc"
 let w32ocamlopt = w32pref^"-ocamlopt"
 let w32ocamlmklib = w32pref^"-ocamlmklib"
+let w32res = w32pref^"-windres"
 let w32lib = "/usr/"^w32pref^"/lib/"
 let w32bin = "/usr/"^w32pref^"/bin/"
+let w32ico = "ide/coq_icon.o"
 
 let _ = if w32 then begin
   Options.ocamlopt := A w32ocamlopt;
@@ -167,6 +169,7 @@ let coqmktop = "scripts/coqmktop"
 type links = Both | Best | BestInPlace | Ide
 
 let all_binaries =
+ (if w32 then [ "mkwinapp", "tools/mkwinapp", Best ] else []) @
  [ "coqtop", coqtop, Both;
    "coqide", coqide, Ide;
    "coqmktop", coqmktop, Both;
@@ -365,18 +368,35 @@ let extra_rules () = begin
 	      "let ide = \""^ide_mods^"\"\n"],
 	     tolink));
 
+(** For windows, building coff object file from a .rc (for the icon) *)
+
+  if w32 then rule ".rc.o" ~deps:["%.rc";"ide/coq.ico"] ~prod:"%.o"
+    (fun env _ ->
+       let rc = env "%.rc" and o = env "%.o" in
+       Cmd (S [P w32res;A "--input-format";A "rc";A "--input";P rc;
+	       A "--output-format";A "coff";A "--output"; Px o]));
+
 (** Coqtop and coqide *)
 
   let mktop_rule f is_ide =
     let fo = f^".native" and fb = f^".byte" in
     let ideflag = if is_ide then A"-ide" else N in
     let depsall = [coqmktopbest;libcoqrun] in
+    let depsall = if w32 then w32ico::depsall else depsall in
     let depso = "coq_config.cmx" :: core_cmxa in
     let depsb = "coq_config.cmo" :: core_cma in
     let depideo = if is_ide then [ide_cmxa] else [] in
     let depideb = if is_ide then [ide_cma] else [] in
-    let w32ideflag = (*if is_ide then [A"-ccopt";A"\"-link -mwindows\""] else*) [] in
-    let w32flag = if not w32 then N else S ([A"-camlbin";A w32bin]@w32ideflag) in
+    let w32ideflag =
+      (* Uncomment the following line to make coqide a console-free win32 app.
+         For the moment we don't, some issue remain to be investigated.
+         In the meantime, coqide can be made console-free a posteriori via
+         the mkwinapp tool. *)
+      (*if is_ide then [A"-ccopt";A"\"-link -Wl,-subsystem,windows\""] else*) [] in
+    let w32flag =
+      if not w32 then N
+      else S ([A"-camlbin";A w32bin;A "-ccopt";P w32ico]@w32ideflag)
+    in
     if opt then rule fo ~prod:fo ~deps:(depsall@depso@depideo) ~insert:`top
       (cmd [P coqmktopbest;w32flag;A"-boot";A"-opt";ideflag;incl fo;A"-o";Px fo]);
     rule fb ~prod:fb ~deps:(depsall@depsb@depideb) ~insert:`top
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml
index cf83c72a..3fc18219 100644
--- a/parsing/prettyp.ml
+++ b/parsing/prettyp.ml
@@ -10,7 +10,7 @@
  * on May-June 2006 for implementation of abstraction of pretty-printing of objects.
  *)
 
-(* $Id: prettyp.ml 13492 2010-10-04 21:20:01Z herbelin $ *)
+(* $Id: prettyp.ml 13967 2011-04-08 14:08:43Z herbelin $ *)
 
 open Pp
 open Util
@@ -460,13 +460,15 @@ let gallina_print_constant_with_infos sp =
   with_line_skip (print_name_infos (ConstRef sp))
 
 let gallina_print_syntactic_def kn =
-  let sep = " := "
-  and qid = Nametab.shortest_qualid_of_syndef Idset.empty kn
+  let qid = Nametab.shortest_qualid_of_syndef Idset.empty kn
   and (vars,a) = Syntax_def.search_syntactic_definition kn in
   let c = Topconstr.rawconstr_of_aconstr dummy_loc a in
-  str "Notation " ++ pr_qualid qid ++
-  prlist_with_sep spc pr_id (List.map fst vars) ++ str sep ++
-  Constrextern.without_symbols pr_lrawconstr c ++ fnl ()
+  hov 2
+    (hov 4
+       (str "Notation " ++ pr_qualid qid ++
+        prlist (fun id -> spc () ++ pr_id id) (List.map fst vars) ++ 
+        spc () ++ str ":=") ++
+     spc () ++ Constrextern.without_symbols pr_rawconstr c) ++ fnl ()
 
 let gallina_print_leaf_entry with_values ((sp,kn as oname),lobj) =
   let sep = if with_values then " = " else " : "
diff --git a/parsing/tacextend.ml4 b/parsing/tacextend.ml4
index f067fcf3..39477b0b 100644
--- a/parsing/tacextend.ml4
+++ b/parsing/tacextend.ml4
@@ -8,7 +8,7 @@
 
 (*i camlp4use: "pa_extend.cmo q_MLast.cmo" i*)
 
-(* $Id: tacextend.ml4 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: tacextend.ml4 13799 2011-01-25 17:38:40Z glondu $ *)
 
 open Util
 open Genarg
@@ -55,7 +55,7 @@ let rec make_let e = function
 let add_clause s (pt,e) l =
   let p = make_patt pt in
   let w = Some (make_when (MLast.loc_of_expr e) pt) in
-  (p, w, make_let e pt)::l
+  (p, <:vala< w >>, make_let e pt)::l
 
 let rec extract_signature = function
   | [] -> []
@@ -72,7 +72,8 @@ let check_unicity s l =
 let make_clauses s l =
   check_unicity s l;
   let default =
-    (<:patt< _ >>,None,<:expr< failwith "Tactic extension: cannot occur" >>) in
+    (<:patt< _ >>,<:vala<None>>,
+     <:expr< failwith "Tactic extension: cannot occur" >>) in
   List.fold_right (add_clause s) l [default]
 
 let rec make_args = function
diff --git a/parsing/vernacextend.ml4 b/parsing/vernacextend.ml4
index 95eccfda..860110e5 100644
--- a/parsing/vernacextend.ml4
+++ b/parsing/vernacextend.ml4
@@ -8,7 +8,7 @@
 
 (*i camlp4use: "pa_extend.cmo q_MLast.cmo" i*)
 
-(* $Id: vernacextend.ml4 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: vernacextend.ml4 13799 2011-01-25 17:38:40Z glondu $ *)
 
 open Util
 open Genarg
@@ -31,7 +31,7 @@ let rec make_let e = function
 let add_clause s (_,pt,e) l =
   let p = make_patt pt in
   let w = Some (make_when (MLast.loc_of_expr e) pt) in
-  (p, w, make_let e pt)::l
+  (p, <:vala<w>>, make_let e pt)::l
 
 let check_unicity s l =
   let l' = List.map (fun (_,l,_) -> extract_signature l) l in
@@ -43,7 +43,8 @@ let check_unicity s l =
 let make_clauses s l =
   check_unicity s l;
   let default =
-    (<:patt< _ >>,None,<:expr< failwith "Vernac extension: cannot occur" >>) in
+    (<:patt< _ >>,<:vala<None>>,
+     <:expr< failwith "Vernac extension: cannot occur" >>) in
   List.fold_right (add_clause s) l [default]
 
 let mlexpr_of_clause =
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
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index bae89329..67bf7043 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: cases.ml 13728 2010-12-19 11:35:20Z herbelin $ *)
+(* $Id: cases.ml 13962 2011-04-06 17:00:45Z herbelin $ *)
 
 open Util
 open Names
@@ -1203,7 +1203,7 @@ and match_current pb tomatch =
 	  let case = mkCase (ci,nf_betaiota Evd.empty pred,current,brvals) in
 	  let inst = List.map mkRel deps in
 	  { uj_val = applist (case, inst);
-	    uj_type = substl inst typ }
+	    uj_type = prod_applist typ inst }
 
 and compile_branch current names deps pb arsign eqn cstr =
   let sign, pb = build_branch current deps names pb arsign eqn cstr in
diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml
index a41cdd6f..b9fd307c 100644
--- a/pretyping/clenv.ml
+++ b/pretyping/clenv.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: clenv.ml 13332 2010-07-26 22:12:43Z msozeau $ *)
+(* $Id: clenv.ml 13902 2011-03-10 15:50:24Z msozeau $ *)
 
 open Pp
 open Util
@@ -305,7 +305,7 @@ let evar_clenv_unique_resolver = clenv_unique_resolver
 
 let connect_clenv gls clenv =
   { clenv with
-    evd = evars_reset_evd gls.sigma clenv.evd;
+    evd = evars_reset_evd ~with_conv_pbs:true gls.sigma clenv.evd;
     env = Global.env_of_context gls.it.evar_hyps }
 
 (* [clenv_fchain mv clenv clenv']
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 77442584..5d61e727 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: evd.ml 13332 2010-07-26 22:12:43Z msozeau $ *)
+(* $Id: evd.ml 13902 2011-03-10 15:50:24Z msozeau $ *)
 
 open Pp
 open Util
@@ -507,7 +507,9 @@ let empty =  {
   metas=Metamap.empty
 }
 
-let evars_reset_evd evd d = {d with evars = evd.evars}
+let evars_reset_evd ?(with_conv_pbs=false) evd d =
+  {d with evars = evd.evars; 
+     conv_pbs = if with_conv_pbs then evd.conv_pbs else d.conv_pbs}
 let add_conv_pb pb d = {d with conv_pbs = pb::d.conv_pbs}
 let evar_source evk d = (EvarMap.find d.evars evk).evar_source
 
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index ce4e1b28..c68cfffe 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: evd.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: evd.mli 13902 2011-03-10 15:50:24Z msozeau $ i*)
 
 (*i*)
 open Util
@@ -177,7 +177,7 @@ val existential_opt_value : evar_map -> existential -> constr option
 val subst_evar_defs_light : substitution -> evar_map -> evar_map
 
 (* spiwack: this function seems to somewhat break the abstraction. *)
-val evars_reset_evd  : evar_map ->  evar_map -> evar_map
+val evars_reset_evd  : ?with_conv_pbs:bool -> evar_map ->  evar_map -> evar_map
 
 
 (* spiwack: [is_undefined_evar] should be considered a candidate
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 1c17ff88..b8dc719b 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: pretyping.ml 13408 2010-09-11 19:19:04Z herbelin $ *)
+(* $Id: pretyping.ml 13780 2011-01-07 16:37:57Z herbelin $ *)
 
 open Pp
 open Util
@@ -634,7 +634,10 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 		let cty = nf_evar !evdref cj.uj_type and tval = nf_evar !evdref tj.utj_val in
 		let cj = match k with
 		  | VMcast when not (occur_existential cty || occur_existential tval) ->
-		      ignore (Reduction.vm_conv Reduction.CUMUL env cty tval); cj
+		     (try ignore (Reduction.vm_conv Reduction.CUMUL env cty tval); cj
+                      with Reduction.NotConvertible ->
+                        error_actual_type_loc loc env !evdref cj tval)
+
 		  | _ -> inh_conv_coerce_to_tycon loc env evdref cj (mk_tycon tval)
 		in
 		let v = mkCast (cj.uj_val, k, tval) in
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 49ccb80c..68a67402 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: tacred.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: tacred.ml 13804 2011-01-27 00:41:34Z letouzey $ *)
 
 open Pp
 open Util
@@ -216,8 +216,7 @@ let invert_name labs l na0 env sigma ref = function
 	  | EvalRel _ | EvalEvar _ -> None
 	  | EvalVar id' -> Some (EvalVar id)
 	  | EvalConst kn ->
-	      let (mp,dp,_) = repr_con kn in
-	      Some (EvalConst (make_con mp dp (label_of_id id))) in
+	      Some (EvalConst (con_with_label kn (label_of_id id))) in
 	match refi with
 	  | None -> None
 	  | Some ref ->
@@ -481,7 +480,6 @@ let reduce_mind_case_use_function func env sigma mia =
     | CoFix (bodynum,(names,_,_) as cofix) ->
 	let build_cofix_name =
 	  if isConst func then
-	    let (mp,dp,_) = repr_con (destConst func) in
             let minargs = List.length mia.mcargs in
 	    fun i ->
 	      if i = bodynum then Some (minargs,func)
@@ -492,7 +490,8 @@ let reduce_mind_case_use_function func env sigma mia =
 		       mutual inductive, try to reuse the global name if
 		       the block was indeed initially built as a global
 		       definition *)
-		    let kn = make_con mp dp (label_of_id id) in
+		    let kn = con_with_label (destConst func) (label_of_id id)
+		    in
 		    try match constant_opt_value env kn with
 		      | None -> None
                           (* TODO: check kn is correct *)
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 171db848..42111213 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: pfedit.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: pfedit.ml 13981 2011-04-08 16:59:26Z herbelin $ *)
 
 open Pp
 open Util
@@ -344,8 +344,7 @@ open Decl_kinds
 
 let next = let n = ref 0 in fun () -> incr n; !n
 
-let build_constant_by_tactic sign typ tac =
-  let id = id_of_string ("temporary_proof"^string_of_int (next())) in
+let build_constant_by_tactic id sign typ tac =
   start_proof id (Global,Proof Theorem) sign typ (fun _ _ -> ());
   try
     by tac;
@@ -357,5 +356,6 @@ let build_constant_by_tactic sign typ tac =
     raise e
 
 let build_by_tactic typ tac =
+  let id = id_of_string ("temporary_proof"^string_of_int (next())) in
   let sign = Decls.clear_proofs (Global.named_context ()) in
-  (build_constant_by_tactic sign typ tac).const_entry_body
+  (build_constant_by_tactic id sign typ tac).const_entry_body
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 1b284f8d..8df26706 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: pfedit.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: pfedit.mli 13981 2011-04-08 16:59:26Z herbelin $ i*)
 
 (*i*)
 open Util
@@ -202,6 +202,6 @@ val mutate : (pftreestate -> pftreestate) -> unit
 
 (* [build_by_tactic typ tac] returns a term of type [typ] by calling [tac] *)
 
-val build_constant_by_tactic : named_context_val -> types -> tactic ->
+val build_constant_by_tactic : identifier -> named_context_val -> types -> tactic ->
   Entries.definition_entry
 val build_by_tactic : types -> tactic -> constr
diff --git a/scripts/coqc.ml b/scripts/coqc.ml
index 7185b140..cc8e5a1a 100644
--- a/scripts/coqc.ml
+++ b/scripts/coqc.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: coqc.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: coqc.ml 14015 2011-04-15 17:48:45Z letouzey $ *)
 
 (* Afin de rendre Coq plus portable, ce programme Caml remplace le script
    coqc.
@@ -84,7 +84,11 @@ let compile command args files =
         Unix.create_process_env command (Array.of_list args') environment
         Unix.stdin Unix.stdout Unix.stderr
      in
-     ignore (Unix.waitpid [] pid)
+     let status = snd (Unix.waitpid [] pid) in
+     let errcode =
+       match status with Unix.WEXITED c|Unix.WSTOPPED c|Unix.WSIGNALED c -> c
+     in
+     exit errcode
   | _ ->
      Unix.execvpe command (Array.of_list args') environment
 
@@ -196,4 +200,4 @@ let main () =
       (*  List.iter (compile coqtopname args) cfiles*)
       Unix.handle_unix_error (compile coqtopname args) cfiles
 
-let _ = Printexc.print main (); exit 0
+let _ = Printexc.print main ()
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index afd13b4c..66f15fbe 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -8,7 +8,7 @@
 
 (*i camlp4deps: "parsing/grammar.cma" i*)
 
-(* $Id: class_tactics.ml4 13332 2010-07-26 22:12:43Z msozeau $ *)
+(* $Id: class_tactics.ml4 13902 2011-03-10 15:50:24Z msozeau $ *)
 
 open Pp
 open Util
@@ -85,7 +85,7 @@ let evars_to_goals p evm =
     if goals = [] then None
     else
       let goals = List.rev goals in
-      let evm' = evars_reset_evd evm' evm in
+      let evm' = evars_reset_evd ~with_conv_pbs:false evm' evm in
 	Some (goals, evm')
 
 (** Typeclasses instance search tactic / eauto *)
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 7a774cc9..411ccc0e 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: equality.ml 13586 2010-10-27 17:42:13Z jforest $ *)
+(* $Id: equality.ml 13874 2011-03-05 16:41:53Z herbelin $ *)
 
 open Pp
 open Util
@@ -888,8 +888,8 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt =
       with
 	| Some w ->
             let w_type = type_of env sigma w in
-            if Evarconv.e_conv env evdref w_type a then
-              applist(exist_term,[a;p_i_minus_1;w;tuple_tail])
+            if Evarconv.e_cumul env evdref w_type a then
+              applist(exist_term,[w_type;p_i_minus_1;w;tuple_tail])
             else
               error "Cannot solve a unification problem."
 	| None -> anomaly "Not enough components to build the dependent tuple"
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 569cf356..771047fd 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: tactics.ml 13693 2010-12-08 15:32:25Z msozeau $ *)
+(* $Id: tactics.ml 13981 2011-04-08 16:59:26Z herbelin $ *)
 
 open Pp
 open Util
@@ -3469,7 +3469,7 @@ let abstract_subproof id tac gl =
     try flush_and_check_evars (project gl) concl
     with Uninstantiated_evar _ ->
       error "\"abstract\" cannot handle existentials." in
-  let const = Pfedit.build_constant_by_tactic secsign concl
+  let const = Pfedit.build_constant_by_tactic id secsign concl
     (tclCOMPLETE (tclTHEN (tclDO (List.length sign) intro) tac)) in
   let cd = Entries.DefinitionEntry const in
   let lem = mkConst (Declare.declare_internal_constant id (cd,IsProof Lemma)) in
diff --git a/test-suite/output/Extraction_matchs_2413.out b/test-suite/output/Extraction_matchs_2413.out
index 7bce6671..848abd00 100644
--- a/test-suite/output/Extraction_matchs_2413.out
+++ b/test-suite/output/Extraction_matchs_2413.out
@@ -9,8 +9,8 @@ let test2 b =
 (** val wrong_id : 'a1 hole -> 'a2 hole **)
 
 let wrong_id = function
-  | Hole -> Hole
-  | Hole2 -> Hole2
+| Hole -> Hole
+| Hole2 -> Hole2
 (** val test3 : 'a1 option -> 'a1 option **)
 
 let test3 o =
@@ -18,35 +18,35 @@ let test3 o =
 (** val test4 : indu -> indu **)
 
 let test4 = function
-  | A m -> A (S m)
-  | x -> x
+| A m -> A (S m)
+| x -> x
 (** val test5 : indu -> indu **)
 
 let test5 = function
-  | A m -> A (S m)
-  | _ -> B
+| A m -> A (S m)
+| _ -> B
 (** val test6 : indu' -> indu' **)
 
 let test6 = function
-  | A' m -> A' (S m)
-  | E' -> B'
-  | F' -> B'
-  | _ -> C'
+| A' m -> A' (S m)
+| E' -> B'
+| F' -> B'
+| _ -> C'
 (** val test7 : indu -> nat option **)
 
 let test7 = function
-  | A m -> Some m
-  | _ -> None
+| A m -> Some m
+| _ -> None
 (** val decode_cond_mode :
     (word -> opcode option) -> (word -> 'a1 decoder_result) -> word -> ('a1
     -> opcode -> 'a2) -> 'a2 decoder_result **)
 
 let decode_cond_mode condition f w g =
   match condition w with
-    | Some oc ->
-        (match f w with
-           | DecUndefined -> DecUndefined
-           | DecUnpredictable -> DecUnpredictable
-           | DecInst i -> DecInst (g i oc)
-           | DecError m -> DecError m)
-    | None -> DecUndefined
+  | Some oc ->
+    (match f w with
+     | DecUndefined -> DecUndefined
+     | DecUnpredictable -> DecUnpredictable
+     | DecInst i -> DecInst (g i oc)
+     | DecError m -> DecError m)
+  | None -> DecUndefined
diff --git a/theories/FSets/FMapAVL.v b/theories/FSets/FMapAVL.v
index cf0449f8..49f595d7 100644
--- a/theories/FSets/FMapAVL.v
+++ b/theories/FSets/FMapAVL.v
@@ -8,7 +8,7 @@
 
 (* Finite map library.  *)
 
-(* $Id: FMapAVL.v 13427 2010-09-17 17:37:52Z letouzey $ *)
+(* $Id: FMapAVL.v 13768 2011-01-06 13:55:35Z glondu $ *)
 
 (** * FMapAVL *)
 
@@ -78,9 +78,9 @@ Definition empty := Leaf.
 
 Definition is_empty m := match m with Leaf => true | _ => false end.
 
-(** * Appartness *)
+(** * Membership *)
 
-(** The [mem] function is deciding appartness. It exploits the [bst] property
+(** The [mem] function is deciding membership. It exploits the [bst] property
     to achieve logarithmic complexity. *)
 
 Fixpoint mem x m : bool :=
@@ -705,7 +705,7 @@ Proof.
  destruct m; simpl; intros; try discriminate; red; intuition_in.
 Qed.
 
-(** * Appartness *)
+(** * Membership *)
 
 Lemma mem_1 : forall m x, bst m -> In x m -> mem x m = true.
 Proof.
diff --git a/theories/MSets/MSetAVL.v b/theories/MSets/MSetAVL.v
index c41df7c2..96580749 100644
--- a/theories/MSets/MSetAVL.v
+++ b/theories/MSets/MSetAVL.v
@@ -82,9 +82,9 @@ Definition empty := Leaf.
 Definition is_empty s :=
   match s with Leaf => true | _ => false end.
 
-(** ** Appartness *)
+(** ** Membership *)
 
-(** The [mem] function is deciding appartness. It exploits the
+(** The [mem] function is deciding membership. It exploits the
     binary search tree invariant to achieve logarithmic complexity. *)
 
 Fixpoint mem x s :=
@@ -792,7 +792,7 @@ Proof.
  split; auto. try discriminate. intro H; elim (H x); auto.
 Qed.
 
-(** * Appartness *)
+(** * Membership *)
 
 Lemma mem_spec : forall s x `{Ok s}, mem x s = true <-> InT x s.
 Proof.
diff --git a/tools/coqdep.ml b/tools/coqdep.ml
index 9bc8965d..3093fa6c 100644
--- a/tools/coqdep.ml
+++ b/tools/coqdep.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: coqdep.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: coqdep.ml 13983 2011-04-08 17:57:56Z herbelin $ *)
 
 open Printf
 open Coqdep_lexer
@@ -41,8 +41,8 @@ let add_coqlib_known phys_dir log_dir f =
   match get_extension f [".vo"] with
     | (basename,".vo") ->
 	let name = log_dir@[basename] in
-	Hashtbl.add coqlibKnown [basename] ();
-	Hashtbl.add coqlibKnown name ()
+	let paths = suffixes name in
+        List.iter (fun f -> Hashtbl.add coqlibKnown f ()) paths
     | _ -> ()
 
 let sort () =
@@ -199,7 +199,8 @@ let coqdep () =
     let coqlib = Envars.coqlib () in
     add_rec_dir add_coqlib_known (coqlib//"theories") ["Coq"];
     add_rec_dir add_coqlib_known (coqlib//"plugins") ["Coq"];
-    add_dir add_coqlib_known (coqlib//"user-contrib") []
+    let user = coqlib//"user-contrib" in
+    if Sys.file_exists user then add_rec_dir add_coqlib_known user []
   end;
   List.iter (fun (f,d) -> add_mli_known f d) !mliAccu;
   List.iter (fun (f,d) -> add_mllib_known f d) !mllibAccu;
diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml
index 0961e398..851b7089 100644
--- a/tools/coqdep_common.ml
+++ b/tools/coqdep_common.ml
@@ -397,8 +397,7 @@ let rec add_directory recur add_file phys_dir log_dir =
 	  | S_DIR when recur ->
 	      if List.mem phys_f !norecdir_list then ()
 	      else
-		let log_dir' = if log_dir = [] then ["Coq"] else log_dir@[f] in
-		add_directory recur add_file phys_f log_dir'
+		add_directory recur add_file phys_f (log_dir@[f])
 	  | S_REG -> add_file phys_dir log_dir f
 	  | _ -> ()
     done
diff --git a/tools/mkwinapp.ml b/tools/mkwinapp.ml
new file mode 100644
index 00000000..226302fb
--- /dev/null
+++ b/tools/mkwinapp.ml
@@ -0,0 +1,92 @@
+(* OCaml-Win32
+ * mkwinapp.ml
+ * Copyright (c) 2002-2004 by Harry Chomsky
+ *
+ * This library is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU Library General Public
+ * License as published by the Free Software Foundation; either
+ * version 2 of the License, or (at your option) any later version.
+ *
+ * This library is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
+ * Library General Public License for more details.
+ *
+ * You should have received a copy of the GNU Library General Public
+ * License along with this library; if not, write to the Free
+ * Software Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.
+ *)
+
+(*********************************************************************
+ * This program alters an .exe file to make it use the "windows subsystem"
+ * instead of the "console subsystem".  In other words, when Windows runs
+ * the program, it will not create a console for it.
+ *)
+
+(* Pierre Letouzey 23/12/2010 : modification to allow selecting the
+   subsystem to use instead of just setting the windows subsystem *)
+
+(* This tool can be run directly via :
+   ocaml unix.cma mkwinapp.ml [-set|-unset] <filename>
+*)
+
+exception Invalid_file_format
+
+let input_word ic =
+    let lo = input_byte ic in
+    let hi = input_byte ic in
+    (hi lsl 8) + lo
+
+let find_pe_header ic =
+    seek_in ic 0x3C;
+    let peheader = input_word ic in
+    seek_in ic peheader;
+    if input_char ic <> 'P' then
+        raise Invalid_file_format;
+    if input_char ic <> 'E' then
+        raise Invalid_file_format;
+    peheader
+
+let find_optional_header ic =
+    let peheader = find_pe_header ic in
+    let coffheader = peheader + 4 in
+    seek_in ic (coffheader + 16);
+    let optsize = input_word ic in
+    if optsize < 96 then
+        raise Invalid_file_format;
+    let optheader = coffheader + 20 in
+    seek_in ic optheader;
+    let magic = input_word ic in
+    if magic <> 0x010B && magic <> 0x020B then
+        raise Invalid_file_format;
+    optheader
+
+let change flag ic oc =
+    let optheader = find_optional_header ic in
+    seek_out oc (optheader + 64);
+    for i = 1 to 4 do
+        output_byte oc 0
+    done;
+    output_byte oc (if flag then 2 else 3)
+
+let usage () =
+  print_endline "Alters a Win32 executable file to use the Windows subsystem or not.";
+  print_endline "Usage: mkwinapp [-set|-unset] <filename>";
+  print_endline "Giving no option is equivalent to -set";
+  exit 1
+
+let main () =
+  let n = Array.length Sys.argv - 1 in
+  if not (n = 1 || n = 2) then usage ();
+  let flag =
+    if n = 1 then true
+    else if Sys.argv.(1) = "-set" then true
+    else if Sys.argv.(1) = "-unset" then false
+    else usage ()
+  in
+  let filename = Sys.argv.(n) in
+  let f = Unix.openfile filename [Unix.O_RDWR] 0 in
+  let ic = Unix.in_channel_of_descr f and oc = Unix.out_channel_of_descr f in
+  change flag ic oc
+
+let _ = main ()
diff --git a/toplevel/search.ml b/toplevel/search.ml
index 0bd552af..574983cd 100644
--- a/toplevel/search.ml
+++ b/toplevel/search.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: search.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: search.ml 13853 2011-02-24 07:57:31Z glondu $ *)
 
 open Pp
 open Util
@@ -197,7 +197,8 @@ let filter_by_module_from_list = function
   | l, outside -> filter_by_module l (not outside)
 
 let filter_subproof gr _ _ =
-  not (string_string_contains (name_of_reference gr) "_subproof")
+  not (string_string_contains (name_of_reference gr) "_subproof") &&
+  not (string_string_contains (name_of_reference gr) "_admitted")
 
 let (&&&&&) f g x y z = f x y z && g x y z
 
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 9464d763..afc5057e 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: vernac.ml 13668 2010-12-02 17:43:59Z herbelin $ *)
+(* $Id: vernac.ml 13923 2011-03-21 16:25:20Z letouzey $ *)
 
 (* Parsing of vernacular. *)
 
@@ -52,8 +52,51 @@ let real_error = function
   | Error_in_file (_, _, e) -> e
   | e -> e
 
+(** Timeout handling *)
+
+(** A global default timeout, controled by option "Set Default Timeout n".
+    Use "Unset Default Timeout" to deactivate it (or set it to 0). *)
+
+let default_timeout = ref None
+
+let _ =
+  Goptions.declare_int_option
+    { Goptions.optsync  = true;
+      Goptions.optname  = "the default timeout";
+      Goptions.optkey   = ["Default";"Timeout"];
+      Goptions.optread  = (fun () -> !default_timeout);
+      Goptions.optwrite = ((:=) default_timeout) }
+
+(** When interpreting a command, the current timeout is initially
+    the default one, but may be modified locally by a Timeout command. *)
+
+let current_timeout = ref None
+
+(** Installing and de-installing a timer.
+    Note: according to ocaml documentation, Unix.alarm isn't available
+    for native win32. *)
+
 let timeout_handler _ = raise Timeout
 
+let set_timeout n =
+  let psh =
+    Sys.signal Sys.sigalrm (Sys.Signal_handle timeout_handler) in
+  ignore (Unix.alarm n);
+  Some psh
+
+let default_set_timeout () =
+  match !current_timeout with
+    | Some n -> set_timeout n
+    | None -> None
+
+let restore_timeout = function
+  | None -> ()
+  | Some psh ->
+    (* stop alarm *)
+    ignore(Unix.alarm 0);
+    (* restore handler *)
+    Sys.set_signal Sys.sigalrm psh
+
 (* Opening and closing a channel. Open it twice when verbose: the first
    channel is used to read the commands, and the second one to print them.
    Note: we could use only one thanks to seek_in, but seeking on and on in
@@ -185,25 +228,21 @@ let rec vernac_com interpfun (loc,com) =
 
     | VernacTimeout(n,v) ->
 	if not !just_parsing then begin
-	  let psh =
-	    Sys.signal Sys.sigalrm (Sys.Signal_handle timeout_handler) in
-	  ignore (Unix.alarm n);
-	  let stop() =
-	    (* stop alarm *)
-	    ignore(Unix.alarm 0);
-	    (* restore handler *)
-	    Sys.set_signal Sys.sigalrm psh in
-	  try interp v; stop()
-	  with e -> stop(); raise e
+	  current_timeout := Some n;
+	  interp v
 	end
 
     | v ->
         if not !just_parsing then
-          States.with_heavy_rollback interpfun
-            Cerrors.process_vernac_interp_error v
-
+	  let psh = default_set_timeout () in
+	  try
+            States.with_heavy_rollback interpfun
+              Cerrors.process_vernac_interp_error v;
+	    restore_timeout psh
+	  with e -> restore_timeout psh; raise e
   in
     try
+      current_timeout := !default_timeout;
       if do_beautify () then pr_new_syntax loc (Some com);
       interp com
     with e ->
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index d74711c2..7710cb95 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: vernacentries.ml 13492 2010-10-04 21:20:01Z herbelin $ i*)
+(*i $Id: vernacentries.ml 13922 2011-03-21 16:25:18Z letouzey $ i*)
 
 (* Concrete syntax of the mathematical vernacular MV V2.6 *)
 
@@ -1013,9 +1013,7 @@ let vernac_set_option locality key = function
   | BoolValue b -> set_bool_option_value_gen locality key b
 
 let vernac_unset_option locality key =
-  try set_bool_option_value_gen locality key false
-  with _ ->
-  set_int_option_value_gen locality key None
+  unset_option_value_gen locality key
 
 let vernac_add_option key lv =
   let f = function