summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--.gitignore2
-rw-r--r--CHANGES44
-rwxr-xr-xCoq.bat8
-rwxr-xr-xCoqide.bat7
-rw-r--r--INSTALL4
-rw-r--r--INSTALL.ide2
-rw-r--r--README.win12
-rw-r--r--_tags1
-rwxr-xr-xconfigure18
-rw-r--r--doc/refman/RefMan-ext.tex10
-rw-r--r--doc/refman/RefMan-oth.tex17
-rw-r--r--doc/stdlib/index-list.html.template4
-rw-r--r--ide/coq.ml10
-rw-r--r--ide/coq_icon.rc1
-rw-r--r--ide/coqide.ml20
-rw-r--r--ide/ideutils.ml10
-rw-r--r--ide/ideutils.mli3
-rw-r--r--ide/utils/configwin_messages.ml4
-rw-r--r--interp/constrextern.ml27
-rw-r--r--kernel/byterun/coq_interp.c14
-rw-r--r--kernel/names.ml8
-rw-r--r--kernel/names.mli3
-rw-r--r--lib/envars.ml7
-rw-r--r--lib/system.ml15
-rw-r--r--library/goptions.ml42
-rw-r--r--library/goptions.mli3
-rw-r--r--myocamlbuild.ml24
-rw-r--r--parsing/prettyp.ml14
-rw-r--r--parsing/tacextend.ml47
-rw-r--r--parsing/vernacextend.ml47
-rw-r--r--plugins/dp/dp_why.ml1
-rw-r--r--plugins/extraction/common.ml49
-rw-r--r--plugins/extraction/common.mli19
-rw-r--r--plugins/extraction/extract_env.ml49
-rw-r--r--plugins/extraction/extraction.ml8
-rw-r--r--plugins/extraction/haskell.ml93
-rw-r--r--plugins/extraction/mlutil.ml38
-rw-r--r--plugins/extraction/modutil.ml33
-rw-r--r--plugins/extraction/ocaml.ml82
-rw-r--r--plugins/extraction/scheme.ml44
-rw-r--r--plugins/extraction/table.ml8
-rw-r--r--plugins/extraction/table.mli3
-rw-r--r--plugins/subtac/subtac_cases.ml4
-rw-r--r--pretyping/cases.ml4
-rw-r--r--pretyping/clenv.ml4
-rw-r--r--pretyping/evd.ml6
-rw-r--r--pretyping/evd.mli4
-rw-r--r--pretyping/pretyping.ml7
-rw-r--r--pretyping/tacred.ml9
-rw-r--r--proofs/pfedit.ml8
-rw-r--r--proofs/pfedit.mli4
-rw-r--r--scripts/coqc.ml10
-rw-r--r--tactics/class_tactics.ml44
-rw-r--r--tactics/equality.ml6
-rw-r--r--tactics/tactics.ml4
-rw-r--r--test-suite/output/Extraction_matchs_2413.out38
-rw-r--r--theories/FSets/FMapAVL.v8
-rw-r--r--theories/MSets/MSetAVL.v6
-rw-r--r--tools/coqdep.ml9
-rw-r--r--tools/coqdep_common.ml3
-rw-r--r--tools/mkwinapp.ml92
-rw-r--r--toplevel/search.ml5
-rw-r--r--toplevel/vernac.ml67
-rw-r--r--toplevel/vernacentries.ml6
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