aboutsummaryrefslogtreecommitdiff
path: root/doc
diff options
context:
space:
mode:
Diffstat (limited to 'doc')
-rw-r--r--doc/Makefile.rt43
-rw-r--r--doc/RecTutorial/RecTutorial.v111
-rw-r--r--doc/common/title.tex2
-rw-r--r--doc/refman/RefMan-ext.tex78
-rw-r--r--doc/refman/RefMan-pre.tex114
-rw-r--r--doc/refman/RefMan-ssr.tex12
-rw-r--r--doc/refman/RefMan-syn.tex14
-rw-r--r--doc/refman/RefMan-tac.tex18
-rw-r--r--doc/refman/RefMan-uti.tex80
-rw-r--r--doc/refman/Setoid.tex2
-rw-r--r--doc/rt/RefMan-cover.tex45
-rw-r--r--doc/rt/Tutorial-cover.tex47
-rw-r--r--doc/tools/Translator.tex2
13 files changed, 326 insertions, 242 deletions
diff --git a/doc/Makefile.rt b/doc/Makefile.rt
deleted file mode 100644
index 6c32813462..0000000000
--- a/doc/Makefile.rt
+++ /dev/null
@@ -1,43 +0,0 @@
-# Makefile for building Coq Technical Reports
-
-# if coqc,coqtop,coq-tex are not in your PATH, you need the environment
-# variable COQBIN to be correctly set
-# (COQTOP is autodetected)
-# (some files are preprocessed using Coq and some part of the documentation
-# is automatically built from the theories sources)
-
-# To compile documentation, you need the following tools:
-# Dvi: latex (latex2e), bibtex, makeindex, dviselect (package RPM dviutils)
-# Ps: dvips, psutils (ftp://ftp.dcs.ed.ac.uk/pub/ajcd/psutils.tar.gz)
-# Pdf: pdflatex
-# Html:
-# - hevea: http://para.inria.fr/~maranget/hevea/
-# - htmlSplit: http://coq.inria.fr/~delahaye
-# Rapports INRIA: dviselect, rrkit (par Michel Mauny)
-
-include ./Makefile
-
-###################
-# RT
-###################
-# Fabrication d'un RT INRIA (utilise rrkit de Michel Mauny)
-rt/Reference-Manual-RT.dvi: refman/Reference-Manual.dvi rt/RefMan-cover.tex
- dviselect -i refman/Reference-Manual.dvi -o rt/RefMan-body.dvi 3:
- (cd rt; $(LATEX) RefMan-cover.tex)
- set a=`tail -1 refman/Reference-Manual.log`;\
- set a=expr \("$$a" : '.*(\(.*\) pages.*'\) % 2;\
- (cd rt; if $(TEST) "$$a = 0";\
- then rrkit RefMan-cover.dvi RefMan-body.dvi Reference-Manual-RT.dvi;\
- else rrkit -odd RefMan-cover.dvi RefMan-body.dvi Reference-Manual-RT.dvi;\
- fi)
-
-# Fabrication d'un RT INRIA (utilise rrkit de Michel Mauny)
-rt/Tutorial-RT.dvi : tutorial/Tutorial.v.dvi rt/Tutorial-cover.tex
- dviselect -i rt/Tutorial.v.dvi -o rt/Tutorial-body.dvi 3:
- (cd rt; $(LATEX) Tutorial-cover.tex)
- set a=`tail -1 tutorial/Tutorial.v.log`;\
- set a=expr \("$$a" : '.*(\(.*\) pages.*'\) % 2;\
- (cd rt; if $(TEST) "$$a = 0";\
- then rrkit Tutorial-cover.dvi Tutorial-body.dvi Tutorial-RT.dvi;\
- else rrkit -odd Tutorial-cover.dvi Tutorial-body.dvi Tutorial-RT.dvi;\
- fi)
diff --git a/doc/RecTutorial/RecTutorial.v b/doc/RecTutorial/RecTutorial.v
index 8cfeebc28b..4b0ab31254 100644
--- a/doc/RecTutorial/RecTutorial.v
+++ b/doc/RecTutorial/RecTutorial.v
@@ -1,3 +1,5 @@
+Unset Automatic Introduction.
+
Check (forall A:Type, (exists x:A, forall (y:A), x <> y) -> 2 = 3).
@@ -69,13 +71,13 @@ Check (Prop::Set::nil).
Require Import Bvector.
-Print vector.
+Print Vector.t.
-Check (Vnil nat).
+Check (Vector.nil nat).
-Check (fun (A:Type)(a:A)=> Vcons _ a _ (Vnil _)).
+Check (fun (A:Type)(a:A)=> Vector.cons _ a _ (Vector.nil _)).
-Check (Vcons _ 5 _ (Vcons _ 3 _ (Vnil _))).
+Check (Vector.cons _ 5 _ (Vector.cons _ 3 _ (Vector.nil _))).
Lemma eq_3_3 : 2 + 1 = 3.
Proof.
@@ -146,6 +148,7 @@ Proof.
intros; absurd (p < p); eauto with arith.
Qed.
+Require Extraction.
Extraction max.
@@ -300,8 +303,8 @@ Section Le_case_analysis.
(HS : forall m, n <= m -> Q (S m)).
Check (
match H in (_ <= q) return (Q q) with
- | le_n => H0
- | le_S m Hm => HS m Hm
+ | le_n _ => H0
+ | le_S _ m Hm => HS m Hm
end
).
@@ -317,16 +320,16 @@ Proof.
Qed.
Definition Vtail_total
- (A : Type) (n : nat) (v : vector A n) : vector A (pred n):=
-match v in (vector _ n0) return (vector A (pred n0)) with
-| Vnil => Vnil A
-| Vcons _ n0 v0 => v0
+ (A : Type) (n : nat) (v : Vector.t A n) : Vector.t A (pred n):=
+match v in (Vector.t _ n0) return (Vector.t A (pred n0)) with
+| Vector.nil _ => Vector.nil A
+| Vector.cons _ _ n0 v0 => v0
end.
-Definition Vtail' (A:Type)(n:nat)(v:vector A n) : vector A (pred n).
+Definition Vtail' (A:Type)(n:nat)(v:Vector.t A n) : Vector.t A (pred n).
intros A n v; case v.
simpl.
- exact (Vnil A).
+ exact (Vector.nil A).
simpl.
auto.
Defined.
@@ -498,10 +501,8 @@ Inductive typ : Type :=
Definition typ_inject: typ.
split.
-exact typ.
+Fail exact typ.
(*
-Defined.
-
Error: Universe Inconsistency.
*)
Abort.
@@ -920,7 +921,6 @@ Defined.
Print minus_decrease.
-
Definition div_aux (x y:nat)(H: Acc lt x):nat.
fix 3.
intros.
@@ -969,40 +969,40 @@ let rec div_aux x y =
| Right -> div_aux (minus x y) y)
*)
-Lemma vector0_is_vnil : forall (A:Type)(v:vector A 0), v = Vnil A.
+Lemma vector0_is_vnil : forall (A:Type)(v:Vector.t A 0), v = Vector.nil A.
Proof.
intros A v;inversion v.
Abort.
(*
- Lemma vector0_is_vnil_aux : forall (A:Type)(n:nat)(v:vector A n),
- n= 0 -> v = Vnil A.
+ Lemma vector0_is_vnil_aux : forall (A:Type)(n:nat)(v:Vector.t A n),
+ n= 0 -> v = Vector.nil A.
Toplevel input, characters 40281-40287
-> Lemma vector0_is_vnil_aux : forall (A:Set)(n:nat)(v:vector A n), n= 0 -> v = Vnil A.
+> Lemma vector0_is_vnil_aux : forall (A:Set)(n:nat)(v:Vector.t A n), n= 0 -> v = Vector.nil A.
> ^^^^^^
Error: In environment
A : Set
n : nat
-v : vector A n
+v : Vector.t A n
e : n = 0
-The term "Vnil A" has type "vector A 0" while it is expected to have type
- "vector A n"
+The term "Vector.nil A" has type "Vector.t A 0" while it is expected to have type
+ "Vector.t A n"
*)
Require Import JMeq.
(* On devrait changer Set en Type ? *)
-Lemma vector0_is_vnil_aux : forall (A:Type)(n:nat)(v:vector A n),
- n= 0 -> JMeq v (Vnil A).
+Lemma vector0_is_vnil_aux : forall (A:Type)(n:nat)(v:Vector.t A n),
+ n= 0 -> JMeq v (Vector.nil A).
Proof.
destruct v.
auto.
intro; discriminate.
Qed.
-Lemma vector0_is_vnil : forall (A:Type)(v:vector A 0), v = Vnil A.
+Lemma vector0_is_vnil : forall (A:Type)(v:Vector.t A 0), v = Vector.nil A.
Proof.
intros a v;apply JMeq_eq.
apply vector0_is_vnil_aux.
@@ -1010,56 +1010,56 @@ Proof.
Qed.
-Implicit Arguments Vcons [A n].
-Implicit Arguments Vnil [A].
-Implicit Arguments Vhead [A n].
-Implicit Arguments Vtail [A n].
+Implicit Arguments Vector.cons [A n].
+Implicit Arguments Vector.nil [A].
+Implicit Arguments Vector.hd [A n].
+Implicit Arguments Vector.tl [A n].
-Definition Vid : forall (A : Type)(n:nat), vector A n -> vector A n.
+Definition Vid : forall (A : Type)(n:nat), Vector.t A n -> Vector.t A n.
Proof.
destruct n; intro v.
- exact Vnil.
- exact (Vcons (Vhead v) (Vtail v)).
+ exact Vector.nil.
+ exact (Vector.cons (Vector.hd v) (Vector.tl v)).
Defined.
-Eval simpl in (fun (A:Type)(v:vector A 0) => (Vid _ _ v)).
+Eval simpl in (fun (A:Type)(v:Vector.t A 0) => (Vid _ _ v)).
-Eval simpl in (fun (A:Type)(v:vector A 0) => v).
+Eval simpl in (fun (A:Type)(v:Vector.t A 0) => v).
-Lemma Vid_eq : forall (n:nat) (A:Type)(v:vector A n), v=(Vid _ n v).
+Lemma Vid_eq : forall (n:nat) (A:Type)(v:Vector.t A n), v=(Vid _ n v).
Proof.
destruct v.
reflexivity.
reflexivity.
Defined.
-Theorem zero_nil : forall A (v:vector A 0), v = Vnil.
+Theorem zero_nil : forall A (v:Vector.t A 0), v = Vector.nil.
Proof.
intros.
- change (Vnil (A:=A)) with (Vid _ 0 v).
+ change (Vector.nil (A:=A)) with (Vid _ 0 v).
apply Vid_eq.
Defined.
Theorem decomp :
- forall (A : Type) (n : nat) (v : vector A (S n)),
- v = Vcons (Vhead v) (Vtail v).
+ forall (A : Type) (n : nat) (v : Vector.t A (S n)),
+ v = Vector.cons (Vector.hd v) (Vector.tl v).
Proof.
intros.
- change (Vcons (Vhead v) (Vtail v)) with (Vid _ (S n) v).
+ change (Vector.cons (Vector.hd v) (Vector.tl v)) with (Vid _ (S n) v).
apply Vid_eq.
Defined.
Definition vector_double_rect :
- forall (A:Type) (P: forall (n:nat),(vector A n)->(vector A n) -> Type),
- P 0 Vnil Vnil ->
- (forall n (v1 v2 : vector A n) a b, P n v1 v2 ->
- P (S n) (Vcons a v1) (Vcons b v2)) ->
- forall n (v1 v2 : vector A n), P n v1 v2.
+ forall (A:Type) (P: forall (n:nat),(Vector.t A n)->(Vector.t A n) -> Type),
+ P 0 Vector.nil Vector.nil ->
+ (forall n (v1 v2 : Vector.t A n) a b, P n v1 v2 ->
+ P (S n) (Vector.cons a v1) (Vector.cons b v2)) ->
+ forall n (v1 v2 : Vector.t A n), P n v1 v2.
induction n.
intros; rewrite (zero_nil _ v1); rewrite (zero_nil _ v2).
auto.
@@ -1069,24 +1069,23 @@ Defined.
Require Import Bool.
-Definition bitwise_or n v1 v2 : vector bool n :=
- vector_double_rect bool (fun n v1 v2 => vector bool n)
- Vnil
- (fun n v1 v2 a b r => Vcons (orb a b) r) n v1 v2.
-
+Definition bitwise_or n v1 v2 : Vector.t bool n :=
+ vector_double_rect bool (fun n v1 v2 => Vector.t bool n)
+ Vector.nil
+ (fun n v1 v2 a b r => Vector.cons (orb a b) r) n v1 v2.
-Fixpoint vector_nth (A:Type)(n:nat)(p:nat)(v:vector A p){struct v}
+Fixpoint vector_nth (A:Type)(n:nat)(p:nat)(v:Vector.t A p){struct v}
: option A :=
match n,v with
- _ , Vnil => None
- | 0 , Vcons b _ _ => Some b
- | S n', Vcons _ p' v' => vector_nth A n' p' v'
+ _ , Vector.nil => None
+ | 0 , Vector.cons b _ => Some b
+ | S n', @Vector.cons _ _ p' v' => vector_nth A n' p' v'
end.
Implicit Arguments vector_nth [A p].
-Lemma nth_bitwise : forall (n:nat) (v1 v2: vector bool n) i a b,
+Lemma nth_bitwise : forall (n:nat) (v1 v2: Vector.t bool n) i a b,
vector_nth i v1 = Some a ->
vector_nth i v2 = Some b ->
vector_nth i (bitwise_or _ v1 v2) = Some (orb a b).
diff --git a/doc/common/title.tex b/doc/common/title.tex
index 0e072b6b65..76e50f65d2 100644
--- a/doc/common/title.tex
+++ b/doc/common/title.tex
@@ -45,7 +45,7 @@ V\coqversion, \today
%END LATEX
\copyright INRIA 1999-2004 ({\Coq} versions 7.x)
-\copyright INRIA 2004-2016 ({\Coq} versions 8.x)
+\copyright INRIA 2004-2017 ({\Coq} versions 8.x)
#3
\end{flushleft}
diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex
index 713f344cbe..7af4e9313a 100644
--- a/doc/refman/RefMan-ext.tex
+++ b/doc/refman/RefMan-ext.tex
@@ -279,15 +279,78 @@ of the chapter devoted to coercions.
\label{prim-proj}
The option {\tt Set Primitive Projections} turns on the use of primitive
-projections when defining subsequent records. Primitive projections
+projections when defining subsequent records (even through the {\tt
+ Inductive} and {\tt CoInductive} commands). Primitive projections
extended the Calculus of Inductive Constructions with a new binary term
constructor {\tt r.(p)} representing a primitive projection p applied to
a record object {\tt r} (i.e., primitive projections are always
applied). Even if the record type has parameters, these do not appear at
applications of the projection, considerably reducing the sizes of terms
when manipulating parameterized records and typechecking time. On the
-user level, primitive projections are a transparent replacement
-for the usual defined ones.
+user level, primitive projections can be used as a replacement for the
+usual defined ones, although there are a few notable differences.
+
+The internally omitted parameters can be reconstructed at printing time
+even though they are absent in the actual AST manipulated by the kernel. This
+can be obtained by setting the {\tt Printing Primitive Projection Parameters}
+flag. Another compatibility printing can be activated thanks to the
+{\tt Printing Primitive Projection Compatibility} option which governs the
+printing of pattern-matching over primitive records.
+
+\subsubsection{Primitive Record Types}
+When the {\tt Set Primitive Projections} option is on, definitions of
+record types change meaning. When a type is declared with primitive
+projections, its {\tt match} construct is disabled (see
+\ref{primproj:compat} though). To eliminate the (co-)inductive type, one
+must use its defined primitive projections.
+
+There are currently two ways to introduce primitive records types:
+\begin{itemize}
+\item Through the {\tt Record} command, in which case the type has to be
+ non-recursive. The defined type enjoys eta-conversion definitionally,
+ that is the generalized form of surjective pairing for records:
+ {\tt $r$ = Build\_R ($r$.($p_1$) .. $r$.($p_n$))}. Eta-conversion allows to define
+ dependent elimination for these types as well.
+\item Through the {\tt Inductive} and {\tt CoInductive} commands, when
+ the body of the definition is a record declaration of the form {\tt
+ Build\_R \{ $p_1$ : $t_1$; .. ; $p_n$ : $t_n$ \}}. In this case the types can be
+ recursive and eta-conversion is disallowed. These kind of record types
+ differ from their traditional versions in the sense that dependent
+ elimination is not available for them and only non-dependent case analysis
+ can be defined.
+\end{itemize}
+
+\subsubsection{Reduction}
+
+The basic reduction rule of a primitive projection is {\tt $p_i$
+ (Build\_R $t_1$ .. $t_n$) $\rightarrow_{\iota}$ $t_i$}. However, to take the $\delta$ flag into
+account, projections can be in two states: folded or unfolded. An
+unfolded primitive projection application obeys the rule above, while
+the folded version delta-reduces to the unfolded version. This allows to
+precisely mimic the usual unfolding rules of constants. Projections
+obey the usual {\tt simpl} flags of the {\tt Arguments} command in particular.
+
+There is currently no way to input unfolded primitive projections at the
+user-level, and one must use the {\tt Printing Primitive Projection
+ Compatibility} to display unfolded primitive projections as matches
+and distinguish them from folded ones.
+
+\subsubsection{Compatibility Projections and {\tt match}}
+\label{primproj:compat}
+To ease compatibility with ordinary record types, each primitive
+projection is also defined as a ordinary constant taking parameters and
+an object of the record type as arguments, and whose body is an
+application of the unfolded primitive projection of the same name. These
+constants are used when elaborating partial applications of the
+projection. One can distinguish them from applications of the primitive
+projection if the {\tt Printing Primitive Projection Parameters} option
+is off: for a primitive projection application, parameters are printed
+as underscores while for the compatibility projections they are printed
+as usual.
+
+Additionally, user-written {\tt match} constructs on primitive records
+are desugared into substitution of the projections, they cannot be
+printed back as {\tt match} constructs.
% - r.(p) and (p r) elaborate to native projection application, and
% the parameters cannot be mentioned. The following arguments are
@@ -305,13 +368,6 @@ for the usual defined ones.
% - [pattern x at n], [rewrite x at n] and in general abstraction and selection
% of occurrences may fail due to the disappearance of parameters.
-The internally omitted parameters can be reconstructed at printing time
-even though they are absent in the actual AST manipulated by the kernel. This
-can be obtained by setting the {\tt Printing Primitive Projection Parameters}
-flag. Another compatibility printing can be activated thanks to the
-{\tt Printing Primitive Projection Compatibility} option which governs the
-printing of pattern-matching over primitive records.
-
\section{Variants and extensions of {\mbox{\tt match}}
\label{Extensions-of-match}
\index{match@{\tt match\ldots with\ldots end}}}
@@ -1664,7 +1720,7 @@ to be given as if none arguments were implicit. By symmetry, this also
affects printing. To restore parsing and normal printing of implicit
arguments, use:
\begin{quote}
-{\tt Set Parsing Explicit.}
+{\tt Unset Parsing Explicit.}
\end{quote}
\subsection{Canonical structures
diff --git a/doc/refman/RefMan-pre.tex b/doc/refman/RefMan-pre.tex
index 0441f952df..0c2a18eb2e 100644
--- a/doc/refman/RefMan-pre.tex
+++ b/doc/refman/RefMan-pre.tex
@@ -1220,6 +1220,120 @@ Paris, November 2016,\\
Matthieu Sozeau and the {\Coq} development team\\
\end{flushright}
+\section*{Credits: version 8.7}
+
+{\Coq} version 8.7 contains the result of refinements, stabilization of
+features and cleanups of the internals of the system along with a few
+new features. The main user visible changes are:
+\begin{itemize}
+\item New tactics: variants of tactics supporting existential variables
+ \texttt{eassert}, \texttt{eenough}, etc... by Hugo Herbelin. Tactics
+ \texttt{extensionality in H} and \texttt{inversion\_sigma} by Jason
+ Gross, \texttt{specialize with ...} accepting partial bindings by
+ Pierre Courtieu.
+\item Cumulative Polymorphic Inductive Types, allowing cumulativity of
+ universes to go through applied inductive types, by Amin Timany and
+ Matthieu Sozeau.
+\item Integration of the \texttt{SSReflect} plugin and its documentation in the
+ reference manual, by Enrico Tassi, Assia Mahboubi and Maxime Dénès.
+\item The \texttt{coq\_makefile} tool was completely redesigned to improve its
+ maintainability and the extensibility of generated Makefiles, and to
+ make \texttt{\_CoqProject} files more palatable to IDEs by Enrico Tassi.
+\end{itemize}
+
+{\Coq} 8.7 involved a large amount of work on cleaning and speeding up
+the code base, notably the work of Pierre-Marie Pédrot on making the
+tactic-level system insensitive to existential variable expansion,
+providing a safer API to plugin writers and making the code more
+robust. The \texttt{dev/doc/changes.txt} file documents the numerous
+changes to the implementation and improvements of interfaces. An effort
+to provide an official, streamlined API to plugin writers is in
+progress, thanks to the work of Matej Košík.
+
+Version 8.7 also comes with a bunch of smaller-scale changes and improvements
+regarding the different components of the system. We shall only list a
+few of them.
+
+The efficiency of the whole system has been significantly improved
+thanks to contributions from Pierre-Marie Pédrot, Maxime Dénès and
+Matthieu Sozeau and performance issue tracking by Jason Gross and Paul
+Steckler.
+
+Thomas Sibut-Pinote and Hugo Herbelin added support for side effects
+hooks in \texttt{cbv}, \texttt{cbn} and \texttt{simpl}. The side
+effects are provided via a plugin available at
+\url{https://github.com/herbelin/reduction-effects/}.
+
+The \texttt{BigN}, \texttt{BigZ}, \texttt{BigQ} libraries are no longer
+part of the {\Coq} standard library, they are now provided by a separate
+repository \url{https://github.com/coq/bignums}, maintained by Pierre
+Letouzey.
+
+In the \texttt{Reals} library, \texttt{IZR} has been changed to produce
+a compact representation of integers and real constants are now
+represented using \texttt{IZR} (work by Guillaume Melquiond).
+
+Standard library additions and improvements by Jason Gross, Pierre
+Letouzey and others, documented in the CHANGES file.
+
+The mathematical proof language/declarative mode plugin was removed from
+the archive.
+
+The OPAM repository for {\Coq} packages has been maintained by Guillaume
+Melquiond, Matthieu Sozeau, Enrico Tassi with contributions from many
+users. A list of packages is available at
+\url{https://coq.inria.fr/opam/www/}.
+
+Packaging tools and software development kits were prepared by Michael
+Soegtrop with the help of Maxime Dénès and Enrico Tassi for Windows, and
+Maxime Dénès for MacOS X. Packages are regularly built on the
+Travis continuous integration server.
+
+The contributors for this version are Abhishek Anand, C.J. Bell, Yves
+Bertot, Frédéric Besson, Tej Chajed, Pierre Courtieu, Maxime Dénès,
+Julien Forest, Gaëtan Gilbert, Jason Gross, Hugo Herbelin, Emilio Jesús
+Gallego Arias, Ralf Jung, Matej Košík, Xavier Leroy, Pierre Letouzey,
+Assia Mahboubi, Cyprien Mangin, Erik Martin-Dorel, Olivier Marty,
+Guillaume Melquiond, Sam Pablo Kuper, Benjamin Pierce, Pierre-Marie
+Pédrot, Lars Rasmusson, Lionel Rieg, Valentin Robert, Yann Régis-Gianas,
+Thomas Sibut-Pinote, Michael Soegtrop, Matthieu Sozeau, Arnaud Spiwack,
+Paul Steckler, George Stelle, Pierre-Yves Strub, Enrico Tassi, Hendrik
+Tews, Amin Timany, Laurent Théry, Vadim Zaliva and Théo Zimmermann.
+
+The development process was coordinated by Matthieu Sozeau with the help
+of Maxime Dénès, who was also in charge of the release process. Théo
+Zimmermann is the maintainer of this release.
+
+Many power users helped to improve the design of the new features via
+the bug tracker, the pull request system, the {\Coq} development mailing
+list or the coq-club mailing list. Special thanks to the users who
+contributed patches and intensive brain-storming and code reviews,
+starting with Jason Gross, Ralf Jung, Robbert Krebbers, Xavier Leroy,
+Clément Pit--Claudel and Gabriel Scherer. It would however be impossible
+to mention exhaustively the names of everybody who to some extent
+influenced the development.
+
+Version 8.7 is the second release of {\Coq} developed on a time-based
+development cycle. Its development spanned 9 months from the release of
+{\Coq} 8.6 and was based on a public road-map. It attracted many external
+contributions. Code reviews and continuous integration testing were
+systematically used before integration of new features, with an
+important focus given to compatibility and performance issues, resulting
+in a hopefully more robust release than {\Coq} 8.6 while maintaining
+compatibility.
+
+Coq Enhancement Proposals (CEPs for short) and open pull-requests
+discussions were used to discuss publicly the new features.
+
+The {\Coq} consortium, an organization directed towards users and
+supporters of the system, is now upcoming and will rely on Inria's
+newly created Foundation.
+
+\begin{flushright}
+Paris, August 2017,\\
+Matthieu Sozeau and the {\Coq} development team\\
+\end{flushright}
+
%new Makefile
diff --git a/doc/refman/RefMan-ssr.tex b/doc/refman/RefMan-ssr.tex
index 61f7421c44..db794e5a63 100644
--- a/doc/refman/RefMan-ssr.tex
+++ b/doc/refman/RefMan-ssr.tex
@@ -42,7 +42,7 @@ Proofs written in \ssr{} typically look quite different from the
ones written using only tactics as per Chapter~\ref{Tactics}.
We try to summarise here the most ``visible'' ones in order to
help the reader already accustomed to the tactics described in
-Chapter~\ref{Tactics}to read this chapter.
+Chapter~\ref{Tactics} to read this chapter.
The first difference between the tactics described in this
chapter and the tactics described in Chapter~\ref{Tactics} is the way
@@ -79,19 +79,19 @@ expansion and partial evaluation participate all to a same concept of
rewriting a goal in a larger sense. As such, all these functionalities are
provided by the \ssrC{rewrite} tactic.
-\ssrC{} includes a little language of patterns to select subterms in tactics
+\ssr{} includes a little language of patterns to select subterms in tactics
or tacticals where it matters. Its most notable application
is in the \ssrC{rewrite} tactic, where patterns are used to specify
where the rewriting step has to take place.
-Finally, \ssr{} supports the so-called reflection steps, typically
+Finally, \ssr{} supports so-called reflection steps, typically
allowing to switch back and forth between the computational view and
logical view of a concept.
To conclude it is worth mentioning that \ssr{} tactics
can be mixed with non \ssr{} tactics in the same proof,
-or in the same LTac expression. The few exceptions
-to this statement are described in section~\label{sec:compat}.
+or in the same Ltac expression. The few exceptions
+to this statement are described in section~\ref{sec:compat}.
\iffalse
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -130,7 +130,7 @@ ProofGeneral provided in the distribution:
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection*{Acknowledgments}
-The authors would like to thank Fr\'ed\'eric Blanqui, Fran\,cois Pottier
+The authors would like to thank Frédéric Blanqui, François Pottier
and Laurence Rideau for their comments and suggestions.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
diff --git a/doc/refman/RefMan-syn.tex b/doc/refman/RefMan-syn.tex
index 084317776b..d8a353300f 100644
--- a/doc/refman/RefMan-syn.tex
+++ b/doc/refman/RefMan-syn.tex
@@ -980,7 +980,7 @@ delimited by key {\tt nat}, and bound to the type {\tt nat} (see \ref{bindscope}
This scope includes the standard arithmetical operators and relations on
type {\tt N} (binary natural numbers). It is delimited by key {\tt N}
-and comes with an interpretation for numerals as closed term of type {\tt Z}.
+and comes with an interpretation for numerals as closed term of type {\tt N}.
\subsubsection{\tt Z\_scope}
@@ -1014,16 +1014,8 @@ fractions of an integer and a strictly positive integer.
This scope includes the standard arithmetical operators and relations on
type {\tt R} (axiomatic real numbers). It is delimited by key {\tt R}
-and comes with an interpretation for numerals as term of type {\tt
-R}. The interpretation is based on the binary decomposition. The
-numeral 2 is represented by $1+1$. The interpretation $\phi(n)$ of an
-odd positive numerals greater $n$ than 3 is {\tt 1+(1+1)*$\phi((n-1)/2)$}.
-The interpretation $\phi(n)$ of an even positive numerals greater $n$
-than 4 is {\tt (1+1)*$\phi(n/2)$}. Negative numerals are represented as the
-opposite of the interpretation of their absolute value. E.g. the
-syntactic object {\tt -11} is interpreted as {\tt
--(1+(1+1)*((1+1)*(1+(1+1))))} where the unit $1$ and all the operations are
-those of {\tt R}.
+and comes with an interpretation for numerals using the {\tt IZR}
+morphism from binary integer numbers to {\tt R}.
\subsubsection{\tt bool\_scope}
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index b3b0df5c8a..8fbcfdf308 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -3269,7 +3269,7 @@ The call-by-value strategy is the one used in ML languages: the
arguments of a function call are systematically weakly evaluated
first. Despite the lazy strategy always performs fewer reductions than
the call-by-value strategy, the latter is generally more efficient for
-evaluating purely computational expressions (i.e. with few dead code).
+evaluating purely computational expressions (i.e. with little dead code).
\begin{Variants}
\item {\tt compute} \tacindex{compute}\\
@@ -3309,7 +3309,7 @@ evaluating purely computational expressions (i.e. with few dead code).
fine-tuned. It is specially interesting for full evaluation of algebraic
objects. This includes the case of reflection-based tactics.
-\item {\tt native\_compute} \tacindex{native\_compute}
+\item {\tt native\_compute} \tacindex{native\_compute} \optindex{NativeCompute Profiling}
This tactic evaluates the goal by compilation to \ocaml{} as described in
\cite{FullReduction}. If \Coq{} is running in native code, it can be typically
@@ -3317,6 +3317,20 @@ evaluating purely computational expressions (i.e. with few dead code).
compilation cost is higher, so it is worth using only for intensive
computations.
+ On Linux, if you have the {\tt perf} profiler installed, you can profile {\tt native\_compute} evaluations.
+ The command
+ \begin{quote}
+ {\tt Set Native Compute Profiling}
+ \end{quote}
+ enables profiling. Use the command
+ \begin{quote}
+ {\tt Set NativeCompute Profile Filename \str}
+ \end{quote}
+ to specify the profile output; the default is {\tt native\_compute\_profile.data}. The actual filename used
+ will contain extra characters to avoid overwriting an existing file; that filename is reported to the user. That means
+ you can individually profile multiple uses of {\tt native\_compute} in a script. From the Linux command line, run {\tt perf report} on
+ the profile file to see the results. Consult the {\tt perf} documentation for more details.
+
\end{Variants}
% Obsolete? Anyway not very important message
diff --git a/doc/refman/RefMan-uti.tex b/doc/refman/RefMan-uti.tex
index 768d0df763..f6371f8e5c 100644
--- a/doc/refman/RefMan-uti.tex
+++ b/doc/refman/RefMan-uti.tex
@@ -51,6 +51,8 @@ arguments. In other cases, the debugger is simply called without additional
arguments. Such a wrapper can be found in the \texttt{dev/}
subdirectory of the sources.
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
\section[Building a \Coq\ project with {\tt coq\_makefile}]
{Building a \Coq\ project with {\tt coq\_makefile}
\label{Makefile}
@@ -95,7 +97,7 @@ Such command generates the following files:
\item[{\tt CoqMakefile.conf}] contains make variables assignments that reflect the contents of the {\tt \_CoqProject} file as well as the path relevant to \Coq{}.
\end{description}
-An optional file {\bf {\tt CoqMakefile.local}} can be provided by the user in order to extend {\tt CoqMakefile}. In particular one can declare custom actions to be performed before or after the build process. Similarly one can customize the install target or even provide new targets. Extension points are documented in the {\tt CoqMakefile} file.
+An optional file {\bf {\tt CoqMakefile.local}} can be provided by the user in order to extend {\tt CoqMakefile}. In particular one can declare custom actions to be performed before or after the build process. Similarly one can customize the install target or even provide new targets. Extension points are documented in paragraph \ref{coqmakefile:local}.
The extensions of the files listed in {\tt \_CoqProject} is
used in order to decide how to build them. In particular:
@@ -114,7 +116,52 @@ the plugin's ``name space'' ({\tt Qux\_plugin}).
This reduces the chances of begin unable to load two distinct plugins
because of a clash in their auxiliary module names.
-\paragraph{Timing targets and performance testing}
+\paragraph{CoqMakefile.local} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\label{coqmakefile:local}
+
+The optional file {\tt CoqMakefile.local} is included by the generated file
+{\tt CoqMakefile}. Such can contain two kinds of directives.
+
+\begin{description}
+ \item[Variable assignment] to the variables listed in the {\tt Parameters}
+ section of the generated makefile. Here we describe only few of them.
+ \begin{description}
+ \item[CAMLPKGS] can be used to specify third party findlib packages, and is
+ passed to the OCaml compiler on building or linking of modules.
+ Eg: {\tt -package yojson}.
+ \item[CAMLFLAGS] can be used to specify additional flags to the OCaml
+ compiler, like {\tt -bin-annot} or {\tt -w...}.
+ \item[COQC, COQDEP, COQDOC] can be set in order to use alternative
+ binaries (e.g. wrappers)
+ \end{description}
+\item[Rule extension]
+ The following makefile rules can be extended. For example
+\begin{verbatim}
+pre-all::
+ echo "This line is print before making the all target"
+install-extra::
+ cp ThisExtraFile /there/it/goes
+\end{verbatim}
+ \begin{description}
+ \item[pre-all::] run before the {\tt all} target. One can use this
+ to configure the project, or initialize sub modules or check
+ dependencies are met.
+ \item[post-all::] run after the {\tt all} target. One can use this
+ to run a test suite, or compile extracted code.
+ \item[install-extra::] run after {\tt install}. One can use this
+ to install extra files.
+ \item[install-doc::] One can use this to install extra doc.
+ \item[uninstall::]
+ \item[uninstall-doc::]
+ \item[clean::]
+ \item[cleanall::]
+ \item[archclean::]
+ \item[merlin-hook::] One can append lines to the generated {\tt .merlin}
+ file extending this target.
+ \end{description}
+\end{description}
+
+\paragraph{Timing targets and performance testing} %%%%%%%%%%%%%%%%%%%%%%%%%%%
The generated \texttt{Makefile} supports the generation of two kinds
of timing data: per-file build-times, and per-line times for an
individual file.
@@ -273,9 +320,10 @@ After | Code | Before || C
\texttt{Note}: This target requires \texttt{python} to build the table.
\end{itemize}
-\paragraph{Notes about including the generated Makefile}
+\paragraph{Reusing/extending the generated Makefile} %%%%%%%%%%%%%%%%%%%%%%%%%
-This practice is discouraged. The contents of this file, including variable names
+Including the generated makefile with an {\tt include} directive is discouraged.
+The contents of this file, including variable names
and status of rules shall change in the future. Users are advised to
include {\tt Makefile.conf} or call a target of the generated Makefile
as in {\tt make -f Makefile target} from another Makefile.
@@ -303,21 +351,23 @@ invoke-coqmakefile: CoqMakefile
.PHONY: invoke-coqmakefile $(KNOWNFILES)
####################################################################
-####################################################################
-####################################################################
-####################################################################
## Your targets here ##
####################################################################
-####################################################################
-####################################################################
-####################################################################
# This should be the last rule, to handle any targets not declared above
%: invoke-coqmakefile
@true
\end{verbatim}
-\paragraph{Notes for users of {\tt coq\_makefile} with version $<$ 8.7}
+\paragraph{Building a subset of the targets with -j} %%%%%%%%%%%%%%%%%%%%%%%%%
+
+To build, say, two targets \texttt{foo.vo} and \texttt{bar.vo}
+in parallel one can use \texttt{make only TGTS="foo.vo bar.vo" -j}.
+
+Note that \texttt{make foo.vo bar.vo -j} has a different meaning for
+the make utility, in particular it may build a shared prerequisite twice.
+
+\paragraph{Notes for users of {\tt coq\_makefile} with version $<$ 8.7} %%%%%%
\begin{itemize}
\item Support for ``sub-directory'' is deprecated. To perform actions before
@@ -328,13 +378,7 @@ invoke-coqmakefile: CoqMakefile
{\tt CoqMakefile.local}
\end{itemize}
-\paragraph{Note: building a subset of the targets with -j}
-
-To build, say, two targets \texttt{foo.vo} and \texttt{bar.vo}
-in parallel one can use \texttt{make only TGTS="foo.vo bar.vo" -j}.
-
-Note that \texttt{make foo.vo bar.vo -j} has a different meaning for
-the make utility, in particular it may build a shared prerequisite twice.
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section[Modules dependencies]{Modules dependencies\label{Dependencies}\index{Dependencies}
\ttindex{coqdep}}
diff --git a/doc/refman/Setoid.tex b/doc/refman/Setoid.tex
index 6c79284389..0c8cd408f2 100644
--- a/doc/refman/Setoid.tex
+++ b/doc/refman/Setoid.tex
@@ -223,7 +223,7 @@ the following command.
\comindex{Add Parametric Morphism}
\begin{quote}
- \texttt{Add Parametric Morphism} ($x_1 : \T_!$) \ldots ($x_k : \T_k$)\\
+ \texttt{Add Parametric Morphism} ($x_1 : \T_1$) \ldots ($x_k : \T_k$) :
(\textit{f $t_1$ \ldots $t_n$})\\
\texttt{~with signature} \textit{sig}\\
\texttt{~as id}.\\
diff --git a/doc/rt/RefMan-cover.tex b/doc/rt/RefMan-cover.tex
deleted file mode 100644
index ac1686c25e..0000000000
--- a/doc/rt/RefMan-cover.tex
+++ /dev/null
@@ -1,45 +0,0 @@
-\documentstyle[RRcover]{book}
- % The use of the style `french' forces the french abstract to appear first.
-
-\RRtitle{Manuel de r\'ef\'erence du syst\`eme Coq \\ version V7.1}
-\RRetitle{The Coq Proof Assistant \\ Reference Manual \\ Version 7.1
-\thanks
-{This research was partly supported by ESPRIT Basic Research
-Action ``Types'' and by the GDR ``Programmation'' co-financed by MRE-PRC and CNRS.}
-}
-\RRauthor{Bruno Barras, Samuel Boutin, Cristina Cornes,
-Judica\"el Courant, Jean-Christophe Filli\^atre, Eduardo Gim\'enez,
-Hugo Herbelin, G\'erard Huet, C\'esar Mu\~noz, Chetan Murthy,
-Catherine Parent, Christine Paulin-Mohring,
-Amokrane Sa{\"\i}bi, Benjamin Werner}
-\authorhead{}
-\titlehead{Coq V7.1 Reference Manual}
-\RRtheme{2}
-\RRprojet{Coq}
-\RRNo{0123456789}
-\RRdate{May 1997}
-%\RRpages{}
-\URRocq
-
-\RRresume{Coq est un syst\`eme permettant le d\'eveloppement et la
-v\'erification de preuves formelles dans une logique d'ordre
-sup\'erieure incluant un riche langage de d\'efinitions de fonctions.
-Ce document constitue le manuel de r\'ef\'erence de la version V7.1
-qui est distribu\'ee par ftp anonyme \`a l'adresse
-\url{ftp://ftp.inria.fr/INRIA/coq/}}
-
-\RRmotcle{Coq, Syst\`eme d'aide \`a la preuve, Preuves formelles,
-Calcul des Constructions Inductives}
-
-
-\RRabstract{Coq is a proof assistant based on a higher-order logic
-allowing powerful definitions of functions.
-Coq V7.1 is available by anonymous
-ftp at \url{ftp://ftp.inria.fr/INRIA/coq/}}
-
-\RRkeyword{Coq, Proof Assistant, Formal Proofs, Calculus of Inductives
-Constructions}
-
-\begin{document}
-\makeRT
-\end{document}
diff --git a/doc/rt/Tutorial-cover.tex b/doc/rt/Tutorial-cover.tex
deleted file mode 100644
index aefea8d429..0000000000
--- a/doc/rt/Tutorial-cover.tex
+++ /dev/null
@@ -1,47 +0,0 @@
-\documentstyle[RRcover]{book}
- % The use of the style `french' forces the french abstract to appear first.
-\RRetitle{
-The Coq Proof Assistant \\ A Tutorial \\ Version 7.1
-\thanks{This research was partly supported by ESPRIT Basic Research
-Action ``Types'' and by the GDR ``Programmation'' co-financed by MRE-PRC and CNRS.}
-}
-\RRtitle{Coq \\ Une introduction \\ V7.1 }
-\RRauthor{G\'erard Huet, Gilles Kahn and Christine Paulin-Mohring}
-\RRtheme{2}
-\RRprojet{{Coq
-\\[15pt]
-{INRIA Rocquencourt}
-{\hskip -5.25pt}
-~~{\bf ---}~~
- \def\thefootnote{\arabic{footnote}\hss}
-{CNRS - ENS Lyon}
-\footnote[1]{LIP URA 1398 du CNRS,
-46 All\'ee d'Italie, 69364 Lyon CEDEX 07, France.}
-{\hskip -14pt}}}
-
-%\RRNo{0123456789}
-\RRNo{0204}
-\RRdate{Ao\^ut 1997}
-
-\URRocq
-\RRresume{Coq est un syst\`eme permettant le d\'eveloppement et la
-v\'erification de preuves formelles dans une logique d'ordre
-sup\'erieure incluant un riche langage de d\'efinitions de fonctions.
-Ce document constitue une introduction pratique \`a l'utilisation de
-la version V7.1 qui est distribu\'ee par ftp anonyme \`a l'adresse
-\url{ftp://ftp.inria.fr/INRIA/coq/}}
-
-\RRmotcle{Coq, Syst\`eme d'aide \`a la preuve, Preuves formelles, Calcul
-des Constructions Inductives}
-
-\RRabstract{Coq is a proof assistant based on a higher-order logic
-allowing powerful definitions of functions. This document is a
-tutorial for the version V7.1 of Coq. This version is available by
-anonymous ftp at \url{ftp://ftp.inria.fr/INRIA/coq/}}
-
-\RRkeyword{Coq, Proof Assistant, Formal Proofs, Calculus of Inductives
-Constructions}
-
-\begin{document}
-\makeRT
-\end{document}
diff --git a/doc/tools/Translator.tex b/doc/tools/Translator.tex
index ed1d336d9e..3ee65d6f22 100644
--- a/doc/tools/Translator.tex
+++ b/doc/tools/Translator.tex
@@ -614,7 +614,7 @@ is compiled by a Makefile with the following constraints:
\begin{itemize}
\item compilation is achieved by invoking make without specifying a target
\item options are passed to Coq with make variable COQFLAGS that
- includes variables OPT, COQLIBS, OTHERFLAGS and COQ_XML.
+ includes variables OPT, COQLIBS, and OTHERFLAGS.
\end{itemize}
These constraints are met by the makefiles produced by {\tt coq\_makefile}
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 20:07:10 +0000