diff options
| -rw-r--r-- | INSTALL | 48 | ||||
| -rw-r--r-- | INSTALL.ide | 126 | ||||
| -rw-r--r-- | INSTALL.macosx | 20 | ||||
| -rw-r--r-- | doc/refman/CanonicalStructures.tex | 16 | ||||
| -rw-r--r-- | doc/refman/Cases.tex | 49 | ||||
| -rw-r--r-- | doc/refman/Misc.tex | 2 | ||||
| -rw-r--r-- | doc/refman/Polynom.tex | 115 | ||||
| -rw-r--r-- | doc/refman/RefMan-com.tex | 3 | ||||
| -rw-r--r-- | doc/refman/RefMan-decl.tex | 81 | ||||
| -rw-r--r-- | doc/refman/RefMan-ext.tex | 6 | ||||
| -rw-r--r-- | doc/refman/RefMan-gal.tex | 2 | ||||
| -rw-r--r-- | doc/refman/RefMan-lib.tex | 8 | ||||
| -rw-r--r-- | doc/refman/RefMan-ltac.tex | 75 | ||||
| -rw-r--r-- | doc/refman/RefMan-mod.tex | 2 | ||||
| -rw-r--r-- | doc/refman/RefMan-oth.tex | 5 | ||||
| -rw-r--r-- | doc/refman/RefMan-pro.tex | 10 | ||||
| -rw-r--r-- | doc/refman/RefMan-syn.tex | 2 | ||||
| -rw-r--r-- | doc/refman/RefMan-tac.tex | 6 | ||||
| -rw-r--r-- | doc/refman/RefMan-tacex.tex | 2 | ||||
| -rw-r--r-- | doc/refman/RefMan-uti.tex | 20 | ||||
| -rw-r--r-- | doc/refman/coqdoc.tex | 5 | ||||
| -rw-r--r-- | ide/coqOps.ml | 9 | ||||
| -rw-r--r-- | ide/wg_Segment.ml | 31 | ||||
| -rw-r--r-- | ide/wg_Segment.mli | 8 | ||||
| -rw-r--r-- | kernel/univ.ml | 2 | ||||
| -rw-r--r-- | tools/coqc.ml | 2 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 3 |
27 files changed, 351 insertions, 307 deletions
@@ -6,19 +6,6 @@ WHAT DO YOU NEED ? ================== - Coq is designed to work on computers equipped with a POSIX (Unix or a - clone) operating system. It also works under Microsoft Windows (see - INSTALL.win); for a MacOS X bundle application, see INSTALL.macosx. - - Coq is known to be actively used under GNU/Linux (i386 and amd64) and - FreeBSD. Automated tests are run under many, many different architectures - under GNU/Linux. - - Naturally, Coq will run faster on an architecture where OCaml can compile - to native code, rather than only bytecode. See - http://caml.inria.fr/ocaml/portability.en.html for details. - - Your OS may already contain Coq under the form of a precompiled package or ready-to-compile port. In this case, and if the supplied version suits you, follow the usual procedure for your OS to @@ -36,34 +23,31 @@ WHAT DO YOU NEED ? urpmi coq - - MacOS: + - MacPorts for MacOS X port install coq - Should you need or prefer to compile Coq V8.5 yourself, you need: - - - Objective Caml version 3.12.1 or later - (available at http://caml.inria.fr/) + To compile Coq V8.5 yourself, you need: - - Camlp5 (version >= 6.06) (Coq compiles with Camlp4 but might be less - well supported) + - Objective Caml version 3.12.1 or later + (available at http://caml.inria.fr/) - - GNU Make version 3.81 or later + - Camlp5 (version >= 6.02) (Coq compiles with Camlp4 but might be less + well supported) - - a C compiler + - GNU Make version 3.81 or later - - for Coqide, the Lablgtk development files, and the GTK libraries - incuding gtksourceview, see INSTALL.ide for more details + - a C compiler - By FTP, Coq comes as a single compressed tar-file. You have - probably already decompressed it if you are reading this document. + - for Coqide, the Lablgtk development files, and the GTK libraries + incuding gtksourceview, see INSTALL.ide for more details QUICK INSTALLATION PROCEDURE. ============================= 1. ./configure -2. make world +2. make 3. make install (you may need superuser rights) 4. make clean @@ -132,17 +116,13 @@ INSTALLATION PROCEDURE IN DETAILS (NORMAL USERS). Compile Coq to run in its source directory. The installation (step 6) is not necessary in that case. --opt - Use the ocamlc.opt compiler instead of ocamlc (and ocamlopt.opt - compiler instead of ocamlopt). Makes compilation faster (recommended). - -browser <command> Use <command> to open an URL in a browser. %s must appear in <command>, and will be replaced by the URL. 5- Still in the root directory, do - make world + make to compile Coq in Objective Caml bytecode (and native-code if supported). @@ -219,7 +199,7 @@ THE AVAILABLE COMMANDS. command "Require". A detailed description of these commands and of their options is given - in the Reference Manual (which you can get by FTP, in the doc/ + in the Reference Manual (which you can get in the doc/ directory, or read online on http://coq.inria.fr/doc/) and in the corresponding manual pages. @@ -291,7 +271,7 @@ DYNAMICALLY LOADED LIBRARIES FOR BYTECODE EXECUTABLES. during compilation of binary packages); - install dllcoqrun.so in a location listed in the file ld.conf that is in the directory of the standard library of OCaml; - - recompile your bytecode executables after reconfiguring the location of + - recompile your bytecode executables after reconfiguring the location of the shared library: ./configure -vmbyteflags "-dllib,-lcoqrun,-dllpath,<path>" ... where <path> is the directory where the dllcoqrun.so is installed; diff --git a/INSTALL.ide b/INSTALL.ide index 2bbb4a5fc..13e741e34 100644 --- a/INSTALL.ide +++ b/INSTALL.ide @@ -1,12 +1,9 @@ - CoqIde Installation procedure. + CoqIde Installation procedure CoqIde is a graphical interface to perform interactive proofs. You should be able to do everything you do in coqtop inside CoqIde excepted dropping to the ML toplevel. -DISCLAIMER: CoqIde is ongoing work. Although it should never let you - loose a proof, you may encounter unexpected bugs. - Do not hesitate to send suggestions/bug reports. DISTRIBUTION PACKAGES @@ -22,92 +19,87 @@ On Gentoo GNU/Linux, do: Else, read the rest of this document to compile your own CoqIde. -REQUIREMENT: - - OCaml >= 3.12.1 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.24.x. - You may still compile CoqIde with older versions and - use all features. - Run - "pkg-config --modversion gtk+-2.0" - to check your version. - All recent distributions have precompiled packages. - Do not forget to install the developement headers packages. - On Debian, installing lablgtk2 (see below) will automatically - install GTK+. (But "aptitude install libgtk2.0-dev" will - install GTK+ 2.x should you need to force it for one reason - or another.) +COMPILATION REQUIREMENTS - - The OCaml bindings for GTK+ 2.x, lablgtk2 with support for gtksourceview2. +- OCaml >= 3.12.1 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.24.x. + You may still compile CoqIde with older versions and use all features. + Run - You need at least version 2.14.2. + pkg-config --modversion gtk+-2.0 - Your distribution may contain precompiled packages. For - example, for Debian, run - aptitude install liblablgtksourceview2-ocaml-dev - for Mandriva, run - urpmi ocaml-lablgtk-devel + to check your version. + Do not forget to install the development headers packages. - If it does not, see - http://lablgtk.forge.ocamlcore.org/ + On Debian, installing lablgtk2 (see below) will automatically + install GTK+. (But "aptitude install libgtk2.0-dev" will + install GTK+ 2.x, should you need to force it for one reason + or another.) +- The OCaml bindings for GTK+ 2.x, lablgtk2 with support for gtksourceview2. + You need at least version 2.14.2. - One official releases of lablgtk2 is here: - https://forge.ocamlcore.org/frs/download.php/561/lablgtk-2.14.2.tar.gz + Your distribution may contain precompiled packages. For example, for + Debian, run - If you are in a hurry just run : + aptitude install liblablgtksourceview2-ocaml-dev - cd /tmp && \ - wget \ - https://forge.ocamlcore.org/frs/download.php/561/lablgtk-2.14.2.tar.gz && \ - tar zxvf lablgtk-2.14.2.tar.gz && \ - cd lablgtk-2.14.2 && \ - ./configure && \ - make world && \ - make install + for Mandriva, run - You must have write access to the OCaml standard library path. + urpmi ocaml-lablgtk-devel - If this fails, read lablgtk-2.14.2/README. + If it does not, see http://lablgtk.forge.ocamlcore.org/ + + The basic command installing lablgtk2 from the source package is: + + ./configure && make world && make install + + You must have write access to the OCaml standard library path. + If this fails, read lablgtk-2.14.2/README. INSTALLATION - 0) For optimal performance, OCaml must support native threads (aka pthreads). - If this not the case, this means that Coq computations will be slow and - "make ide" will fail. Use "make bin/coqide.byte" instead. To fix this - problem, just recompile OCaml from source and configure OCaml with : + +0) For optimal performance, OCaml must support native threads (aka pthreads). + If this not the case, this means that Coq computations will be slow and + "make ide" will fail. Use "make bin/coqide.byte" instead. To fix this + problem, just recompile OCaml from source and configure OCaml with: + "./configure --with-pthreads". - In case you install over an existing copy of OCaml, you should better - empty the OCaml installation directory. - 1) Go into your Coq source directory and, as usual, configure with: + In case you install over an existing copy of OCaml, you should better + empty the OCaml installation directory. + +1) Go into your Coq source directory and, as usual, configure with: ./configure - This should detect the ability of making CoqIde; check that is - says it has detected this ability and activated the building of - CoqIde. + This should detect the ability of making CoqIde; check in the + report printed by configure that ability to build CoqIde is detected. - Then compile with + Then compile with make world - and install with + and install with make install - In case you are upgrading from an old version you may need to run + In case you are upgrading from an old version you may need to run + make clean-ide -3) You may now run bin/coqide +2) You may now run bin/coqide NOTES -There are three configuration files located in your $(XDG_CONFIG_HOME)/coq dir. - You may need to set HOME to some sensible value under Windows. -- coqiderc is generated by coqide itself. It may be edited by hand or +There are three configuration files located in your $(XDG_CONFIG_HOME)/coq +dir (defaulting to $HOME/.config/coq). + +- coqiderc is generated by coqide itself. It may be edited by hand or by using the Preference menu from coqide. It will be generated the first time you save your the preferences in Coqide. @@ -119,13 +111,13 @@ Read ide/FAQ for more informations. TROUBLESHOOTING - - Problem with automatic templates +- Problem with automatic templates - Some users may experiment problems with unwanted automatic - templates while using Coqide. This is due to a change in the - modifiers keys available through GTK. The straightest way to get - rid of the problem is to edit by hand your coqiderc (either - /home/<user>/.config/coq/coqiderc under Linux, or - C:\Documents and Settings\<user>\.config\coq\coqiderc under Windows) - and replace any occurence of MOD4 by MOD1. + Some users may experiment problems with unwanted automatic + templates while using Coqide. This is due to a change in the + modifiers keys available through GTK. The straightest way to get + rid of the problem is to edit by hand your coqiderc (either + /home/<user>/.config/coq/coqiderc under Linux, or + C:\Documents and Settings\<user>\.config\coq\coqiderc under Windows) + and replace any occurence of MOD4 by MOD1. diff --git a/INSTALL.macosx b/INSTALL.macosx deleted file mode 100644 index cc1317b15..000000000 --- a/INSTALL.macosx +++ /dev/null @@ -1,20 +0,0 @@ -INSTALLATION PROCEDURE FOR THE PRECOMPILED COQ V8.1 SYSTEM UNDER MACOS X ------------------------------------------------------------------------- - -You can also use fink, or the MacOS X package prepared by the Coq -team. To use the MacOS X package,: - -1) Download archive coq-8.1-macosx-ppc.dmg (for PowerPC-base computer) - or coq-8.1-macosx-i386.dmg (for Pentium-based computer). - -2) Double-click on its icon; it mounts a disk volume named "Coq V8.1". - -3) Open volume "Coq 8.1" and double-click on coq-8.1.pkg to launch the - installer (you'll need administrator permissions). - -4) Coq installs in /usr/local/bin, which should be in your PATH, and - can be used from a Terminal window: the interactive toplevel is - named coqtop and the compiler is coqc. - -If you have any trouble with this installation, please contact: -coq-bugs@pauillac.inria.fr. diff --git a/doc/refman/CanonicalStructures.tex b/doc/refman/CanonicalStructures.tex index c8e36197c..b1c278ced 100644 --- a/doc/refman/CanonicalStructures.tex +++ b/doc/refman/CanonicalStructures.tex @@ -305,15 +305,21 @@ canonical structures. We need some infrastructure for that. -\begin{coq_example} +\begin{coq_example*} Require Import Strings.String. +\end{coq_example*} +\begin{coq_example} Module infrastructure. Inductive phantom {T : Type} (t : T) : Type := Phantom. - Definition unify {T1 T2} (t1 : T1) (t2 : T2) (s : option string) := phantom t1 -> phantom t2. + Definition unify {T1 T2} (t1 : T1) (t2 : T2) (s : option string) := + phantom t1 -> phantom t2. Definition id {T} {t : T} (x : phantom t) := x. - Notation "[find v | t1 ~ t2 ] p" := (fun v (_ : unify t1 t2 None) => p) (at level 50, v ident, only parsing). - Notation "[find v | t1 ~ t2 | s ] p" := (fun v (_ : unify t1 t2 (Some s)) => p) (at level 50, v ident, only parsing). - Notation "'Error : t : s" := (unify _ t (Some s)) (at level 50, format "''Error' : t : s"). + Notation "[find v | t1 ~ t2 ] p" := (fun v (_ : unify t1 t2 None) => p) + (at level 50, v ident, only parsing). + Notation "[find v | t1 ~ t2 | s ] p" := (fun v (_ : unify t1 t2 (Some s)) => p) + (at level 50, v ident, only parsing). + Notation "'Error : t : s" := (unify _ t (Some s)) + (at level 50, format "''Error' : t : s"). Open Scope string_scope. End infrastructure. \end{coq_example} diff --git a/doc/refman/Cases.tex b/doc/refman/Cases.tex index 7e01edeb0..51ec2ef81 100644 --- a/doc/refman/Cases.tex +++ b/doc/refman/Cases.tex @@ -77,8 +77,10 @@ Fixpoint max (n m:nat) {struct m} : nat := Using multiple patterns in the definition of {\tt max} lets us write: -\begin{coq_example} +\begin{coq_eval} Reset max. +\end{coq_eval} +\begin{coq_example} Fixpoint max (n m:nat) {struct m} : nat := match n, m with | O, _ => m @@ -105,8 +107,10 @@ Check (fun x:nat => match x return nat with We can also use ``\texttt{as} {\ident}'' to associate a name to a sub-pattern: -\begin{coq_example} +\begin{coq_eval} Reset max. +\end{coq_eval} +\begin{coq_example} Fixpoint max (n m:nat) {struct n} : nat := match n, m with | O, _ => m @@ -133,8 +137,10 @@ This is compiled into: \begin{coq_example} Unset Printing Matching. Print even. -Set Printing Matching. \end{coq_example} +\begin{coq_eval} +Set Printing Matching. +\end{coq_eval} In the previous examples patterns do not conflict with, but sometimes it is comfortable to write patterns that admit a non @@ -164,8 +170,10 @@ yields \texttt{true}. Another way to write this function is: -\begin{coq_example} +\begin{coq_eval} Reset lef. +\end{coq_eval} +\begin{coq_example} Fixpoint lef (n m:nat) {struct m} : bool := match n, m with | O, x => true @@ -181,11 +189,9 @@ the second one. Terms with useless patterns are not accepted by the system. Here is an example: -% Test failure +% Test failure: "This clause is redundant." \begin{coq_eval} Set Printing Depth 50. - (********** The following is not correct and should produce **********) - (**************** Error: This clause is redundant ********************) \end{coq_eval} \begin{coq_example} Check (fun x:nat => @@ -260,11 +266,9 @@ Check When we use parameters in patterns there is an error message: -% Test failure +% Test failure: "The parameters do not bind in patterns." \begin{coq_eval} Set Printing Depth 50. -(********** The following is not correct and should produce **********) -(******** Error: Parameters do not bind ... ************) \end{coq_eval} \begin{coq_example} Check @@ -324,8 +328,10 @@ Definition length (n:nat) (l:listn n) := n. Just for illustrating pattern matching, we can define it by case analysis: -\begin{coq_example} +\begin{coq_eval} Reset length. +\end{coq_eval} +\begin{coq_example} Definition length (n:nat) (l:listn n) := match l with | niln => 0 @@ -454,8 +460,10 @@ introduce a dependent product. For example, an equivalent definition for \texttt{concat} (even though the matching on the second term is trivial) would have been: -\begin{coq_example} +\begin{coq_eval} Reset concat. +\end{coq_eval} +\begin{coq_example} Fixpoint concat (n:nat) (l:listn n) (m:nat) (l':listn m) {struct l} : listn (n + m) := match l in listn n, l' return listn (n + m) with @@ -517,17 +525,18 @@ If the type of the matched term is more precise than an inductive applied to variables, arguments of the inductive in the {\tt in} branch can be more complicated patterns than a variable. -Moreover, constructors whose type do not follow the same pattern will become -impossible branch. In impossible branch, you can answer anything but {\tt - False\_rect unit} has the advantage to be subterm of anything. +Moreover, constructors whose type do not follow the same pattern will +become impossible branches. In an impossible branch, you can answer +anything but {\tt False\_rect unit} has the advantage to be subterm of +anything. % ??? To be concrete: the tail function can be written: \begin{coq_example} - Definition tail n (v: listn (S n)) := - match v in listn (S m) return listn m with - | niln => False_rect unit - | consn n' a y => y - end. +Definition tail n (v: listn (S n)) := + match v in listn (S m) return listn m with + | niln => False_rect unit + | consn n' a y => y + end. \end{coq_example} and {\tt tail n v} will be subterm of {\tt v}. diff --git a/doc/refman/Misc.tex b/doc/refman/Misc.tex index 6ce4ee480..e953d2f70 100644 --- a/doc/refman/Misc.tex +++ b/doc/refman/Misc.tex @@ -30,7 +30,7 @@ always transparent. \Example \begin{coq_example*} -Require Coq.Derive.Derive. +Require Coq.derive.Derive. Require Import Coq.Numbers.Natural.Peano.NPeano. Section P. diff --git a/doc/refman/Polynom.tex b/doc/refman/Polynom.tex index 974a56247..0664bf909 100644 --- a/doc/refman/Polynom.tex +++ b/doc/refman/Polynom.tex @@ -122,8 +122,10 @@ for \texttt{N}, do \texttt{Require Import NArithRing} or \begin{coq_eval} Reset Initial. \end{coq_eval} -\begin{coq_example} +\begin{coq_example*} Require Import ZArith. +\end{coq_example*} +\begin{coq_example} Open Scope Z_scope. Goal forall a b c:Z, (a + b + c)^2 = @@ -193,28 +195,28 @@ also supported. The equality can be either Leibniz equality, or any relation declared as a setoid (see~\ref{setoidtactics}). The definition of ring and semi-rings (see module {\tt Ring\_theory}) is: \begin{verbatim} - Record ring_theory : Prop := mk_rt { - Radd_0_l : forall x, 0 + x == x; - Radd_sym : forall x y, x + y == y + x; - Radd_assoc : forall x y z, x + (y + z) == (x + y) + z; - Rmul_1_l : forall x, 1 * x == x; - Rmul_sym : forall x y, x * y == y * x; - Rmul_assoc : forall x y z, x * (y * z) == (x * y) * z; - Rdistr_l : forall x y z, (x + y) * z == (x * z) + (y * z); - Rsub_def : forall x y, x - y == x + -y; - Ropp_def : forall x, x + (- x) == 0 - }. +Record ring_theory : Prop := mk_rt { + Radd_0_l : forall x, 0 + x == x; + Radd_sym : forall x y, x + y == y + x; + Radd_assoc : forall x y z, x + (y + z) == (x + y) + z; + Rmul_1_l : forall x, 1 * x == x; + Rmul_sym : forall x y, x * y == y * x; + Rmul_assoc : forall x y z, x * (y * z) == (x * y) * z; + Rdistr_l : forall x y z, (x + y) * z == (x * z) + (y * z); + Rsub_def : forall x y, x - y == x + -y; + Ropp_def : forall x, x + (- x) == 0 +}. Record semi_ring_theory : Prop := mk_srt { - SRadd_0_l : forall n, 0 + n == n; - SRadd_sym : forall n m, n + m == m + n ; - SRadd_assoc : forall n m p, n + (m + p) == (n + m) + p; - SRmul_1_l : forall n, 1*n == n; - SRmul_0_l : forall n, 0*n == 0; - SRmul_sym : forall n m, n*m == m*n; - SRmul_assoc : forall n m p, n*(m*p) == (n*m)*p; - SRdistr_l : forall n m p, (n + m)*p == n*p + m*p - }. + SRadd_0_l : forall n, 0 + n == n; + SRadd_sym : forall n m, n + m == m + n ; + SRadd_assoc : forall n m p, n + (m + p) == (n + m) + p; + SRmul_1_l : forall n, 1*n == n; + SRmul_0_l : forall n, 0*n == 0; + SRmul_sym : forall n m, n*m == m*n; + SRmul_assoc : forall n m p, n*(m*p) == (n*m)*p; + SRdistr_l : forall n m p, (n + m)*p == n*p + m*p +}. \end{verbatim} This implementation of {\tt ring} also features a notion of constant @@ -230,23 +232,23 @@ could be the rational numbers, upon which the ring operations can be implemented. The fact that there exists a morphism is defined by the following properties: \begin{verbatim} - Record ring_morph : Prop := mkmorph { - morph0 : [cO] == 0; - morph1 : [cI] == 1; - morph_add : forall x y, [x +! y] == [x]+[y]; - morph_sub : forall x y, [x -! y] == [x]-[y]; - morph_mul : forall x y, [x *! y] == [x]*[y]; - morph_opp : forall x, [-!x] == -[x]; - morph_eq : forall x y, x?=!y = true -> [x] == [y] - }. +Record ring_morph : Prop := mkmorph { + morph0 : [cO] == 0; + morph1 : [cI] == 1; + morph_add : forall x y, [x +! y] == [x]+[y]; + morph_sub : forall x y, [x -! y] == [x]-[y]; + morph_mul : forall x y, [x *! y] == [x]*[y]; + morph_opp : forall x, [-!x] == -[x]; + morph_eq : forall x y, x?=!y = true -> [x] == [y] +}. - Record semi_morph : Prop := mkRmorph { - Smorph0 : [cO] == 0; - Smorph1 : [cI] == 1; - Smorph_add : forall x y, [x +! y] == [x]+[y]; - Smorph_mul : forall x y, [x *! y] == [x]*[y]; - Smorph_eq : forall x y, x?=!y = true -> [x] == [y] - }. +Record semi_morph : Prop := mkRmorph { + Smorph0 : [cO] == 0; + Smorph1 : [cI] == 1; + Smorph_add : forall x y, [x +! y] == [x]+[y]; + Smorph_mul : forall x y, [x *! y] == [x]*[y]; + Smorph_eq : forall x y, x?=!y = true -> [x] == [y] +}. \end{verbatim} where {\tt c0} and {\tt cI} denote the 0 and 1 of the coefficient set, {\tt +!}, {\tt *!}, {\tt -!} are the implementations of the ring @@ -274,16 +276,16 @@ This implementation of ring can also recognize simple power expressions as ring expressions. A power function is specified by the following property: \begin{verbatim} - Section POWER. +Section POWER. Variable Cpow : Set. Variable Cp_phi : N -> Cpow. - Variable rpow : R -> Cpow -> R. - + Variable rpow : R -> Cpow -> R. + Record power_theory : Prop := mkpow_th { rpow_pow_N : forall r n, req (rpow r (Cp_phi n)) (pow_N rI rmul r n) }. - End POWER. +End POWER. \end{verbatim} @@ -398,7 +400,7 @@ Polynomials in normal form are defined as: \begin{small} \begin{flushleft} \begin{verbatim} - Inductive Pol : Type := +Inductive Pol : Type := | Pc : C -> Pol | Pinj : positive -> Pol -> Pol | PX : Pol -> positive -> Pol -> Pol. @@ -501,8 +503,10 @@ field in module \texttt{Qcanon}. \begin{coq_eval} Reset Initial. \end{coq_eval} -\begin{coq_example} +\begin{coq_example*} Require Import Reals. +\end{coq_example*} +\begin{coq_example} Open Scope R_scope. Goal forall x, x <> 0 -> (1 - 1/x) * x - x + 1 = 0. @@ -600,17 +604,17 @@ relation declared as a setoid (see~\ref{setoidtactics}). The definition of fields and semi-fields is: \begin{verbatim} Record field_theory : Prop := mk_field { - F_R : ring_theory rO rI radd rmul rsub ropp req; - F_1_neq_0 : ~ 1 == 0; - Fdiv_def : forall p q, p / q == p * / q; - Finv_l : forall p, ~ p == 0 -> / p * p == 1 + F_R : ring_theory rO rI radd rmul rsub ropp req; + F_1_neq_0 : ~ 1 == 0; + Fdiv_def : forall p q, p / q == p * / q; + Finv_l : forall p, ~ p == 0 -> / p * p == 1 }. Record semi_field_theory : Prop := mk_sfield { - SF_SR : semi_ring_theory rO rI radd rmul req; - SF_1_neq_0 : ~ 1 == 0; - SFdiv_def : forall p q, p / q == p * / q; - SFinv_l : forall p, ~ p == 0 -> / p * p == 1 + SF_SR : semi_ring_theory rO rI radd rmul req; + SF_1_neq_0 : ~ 1 == 0; + SFdiv_def : forall p q, p / q == p * / q; + SFinv_l : forall p, ~ p == 0 -> / p * p == 1 }. \end{verbatim} @@ -618,9 +622,10 @@ The result of the normalization process is a fraction represented by the following type: \begin{verbatim} Record linear : Type := mk_linear { - num : PExpr C; - denum : PExpr C; - condition : list (PExpr C) }. + num : PExpr C; + denum : PExpr C; + condition : list (PExpr C) +}. \end{verbatim} where {\tt num} and {\tt denum} are the numerator and denominator; {\tt condition} is a list of expressions that have appeared as a @@ -661,7 +666,7 @@ intros; rewrite (Z.mul_comm y z); reflexivity. Save toto. \end{coq_example*} \begin{coq_example} -Print toto. +Print toto. \end{coq_example} At each step of rewriting, the whole context is duplicated in the proof diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex index a93733256..49bcdb1db 100644 --- a/doc/refman/RefMan-com.tex +++ b/doc/refman/RefMan-com.tex @@ -1,6 +1,7 @@ \chapter[The \Coq~commands]{The \Coq~commands\label{Addoc-coqc} \ttindex{coqtop} -\ttindex{coqc}} +\ttindex{coqc} +\ttindex{coqchk}} There are three \Coq~commands: \begin{itemize} diff --git a/doc/refman/RefMan-decl.tex b/doc/refman/RefMan-decl.tex index 292b8bbed..c84e3a9df 100644 --- a/doc/refman/RefMan-decl.tex +++ b/doc/refman/RefMan-decl.tex @@ -16,7 +16,7 @@ The intent is to provide language where proofs are less formalism-{} and implementation-{}sensitive, and in the process to ease a bit the learning of computer-{}aided proof verification. -\subsection{What is a declarative proof ?{}} +\subsection{What is a declarative proof?} In vanilla Coq, proofs are written in the imperative style: the user issues commands that transform a so called proof state until it reaches a state where the proof is completed. In the process, the user @@ -48,7 +48,7 @@ correct: \subsection{Note for tactics users} This section explain what differences the casual Coq user will -experience using the \DPL . +experience using the \DPL. \begin{enumerate} \item The focusing mechanism is constrained so that only one goal at a time is visible. @@ -77,7 +77,7 @@ However it is not supported by structured editors such as PCoq. \section{Syntax} -Here is a complete formal description of the syntax for DPL commands. +Here is a complete formal description of the syntax for \DPL{} commands. \begin{figure}[htbp] \begin{centerframe} @@ -127,7 +127,7 @@ The lexical conventions used here follows those of section \ref{lexical}. Conventions:\begin{itemize} - \item {\texttt{<{}tactic>{}}} stands for an Coq tactic. + \item {\texttt{<{}tactic>{}}} stands for a Coq tactic. \end{itemize} @@ -135,7 +135,7 @@ Conventions:\begin{itemize} In proof commands where an optional name is asked for, omitting the name will trigger the creation of a fresh temporary name (e.g. for a -hypothesis). Temporary names always start with an undescore '\_' +hypothesis). Temporary names always start with an underscore `\_' character (e.g. {\tt \_hyp0}). Temporary names have a lifespan of one command: they get erased after the next command. They can however be safely in the step after their creation. @@ -143,7 +143,12 @@ command: they get erased after the next command. They can however be safely in t \subsection{Starting and Ending a mathematical proof} - The standard way to use the \DPL is to first state a {\texttt{Lemma/Theorem/Definition}} and then use the {\texttt{proof}} command to switch the current subgoal to mathematical mode. After the proof is completed, the {\texttt{end proof}} command will close the mathematical proof. If any subgoal remains to be proved, they will be displayed using the usual Coq display. +The standard way to use the \DPL{} is to first state a \texttt{Lemma} / +\texttt{Theorem} / \texttt{Definition} and then use the \texttt{proof} +command to switch the current subgoal to mathematical mode. After the +proof is completed, the \texttt{end proof} command will close the +mathematical proof. If any subgoal remains to be proved, they will be +displayed using the usual Coq display. \begin{coq_example} Theorem this_is_trivial: True. @@ -154,13 +159,13 @@ Qed. \end{coq_example} The {\texttt{proof}} command only applies to \emph{one subgoal}, thus -if several sub-goals are already present, the {\texttt{proof .. end +if several sub-goals are already present, the {\texttt{proof ... end proof}} sequence has to be used several times. -\begin{coq_eval} +\begin{coq_example*} Theorem T: (True /\ True) /\ True. split. split. -\end{coq_eval} +\end{coq_example*} \begin{coq_example} Show. proof. (* first subgoal *) @@ -187,7 +192,7 @@ later. Theorem this_is_not_so_trivial: False. proof. end proof. (* here a warning is issued *) -Qed. (* fails : the proof in incomplete *) +Qed. (* fails: the proof in incomplete *) Admitted. (* Oops! *) \end{coq_example} \begin{coq_eval} @@ -220,7 +225,7 @@ warning is issued and the proof cannot be saved anymore. It is possible to use the {\texttt{proof}} command inside an {\texttt{escape...return}} block, thus nesting a mathematical proof -inside a procedural proof inside a mathematical proof ... +inside a procedural proof inside a mathematical proof... \subsection{Computation steps} @@ -244,8 +249,10 @@ Abort. \subsection{Deduction steps} -The most common instruction in a mathematical proof is the deduction step: - it asserts a new statement (a formula/type of the \CIC) and tries to prove it using a user-provided indication : the justification. The asserted statement is then added as a hypothesis to the proof context. +The most common instruction in a mathematical proof is the deduction +step: it asserts a new statement (a formula/type of the \CIC) and tries +to prove it using a user-provided indication: the justification. The +asserted statement is then added as a hypothesis to the proof context. \begin{coq_eval} Theorem T: forall x, x=2 -> 2+x=4. @@ -260,7 +267,9 @@ let x be such that H:(x=2). Abort. \end{coq_eval} -It is very often the case that the justifications uses the last hypothesis introduced in the context, so the {\tt then} keyword can be used as a shortcut, e.g. if we want to do the same as the last example : +It is often the case that the justifications uses the last hypothesis +introduced in the context, so the {\tt then} keyword can be used as a +shortcut, e.g. if we want to do the same as the last example: \begin{coq_eval} Theorem T: forall x, x=2 -> 2+x=4. @@ -279,7 +288,7 @@ In this example, you can also see the creation of a temporary name {\tt \_fact}. \subsection{Iterated equalities} -A common proof pattern when doing a chain of deductions, is to do +A common proof pattern when doing a chain of deductions is to do multiple rewriting steps over the same term, thus proving the corresponding equalities. The iterated equalities are a syntactic support for this kind of reasoning: @@ -305,7 +314,10 @@ Notice that here we use temporary names heavily. \subsection{Subproofs} -When an intermediate step in a proof gets too complicated or involves a well contained set of intermediate deductions, it can be useful to insert its proof as a subproof of the current proof. this is done by using the {\tt claim ... end claim} pair of commands. +When an intermediate step in a proof gets too complicated or involves a +well contained set of intermediate deductions, it can be useful to insert +its proof as a subproof of the current proof. This is done by using the +{\tt claim ... end claim} pair of commands. \begin{coq_eval} Theorem T: forall x, x + x = x * x -> x = 0 \/ x = 2. @@ -317,7 +329,7 @@ Show. claim H':((x - 2) * x = 0). \end{coq_example} -A few steps later ... +A few steps later... \begin{coq_example} thus thesis. @@ -350,7 +362,7 @@ conclusion step & {\tt thus} & {\tt hence} & \caption{Correspondence between basic forward steps and conclusion steps} \end{figure} -Let us begin with simple examples : +Let us begin with simple examples: \begin{coq_eval} Theorem T: forall (A B:Prop), A -> B -> A /\ B. @@ -381,7 +393,7 @@ thus B by HB. Abort. \end{coq_eval} -The command fails the refinement process cannot find a place to fit +The command fails if the refinement process cannot find a place to fit the object in a proof of the conclusion. @@ -494,7 +506,7 @@ suffices to have x such that HP':(P x) to show B by HP,HP'. Abort. \end{coq_eval} -Finally, an example where {\tt focus} is handy : local assumptions. +Finally, an example where {\tt focus} is handy: local assumptions. \begin{coq_eval} Theorem T: forall (A:Prop) (P:nat -> Prop), P 2 -> A -> A /\ (forall x, x = 2 -> P x). @@ -518,7 +530,7 @@ In order to shorten long expressions, it is possible to use the {\tt define ... as ...} command to give a name to recurring expressions. \begin{coq_eval} -Theorem T: forall x, x = 0 -> x + x = x * x . +Theorem T: forall x, x = 0 -> x + x = x * x. proof. let x be such that H:(x = 0). \end{coq_eval} @@ -534,10 +546,12 @@ Abort. \subsection{Introduction steps} When the {\tt thesis} consists of a hypothetical formula (implication -or universal quantification (e.g. \verb+A -> B+) , it is possible to +or universal quantification (e.g. \verb+A -> B+), it is possible to assume the hypothetical part {\tt A} and then prove {\tt B}. In the \DPL{}, this comes in two syntactic flavors that are semantically -equivalent : {\tt let} and {\tt assume}. Their syntax is designed so that {\tt let} works better for universal quantifiers and {\tt assume} for implications. +equivalent: {\tt let} and {\tt assume}. Their syntax is designed so that +{\tt let} works better for universal quantifiers and {\tt assume} for +implications. \begin{coq_eval} Theorem T: forall (P:nat -> Prop), forall x, P x -> P x. @@ -571,7 +585,8 @@ let x be such that HP:(P x). (* here x's type is inferred from (P x) *) Abort. \end{coq_eval} -In the {\tt assume } variant, the type of the assumed object is mandatory but the name is optional : +In the {\tt assume } variant, the type of the assumed object is mandatory +but the name is optional: \begin{coq_eval} Theorem T: forall (P:nat -> Prop), forall x, P x -> P x -> P x. @@ -587,7 +602,7 @@ assume (P x). (* temporary name created *) Abort. \end{coq_eval} -After {\tt such that}, it is also the case : +After {\tt such that}, it is also the case: \begin{coq_eval} Theorem T: forall (P:nat -> Prop), forall x, P x -> P x. @@ -604,8 +619,8 @@ Abort. \subsection{Tuple elimination steps} -In the \CIC, many objects dealt with in simple proofs are tuples : -pairs , records, existentially quantified formulas. These are so +In the \CIC, many objects dealt with in simple proofs are tuples: +pairs, records, existentially quantified formulas. These are so common that the \DPL{} provides a mechanism to extract members of those tuples, and also objects in tuples within tuples within tuples... @@ -613,7 +628,7 @@ tuples... \begin{coq_eval} Theorem T: forall (P:nat -> Prop) (A:Prop), (exists x, (P x /\ A)) -> A. proof. -let P:(nat -> Prop),A:Prop be such that H:(exists x, P x /\ A) . +let P:(nat -> Prop),A:Prop be such that H:(exists x, P x /\ A). \end{coq_eval} \begin{coq_example} Show. @@ -643,10 +658,10 @@ It is sometimes desirable to combine assumption and tuple decomposition. This can be done using the {\tt given} command. \begin{coq_eval} -Theorem T: forall P:(nat -> Prop), (forall n , P n -> P (n - 1)) -> +Theorem T: forall P:(nat -> Prop), (forall n, P n -> P (n - 1)) -> (exists m, P m) -> P 0. proof. -let P:(nat -> Prop) be such that HP:(forall n , P n -> P (n - 1)). +let P:(nat -> Prop) be such that HP:(forall n, P n -> P (n - 1)). \end{coq_eval} \begin{coq_example} Show. @@ -687,7 +702,7 @@ The proof is well formed (but incomplete) even if you type {\tt end If the disjunction is derived from a more general principle, e.g. the excluded middle axiom), it is desirable to just specify which instance -of it is being used : +of it is being used: \begin{coq_eval} Section Coq. @@ -789,14 +804,14 @@ Intuitively, justifications are hints for the system to understand how to prove the statements the user types in. In the case of this language justifications are made of two components: -Justification objects : {\texttt{by}} followed by a comma-{}separated +Justification objects: {\texttt{by}} followed by a comma-{}separated list of objects that will be used by a selected tactic to prove the statement. This defaults to the empty list (the statement should then be tautological). The * wildcard provides the usual tactics behavior: use all statements in local context. However, this wildcard should be avoided since it reduces the robustness of the script. -Justification tactic : {\texttt{using}} followed by a Coq tactic that +Justification tactic: {\texttt{using}} followed by a Coq tactic that is executed to prove the statement. The default is a solver for (intuitionistic) first-{}order with equality. diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex index 193479cce..3605a716e 100644 --- a/doc/refman/RefMan-ext.tex +++ b/doc/refman/RefMan-ext.tex @@ -167,7 +167,7 @@ defined with the {\tt Record} keyword can be activated with the (see~\ref{set-nonrecursive-elimination-schemes}). \begin{Warnings} -\item {\tt Warning: {\ident$_i$} cannot be defined.} +\item {\tt {\ident$_i$} cannot be defined.} It can happen that the definition of a projection is impossible. This message is followed by an explanation of this impossibility. @@ -434,7 +434,7 @@ we have an equivalence between {\tt match {\term} \zeroone{\ifitem} with C {\ident}$_1$ {\ldots} {\ident}$_n$ \verb!=>! {\term}' end} -\subsubsection{Second destructuring {\tt let} syntax\index{let '... in}} +\subsubsection{Second destructuring {\tt let} syntax\index{let '... in@\texttt{let '... in}}} Another destructuring {\tt let} syntax is available for inductive types with one constructor by giving an arbitrary pattern instead of just a tuple @@ -2000,7 +2000,7 @@ variables, use \end{quote} \subsection{Solving existential variables using tactics} -\index{\tt \textdollar( \ldots )\textdollar} +\ttindex{\textdollar( \ldots )\textdollar} \def\expr{\textrm{\textsl{tacexpr}}} diff --git a/doc/refman/RefMan-gal.tex b/doc/refman/RefMan-gal.tex index 68a2e5dac..0d628ac7e 100644 --- a/doc/refman/RefMan-gal.tex +++ b/doc/refman/RefMan-gal.tex @@ -900,7 +900,7 @@ These are synonyms of the {\tt Definition} forms. \end{Variants} \begin{ErrMsgs} -\item \errindex{Error: The term {\term} has type {\type} while it is expected to have type {\type}} +\item \errindex{The term {\term} has type {\type} while it is expected to have type {\type}} \end{ErrMsgs} \SeeAlso Sections \ref{Opaque}, \ref{Transparent}, \ref{unfold}. diff --git a/doc/refman/RefMan-lib.tex b/doc/refman/RefMan-lib.tex index 49382f3e2..7227f4b7b 100644 --- a/doc/refman/RefMan-lib.tex +++ b/doc/refman/RefMan-lib.tex @@ -892,8 +892,10 @@ Figure~\ref{zarith-syntax} shows the notations provided by {\tt Z\_scope}. It specifies how notations are interpreted and, when not already reserved, the precedence and associativity. -\begin{coq_example} +\begin{coq_example*} Require Import ZArith. +\end{coq_example*} +\begin{coq_example} Check (2 + 3)%Z. Open Scope Z_scope. Check 2 + 3. @@ -968,8 +970,10 @@ Notation & Interpretation \\ \begin{coq_eval} Reset Initial. \end{coq_eval} -\begin{coq_example} +\begin{coq_example*} Require Import Reals. +\end{coq_example*} +\begin{coq_example} Check (2 + 3)%R. Open Scope R_scope. Check 2 + 3. diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex index de8c26943..689ac1425 100644 --- a/doc/refman/RefMan-ltac.tex +++ b/doc/refman/RefMan-ltac.tex @@ -620,10 +620,10 @@ runs is displayed. Time is in seconds and is machine-dependent. The {\qstring} argument is optional. When provided, it is used to identify this particular occurrence of {\tt time}. -\subsubsection[Local definitions]{Local definitions\index{Ltac!let} -\index{Ltac!let rec} -\index{let!in Ltac} -\index{let rec!in Ltac}} +\subsubsection[Local definitions]{Local definitions\index{Ltac!let@\texttt{let}} +\index{Ltac!let rec@\texttt{let rec}} +\index{let@\texttt{let}!in Ltac} +\index{let rec@\texttt{let rec}!in Ltac}} Local definitions can be done as follows: \begin{quote} @@ -659,8 +659,8 @@ definition expecting at least $n$ arguments. The expressions %\subsection{Application of tactic values} -\subsubsection[Function construction]{Function construction\index{fun!in Ltac} -\index{Ltac!fun}} +\subsubsection[Function construction]{Function construction\index{fun@\texttt{fun}!in Ltac} +\index{Ltac!fun@\texttt{fun}}} A parameterized tactic can be built anonymously (without resorting to local definitions) with: @@ -670,8 +670,8 @@ local definitions) with: Indeed, local definitions of functions are a syntactic sugar for binding a {\tt fun} tactic to an identifier. -\subsubsection[Pattern matching on terms]{Pattern matching on terms\index{Ltac!match} -\index{match!in Ltac}} +\subsubsection[Pattern matching on terms]{Pattern matching on terms\index{Ltac!match@\texttt{match}} +\index{match@\texttt{match}!in Ltac}} We can carry out pattern matching on terms with: \begin{quote} @@ -729,8 +729,8 @@ it has backtracking points. \begin{Variants} -\item \index{multimatch!in Ltac} -\index{Ltac!multimatch} +\item \index{multimatch@\texttt{multimatch}!in Ltac} +\index{Ltac!multimatch@\texttt{multimatch}} Using {\tt multimatch} instead of {\tt match} will allow subsequent tactics to backtrack into a right-hand side tactic which has backtracking points left and trigger the selection of a new matching @@ -740,8 +740,8 @@ been consumed. The syntax {\tt match \ldots} is, in fact, a shorthand for {\tt once multimatch \ldots}. -\item \index{lazymatch!in Ltac} -\index{Ltac!lazymatch} +\item \index{lazymatch@\texttt{lazymatch}!in Ltac} +\index{Ltac!lazymatch@\texttt{lazymatch}} Using {\tt lazymatch} instead of {\tt match} will perform the same pattern matching procedure but will commit to the first matching branch rather than trying a new matching if the right-hand side @@ -749,7 +749,7 @@ fails. If the right-hand side of the selected branch is a tactic with backtracking points, then subsequent failures cause this tactic to backtrack. -\item \index{context!in pattern} +\item \index{context@\texttt{context}!in pattern} There is a special form of patterns to match a subterm against the pattern: \begin{quote} @@ -778,7 +778,7 @@ Goal True. f (3+4). \end{coq_example} -\item \index{appcontext!in pattern} +\item \index{appcontext@\texttt{appcontext}!in pattern} \comindex{Set Tactic Compat Context} \comindex{Unset Tactic Compat Context} For historical reasons, {\tt context} used to consider $n$-ary applications @@ -796,10 +796,10 @@ behavior can be retrieved with the {\tt Tactic Compat Context} flag. \end{Variants} -\subsubsection[Pattern matching on goals]{Pattern matching on goals\index{Ltac!match goal} -\index{Ltac!match reverse goal} -\index{match goal!in Ltac} -\index{match reverse goal!in Ltac}} +\subsubsection[Pattern matching on goals]{Pattern matching on goals\index{Ltac!match goal@\texttt{match goal}} +\index{Ltac!match reverse goal@\texttt{match reverse goal}} +\index{match goal@\texttt{match goal}!in Ltac} +\index{match reverse goal@\texttt{match reverse goal}!in Ltac}} We can make pattern matching on goals using the following expression: \begin{quote} @@ -854,10 +854,10 @@ the {\tt match reverse goal with} variant. \variant -\index{multimatch goal!in Ltac} -\index{Ltac!multimatch goal} -\index{multimatch reverse goal!in Ltac} -\index{Ltac!multimatch reverse goal} +\index{multimatch goal@\texttt{multimatch goal}!in Ltac} +\index{Ltac!multimatch goal@\texttt{multimatch goal}} +\index{multimatch reverse goal@\texttt{multimatch reverse goal}!in Ltac} +\index{Ltac!multimatch reverse goal@\texttt{multimatch reverse goal}} Using {\tt multimatch} instead of {\tt match} will allow subsequent tactics to backtrack into a right-hand side tactic which has @@ -868,10 +868,10 @@ of the right-hand side have been consumed. The syntax {\tt match [reverse] goal \ldots} is, in fact, a shorthand for {\tt once multimatch [reverse] goal \ldots}. -\index{lazymatch goal!in Ltac} -\index{Ltac!lazymatch goal} -\index{lazymatch reverse goal!in Ltac} -\index{Ltac!lazymatch reverse goal} +\index{lazymatch goal@\texttt{lazymatch goal}!in Ltac} +\index{Ltac!lazymatch goal@\texttt{lazymatch goal}} +\index{lazymatch reverse goal@\texttt{lazymatch reverse goal}!in Ltac} +\index{Ltac!lazymatch reverse goal@\texttt{lazymatch reverse goal}} Using {\tt lazymatch} instead of {\tt match} will perform the same pattern matching procedure but will commit to the first matching branch with the first matching combination of hypotheses rather than @@ -879,7 +879,7 @@ trying a new matching if the right-hand side fails. If the right-hand side of the selected branch is a tactic with backtracking points, then subsequent failures cause this tactic to backtrack. -\subsubsection[Filling a term context]{Filling a term context\index{context!in expression}} +\subsubsection[Filling a term context]{Filling a term context\index{context@\texttt{context}!in expression}} The following expression is not a tactic in the sense that it does not produce subgoals but generates a term to be used in tactic @@ -895,8 +895,8 @@ replaces the hole of the value of {\ident} by the value of \ErrMsg \errindex{not a context variable} -\subsubsection[Generating fresh hypothesis names]{Generating fresh hypothesis names\index{Ltac!fresh} -\index{fresh!in Ltac}} +\subsubsection[Generating fresh hypothesis names]{Generating fresh hypothesis names\index{Ltac!fresh@\texttt{fresh}} +\index{fresh@\texttt{fresh}!in Ltac}} Tactics sometimes have to generate new names for hypothesis. Letting the system decide a name with the {\tt intro} tactic is not so good @@ -913,8 +913,8 @@ has to refer to a name, or directly a name denoted by a with a number so that it becomes fresh. If no component is given, the name is a fresh derivative of the name {\tt H}. -\subsubsection[Computing in a constr]{Computing in a constr\index{Ltac!eval} -\index{eval!in Ltac}} +\subsubsection[Computing in a constr]{Computing in a constr\index{Ltac!eval@\texttt{eval}} +\index{eval@\texttt{eval}!in Ltac}} Evaluation of a term can be performed with: \begin{quote} @@ -926,8 +926,8 @@ hnf}, {\tt compute}, {\tt simpl}, {\tt cbv}, {\tt lazy}, {\tt unfold}, \subsubsection{Recovering the type of a term} %\tacindex{type of} -\index{Ltac!type of} -\index{type of!in Ltac} +\index{Ltac!type of@\texttt{type of}} +\index{type of@\texttt{type of}!in Ltac} The following returns the type of {\term}: @@ -935,7 +935,10 @@ The following returns the type of {\term}: {\tt type of} {\term} \end{quote} -\subsubsection[Manipulating untyped terms]{Manipulating untyped terms\index{Ltac!uconstr}\index{uconstr!in Ltac}\index{Ltac!type\_term}\index{type\_term!in Ltac}} +\subsubsection[Manipulating untyped terms]{Manipulating untyped terms\index{Ltac!uconstr@\texttt{uconstr}} +\index{uconstr@\texttt{uconstr}!in Ltac} +\index{Ltac!type\_term@\texttt{type\_term}} +\index{type\_term@\texttt{type\_term}!in Ltac}} The terms built in Ltac are well-typed by default. It may not be appropriate for building large terms using a recursive Ltac function: @@ -963,7 +966,7 @@ untyped term is type checked against the conclusion of the goal, and the holes which are not solved by the typing procedure are turned into new subgoals. -\subsubsection[Counting the goals]{Counting the goals\index{Ltac!numgoals}\index{numgoals!in Ltac}} +\subsubsection[Counting the goals]{Counting the goals\index{Ltac!numgoals@\texttt{numgoals}}\index{numgoals@\texttt{numgoals}!in Ltac}} The number of goals under focus can be recovered using the {\tt numgoals} function. Combined with the {\tt guard} command below, it @@ -979,7 +982,7 @@ split;[|split]. all:pr_numgoals. \end{coq_example} -\subsubsection[Testing boolean expressions]{Testing boolean expressions\index{Ltac!guard}\index{guard!in Ltac}} +\subsubsection[Testing boolean expressions]{Testing boolean expressions\index{Ltac!guard@\texttt{guard}}\index{guard@\texttt{guard}!in Ltac}} The {\tt guard} tactic tests a boolean expression, and fails if the expression evaluates to false. If the expression evaluates to true, it succeeds without affecting the proof. diff --git a/doc/refman/RefMan-mod.tex b/doc/refman/RefMan-mod.tex index 505c1110c..0e7b39c75 100644 --- a/doc/refman/RefMan-mod.tex +++ b/doc/refman/RefMan-mod.tex @@ -403,7 +403,7 @@ Check B.T. \end{ErrMsgs} \begin{Warnings} - \item Warning: Trying to mask the absolute name {\qualid} ! + \item Trying to mask the absolute name {\qualid} ! \end{Warnings} \subsection{\tt Print Module {\ident} diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex index 64fab055e..ce230a0f7 100644 --- a/doc/refman/RefMan-oth.tex +++ b/doc/refman/RefMan-oth.tex @@ -355,8 +355,10 @@ is a variant of {\tt Search statements whose conclusion has exactly the expected form, or whose statement finishes by the given series of hypothesis/conclusion. -\begin{coq_example} +\begin{coq_example*} Require Import Arith. +\end{coq_example*} +\begin{coq_example} SearchPattern (_ + _ = _ + _). SearchPattern (nat -> bool). SearchPattern (forall l : list _, _ l l). @@ -367,7 +369,6 @@ must occur in two places by using pattern variables `{\texttt ?{\ident}}''. \begin{coq_example} -Require Import Arith. SearchPattern (?X1 + _ = _ + ?X1). \end{coq_example} diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex index df707ce94..08213abe9 100644 --- a/doc/refman/RefMan-pro.tex +++ b/doc/refman/RefMan-pro.tex @@ -312,7 +312,7 @@ together with a suggestion about the right bullet or {\tt \}} to unfocus it or focus the next one. \begin{ErrMsgs} -\item \errindex{Error: This proof is focused, but cannot be unfocused +\item \errindex{This proof is focused, but cannot be unfocused this way} You are trying to use {\tt \}} but the current subproof has not been fully solved. \item see also error message about bullets below. @@ -363,25 +363,25 @@ Proof. \begin{ErrMsgs} -\item \errindex{Error: Wrong bullet {\abullet}1 : Current bullet +\item \errindex{Wrong bullet {\abullet}1 : Current bullet {\abullet}2 is not finished.} Before using bullet {\abullet}1 again, you should first finish proving the current focused goal. Note that {\abullet}1 and {\abullet}2 may be the same. -\item \errindex{Error: Wrong bullet {\abullet}1 : Bullet {\abullet}2 +\item \errindex{Wrong bullet {\abullet}1 : Bullet {\abullet}2 is mandatory here.} You must put {\abullet}2 to focus next goal. No other bullet is allowed here. -\item \errindex{Error: No such goal. Focus next goal with bullet +\item \errindex{No such goal. Focus next goal with bullet {\abullet}.} You tried to applied a tactic but no goal where under focus. Using {\abullet} is mandatory here. -\item \errindex{Error: No such goal. Try unfocusing with "{\tt \}}".} You +\item \errindex{No such goal. Try unfocusing with {"{\tt \}}"}.} You just finished a goal focused by {\tt \{}, you must unfocus it with "{\tt \}}". \end{ErrMsgs} diff --git a/doc/refman/RefMan-syn.tex b/doc/refman/RefMan-syn.tex index df4066169..11954ed0e 100644 --- a/doc/refman/RefMan-syn.tex +++ b/doc/refman/RefMan-syn.tex @@ -878,7 +878,7 @@ interpretation. See the next section. \SeeAlso The command to show the scopes bound to the arguments of a function is described in Section~\ref{About}. -\subsection[The {\tt type\_scope} interpretation scope]{The {\tt type\_scope} interpretation scope\index{type\_scope}} +\subsection[The {\tt type\_scope} interpretation scope]{The {\tt type\_scope} interpretation scope\index{type\_scope@\texttt{type\_scope}}} The scope {\tt type\_scope} has a special status. It is a primitive interpretation scope which is temporarily activated each time a diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index 35da17d54..dcc2bcc1f 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -65,8 +65,8 @@ make is so that tactics are, by default, applied to every goal simultaneously. Then, to apply a tactic {\tt tac} to the first goal only, you can write {\tt 1:tac}. -\subsection[\tt Test Default Goal Selector ``\selector''.] - {\tt Test Default Goal Selector ``\selector''. +\subsection[\tt Test Default Goal Selector.] + {\tt Test Default Goal Selector. \comindex{Test Default Goal Selector}} This command displays the current default selector. @@ -2029,7 +2029,7 @@ Import Nat. Functional Scheme minus_ind := Induction for minus Sort Prop. Check minus_ind. Lemma le_minus (n m:nat) : n - m <= n. -functional induction (minus n m); simpl; auto. +functional induction (minus n m) using minus_ind; simpl; auto. \end{coq_example} \begin{coq_example*} Qed. diff --git a/doc/refman/RefMan-tacex.tex b/doc/refman/RefMan-tacex.tex index 5703c73f0..668a68c9c 100644 --- a/doc/refman/RefMan-tacex.tex +++ b/doc/refman/RefMan-tacex.tex @@ -164,7 +164,7 @@ Notation " t --> t' " := (arrow t t') (at level 20, t' at next level). Inductive ctx : Type := | empty : ctx | snoc : ctx -> type -> ctx. -Notation " G , tau " := (snoc G tau) (at level 20, t at next level). +Notation " G , tau " := (snoc G tau) (at level 20, tau at next level). Fixpoint conc (G D : ctx) : ctx := match D with | empty => G diff --git a/doc/refman/RefMan-uti.tex b/doc/refman/RefMan-uti.tex index 07d711424..48e2df19d 100644 --- a/doc/refman/RefMan-uti.tex +++ b/doc/refman/RefMan-uti.tex @@ -3,7 +3,7 @@ The distribution provides utilities to simplify some tedious works beside proof development, tactics writing or documentation. -\section[Building a toplevel extended with user tactics]{Building a toplevel extended with user tactics\label{Coqmktop}\index{Coqmktop@{\tt coqmktop}}} +\section[Building a toplevel extended with user tactics]{Building a toplevel extended with user tactics\label{Coqmktop}\ttindex{coqmktop}} The native-code version of \Coq\ cannot dynamically load user tactics using {\ocaml} code. It is possible to build a toplevel of \Coq, @@ -52,7 +52,7 @@ arguments. Such a wrapper can be found in the \texttt{dev/} subdirectory of the sources. \section[Modules dependencies]{Modules dependencies\label{Dependencies}\index{Dependencies} - \index{Coqdep@{\tt coqdep}}} + \ttindex{coqdep}} In order to compute modules dependencies (so to use {\tt make}), \Coq\ comes with an appropriate tool, {\tt coqdep}. @@ -75,8 +75,8 @@ See the man page of {\tt coqdep} for more details and options. \section[Creating a {\tt Makefile} for \Coq\ modules]{Creating a {\tt Makefile} for \Coq\ modules\label{Makefile} -\index{Makefile@{\tt Makefile}} -\index{CoqMakefile@{\tt coq\_Makefile}}} +\ttindex{Makefile} +\ttindex{coq\_Makefile}} \paragraph{\_CoqProject} When a proof development becomes a larger project, split into several @@ -128,8 +128,8 @@ will recursively call this target in all the subdirectories. dependencies on already defined rules. For example the following skeleton appends something to the \texttt{install} rule: \begin{quotation} -\texttt{-extra-phony ``install'' ``install-my-stuff'' ``'' - -extra-phony ``install-my-stuff'' ``'' ``something''} +\texttt{-extra-phony "install" "install-my-stuff" "" + -extra-phony "install-my-stuff" "" "something"} \end{quotation} \end{itemize} @@ -146,12 +146,12 @@ to generate a \texttt{Makefile} the first time. \texttt{Makefile} will be automatically regenerated when \texttt{\_CoqProject} is updated afterward. \section[Documenting \Coq\ files with coqdoc]{Documenting \Coq\ files with coqdoc\label{coqdoc} -\index{Coqdoc@{\sf coqdoc}}} +\ttindex{coqdoc}} \input{./coqdoc} \section[Embedded \Coq\ phrases inside \LaTeX\ documents]{Embedded \Coq\ phrases inside \LaTeX\ documents\label{Latex} - \index{Coqtex@{\tt coq-tex}}\index{Latex@{\LaTeX}}} + \ttindex{coq-tex}\index{Latex@{\LaTeX}}} When writing a documentation about a proof development, one may want to insert \Coq\ phrases inside a \LaTeX\ document, possibly together with @@ -207,7 +207,7 @@ An inferior mode to run \Coq\ under Emacs, by Marco Maggesi, is also included in the distribution, in file \texttt{coq-inferior.el}. Instructions to use it are contained in this file. -\subsection[{\ProofGeneral}]{{\ProofGeneral}\index{\ProofGeneral}} +\subsection[{\ProofGeneral}]{{\ProofGeneral}\index{Proof General@{\ProofGeneral}}} {\ProofGeneral} is a generic interface for proof assistants based on Emacs. The main idea is that the \Coq\ commands you are @@ -221,7 +221,7 @@ files. system \Coq. It is freely available at \verb!proofgeneral.inf.ed.ac.uk!. -\section[Module specification]{Module specification\label{gallina}\index{Gallina@{\tt gallina}}} +\section[Module specification]{Module specification\label{gallina}\ttindex{gallina}} Given a \Coq\ vernacular file, the {\tt gallina} filter extracts its specification (inductive types declarations, definitions, type of diff --git a/doc/refman/coqdoc.tex b/doc/refman/coqdoc.tex index b66cbb436..b42480a56 100644 --- a/doc/refman/coqdoc.tex +++ b/doc/refman/coqdoc.tex @@ -252,8 +252,9 @@ suffix \verb!.tex!. \item[\texmacs\ output] ~\par To translate the input files to \texmacs\ format, to be used by - the \texmacs\ Coq interface - (see \url{http://www-sop.inria.fr/lemme/Philippe.Audebaud/tmcoq/}). + the \texmacs\ Coq interface. + %broken link: + %(see \url{http://www-sop.inria.fr/lemme/Philippe.Audebaud/tmcoq/}). \end{description} diff --git a/ide/coqOps.ml b/ide/coqOps.ml index 52e184564..689d4908f 100644 --- a/ide/coqOps.ml +++ b/ide/coqOps.ml @@ -215,8 +215,17 @@ object(self) document_length <- pred document_length; segment#set_length document_length; in + let on_click id = + let find _ _ s = Int.equal s.index id in + let sentence = Doc.find document find in + let mark = sentence.stop in + let iter = script#buffer#get_iter_at_mark mark in + script#buffer#place_cursor iter; + ignore (script#scroll_to_iter ~use_align:true ~yalign:0. iter) + in let _ = (Doc.connect document)#pushed on_push in let _ = (Doc.connect document)#popped on_pop in + let _ = segment#connect#clicked on_click in () method private tooltip_callback ~x ~y ~kbd tooltip = diff --git a/ide/wg_Segment.ml b/ide/wg_Segment.ml index 8520727a7..25a031d6e 100644 --- a/ide/wg_Segment.ml +++ b/ide/wg_Segment.ml @@ -70,9 +70,25 @@ let color_eq (c1 : GDraw.color) (c2 : GDraw.color) = match c1, c2 with | `WHITE, `WHITE -> true | _ -> false +class type segment_signals = +object + inherit GObj.misc_signals + inherit GUtil.add_ml_signals + method clicked : callback:(int -> unit) -> GtkSignal.id +end + +class segment_signals_impl obj (clicked : 'a GUtil.signal) : segment_signals = +object + val after = false + inherit GObj.misc_signals obj + inherit GUtil.add_ml_signals obj [clicked#disconnect] + method clicked = clicked#connect ~after +end + class segment () = let box = GBin.frame () in -let draw = GMisc.image ~packing:box#add () in +let eventbox = GBin.event_box ~packing:box#add () in +let draw = GMisc.image ~packing:eventbox#add () in object (self) inherit GObj.widget box#as_widget @@ -82,6 +98,7 @@ object (self) val mutable data = Segment.empty val mutable default : color = `WHITE val mutable pixmap : GDraw.pixmap = GDraw.pixmap ~width:1 ~height:1 () + val clicked = new GUtil.signal () initializer box#misc#set_size_request ~height (); @@ -96,6 +113,15 @@ object (self) end in let _ = box#misc#connect#size_allocate cb in + let clicked_cb ev = + let x = GdkEvent.Button.x ev in + let (width, _) = pixmap#size in + let len = Segment.length data in + let idx = f2i ((x *. i2f len) /. i2f width) in + let () = clicked#call idx in + true + in + let _ = eventbox#event#connect#button_press clicked_cb in (** Initial pixmap *) draw#set_pixmap pixmap @@ -140,4 +166,7 @@ object (self) Segment.fold color_eq fold data (); draw#set_mask None; + method connect = + new segment_signals_impl box#as_widget clicked + end diff --git a/ide/wg_Segment.mli b/ide/wg_Segment.mli index ecb451475..0263856ae 100644 --- a/ide/wg_Segment.mli +++ b/ide/wg_Segment.mli @@ -8,10 +8,18 @@ type color = GDraw.color +class type segment_signals = +object + inherit GObj.misc_signals + inherit GUtil.add_ml_signals + method clicked : callback:(int -> unit) -> GtkSignal.id +end + class segment : unit -> object inherit GObj.widget val obj : Gtk.widget Gtk.obj + method connect : segment_signals method length : int method set_length : int -> unit method default_color : color diff --git a/kernel/univ.ml b/kernel/univ.ml index 08e9fee05..492762df3 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -2064,7 +2064,7 @@ let explain_universe_inconsistency prl (o,u,v,p) = (spc() ++ str "= " ++ pr_uni u)) in str "Cannot enforce" ++ spc() ++ pr_uni u ++ spc() ++ - pr_rel o ++ spc() ++ pr_uni v ++ reason ++ str")" + pr_rel o ++ spc() ++ pr_uni v ++ reason let compare_levels = Level.compare let eq_levels = Level.equal diff --git a/tools/coqc.ml b/tools/coqc.ml index f636ffd87..5c7be41be 100644 --- a/tools/coqc.ml +++ b/tools/coqc.ml @@ -111,7 +111,7 @@ let parse_args () = |"-dont-load-proofs"|"-load-proofs"|"-force-load-proofs" |"-impredicative-set"|"-vm"|"-no-native-compiler" |"-verbose-compat-notations"|"-no-compat-notations" - |"-indices-matter"|"-quick"|"-color" + |"-indices-matter"|"-quick"|"-color"|"-type-in-type" |"-async-proofs-always-delegate"|"-async-proofs-never-reopen-branch" as o) :: rem -> parse (cfiles,o::args) rem diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index bb2073001..c6e40725b 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -1124,6 +1124,7 @@ let vernac_declare_arguments locality r l nargs flags = vernac_declare_implicits locality r implicits; if nargs >= 0 && nargs < List.fold_left max 0 rargs then error "The \"/\" option must be placed after the last \"!\"."; + let no_flags = List.is_empty flags in let rec narrow = function | #Reductionops.ReductionBehaviour.flag as x :: tl -> x :: narrow tl | [] -> [] | _ :: tl -> narrow tl in @@ -1141,7 +1142,7 @@ let vernac_declare_arguments locality r l nargs flags = some_implicits_specified || some_scopes_specified || some_simpl_flags_specified) && - List.length flags = 0 then + no_flags then msg_warning (strbrk "This command is just asserting the number and names of arguments of " ++ pr_global sr ++ strbrk". If this is what you want add ': assert' to silence the warning. If you want to clear implicit arguments add ': clear implicits'. If you want to clear notation scopes add ': clear scopes'") |