From 72bb3992d912df33bac34f3a1c21989edcf9aa02 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 12 Dec 2015 14:53:00 +0100 Subject: Indexing and documenting some options. --- doc/refman/RefMan-ext.tex | 10 ++++++++++ doc/refman/RefMan-sch.tex | 6 ++++++ doc/refman/Universes.tex | 3 ++- 3 files changed, 18 insertions(+), 1 deletion(-) (limited to 'doc') diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex index a718a26ea5..f2ab79dced 100644 --- a/doc/refman/RefMan-ext.tex +++ b/doc/refman/RefMan-ext.tex @@ -226,6 +226,7 @@ Definition c := {| y := 3; x := 5 |}. This syntax can be disabled globally for printing by \begin{quote} {\tt Unset Printing Records.} +\optindex{Printing Records} \end{quote} For a given type, one can override this using either \begin{quote} @@ -284,6 +285,9 @@ To deactivate the printing of projections, use {\tt Unset Printing Projections}. \subsection{Primitive Projections} +\optindex{Primitive Projections} +\optindex{Printing Primitive Projection Parameters} +\optindex{Printing Primitive Projection Compatibility} \index{Primitive projections} \label{prim-proj} @@ -314,6 +318,12 @@ 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. +For compatibility, the parameters still appear to the user when printing terms +even though they are absent in the actual AST manipulated by the kernel. This +can be changed by unsetting the {\tt Printing Primitive Projection Parameters} +flag. Further compatibility printing can be deactivated 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} diff --git a/doc/refman/RefMan-sch.tex b/doc/refman/RefMan-sch.tex index 571e16d578..53aa6b86ab 100644 --- a/doc/refman/RefMan-sch.tex +++ b/doc/refman/RefMan-sch.tex @@ -126,6 +126,8 @@ conclusion is {\tt (n:nat)(even n)->(Q n)}. \optindex{Boolean Equality Schemes} \optindex{Elimination Schemes} \optindex{Nonrecursive Elimination Schemes} +\optindex{Case Analysis Schemes} +\optindex{Decidable Equality Schemes} \label{set-nonrecursive-elimination-schemes} } @@ -139,6 +141,10 @@ and {\tt Record} (see~\ref{Record}) do not have an automatic declaration of the induction principles. It can be activated with the command {\tt Set Nonrecursive Elimination Schemes}. It can be deactivated again with {\tt Unset Nonrecursive Elimination Schemes}. + +In addition, the {\tt Case Analysis Schemes} flag governs the generation of +case analysis lemmas for inductive types, i.e. corresponding to the +pattern-matching term alone and without fixpoint. \\ You can also activate the automatic declaration of those Boolean equalities diff --git a/doc/refman/Universes.tex b/doc/refman/Universes.tex index ea3cca77ed..a08cd1475a 100644 --- a/doc/refman/Universes.tex +++ b/doc/refman/Universes.tex @@ -159,6 +159,7 @@ unification can have different unfolding behaviors on the same development with universe polymorphism switched on or off. \asection{Minimization} +\optindex{Universe Minimization ToSet} Universe polymorphism with cumulativity tends to generate many useless inclusion constraints in general. Typically at each application of a @@ -248,7 +249,7 @@ User-named universes are considered rigid for unification and are never minimized. \subsection{\tt Unset Strict Universe Declaration. - \optindex{StrictUniverseDeclaration} + \optindex{Strict Universe Declaration} \label{StrictUniverseDeclaration}} The command \texttt{Unset Strict Universe Declaration} allows one to -- cgit v1.2.3 From a275da6e67b91d9ccae0a952eb1feab2e122076e Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Sun, 6 Dec 2015 12:41:55 +0100 Subject: Extraction: documentation of the new option Unset Extraction SafeImplicits --- doc/refman/Extraction.tex | 30 +++++++++++++++++++++++++----- 1 file changed, 25 insertions(+), 5 deletions(-) (limited to 'doc') diff --git a/doc/refman/Extraction.tex b/doc/refman/Extraction.tex index 74c8374de4..a963662f64 100644 --- a/doc/refman/Extraction.tex +++ b/doc/refman/Extraction.tex @@ -198,6 +198,11 @@ this constant is not declared in the generated file. \asubsection{Extra elimination of useless arguments} +The following command provides some extra manual control on the +code elimination performed during extraction, in a way which +is independent but complementary to the main elimination +principles of extraction (logical parts and types). + \begin{description} \item \comindex{Extraction Implicit} {\tt Extraction Implicit} \qualid\ [ \ident$_1$ \dots\ \ident$_n$ ]. @@ -207,12 +212,27 @@ This experimental command allows declaring some arguments of be removed by extraction. Here \qualid\ can be any function or inductive constructor, and \ident$_i$ are the names of the concerned arguments. In fact, an argument can also be referred by a number -indicating its position, starting from 1. When an actual extraction -takes place, an error is raised if the {\tt Extraction Implicit} +indicating its position, starting from 1. +\end{description} + +When an actual extraction takes place, an error is normally raised if the +{\tt Extraction Implicit} declarations cannot be honored, that is if any of the implicited -variables still occurs in the final code. This declaration of useless -arguments is independent but complementary to the main elimination -principles of extraction (logical parts and types). +variables still occurs in the final code. This behavior can be relaxed +via the following option: + +\begin{description} +\item \optindex{Extraction SafeImplicits} {\tt Unset Extraction SafeImplicits.} + +Default is Set. When this option is Unset, a warning is emitted +instead of an error if some implicited variables still occur in the +final code of an extraction. This way, the extracted code may be +obtained nonetheless and reviewed manually to locate the source of the issue +(in the code, some comments mark the location of these remaining +implicited variables). +Note that this extracted code might not compile or run properly, +depending of the use of these remaining implicited variables. + \end{description} \asubsection{Realizing axioms}\label{extraction:axioms} -- cgit v1.2.3 From 81ef6a6dc1bfc3db0e7df3e32b6446fc4d2c4008 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Mon, 14 Dec 2015 11:22:54 +0100 Subject: Moved proof_admitted to its own file, named "AdmitAxiom.v". --- doc/stdlib/index-list.html.template | 1 + 1 file changed, 1 insertion(+) (limited to 'doc') diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template index 866193ffb4..292b2b36cc 100644 --- a/doc/stdlib/index-list.html.template +++ b/doc/stdlib/index-list.html.template @@ -617,6 +617,7 @@ through the Require Import command.

Compatibility wrappers for previous versions of Coq
+ theories/Compat/AdmitAxiom.v theories/Compat/Coq84.v theories/Compat/Coq85.v
-- cgit v1.2.3 From 78c2ebe640e86e7357982e6e07b8121111a51fcc Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Mon, 14 Dec 2015 15:16:35 +0100 Subject: Remove a mention of Set Virtual Machine in doc. --- doc/refman/RefMan-gal.tex | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) (limited to 'doc') diff --git a/doc/refman/RefMan-gal.tex b/doc/refman/RefMan-gal.tex index 0e758bcab6..fcccd9cb4b 100644 --- a/doc/refman/RefMan-gal.tex +++ b/doc/refman/RefMan-gal.tex @@ -496,9 +496,8 @@ arguments is used for making explicit the value of implicit arguments The expression ``{\term}~{\tt :}~{\type}'' is a type cast expression. It enforces the type of {\term} to be {\type}. -``{\term}~{\tt <:}~{\type}'' locally sets up the virtual machine (as if option -{\tt Virtual Machine} were on, see \ref{SetVirtualMachine}) for checking that -{\term} has type {\type}. +``{\term}~{\tt <:}~{\type}'' locally sets up the virtual machine for checking +that {\term} has type {\type}. \subsection{Inferable subterms \label{hole} -- cgit v1.2.3 From 7c645566ef64f09bd6c80007c9e66305ccb90659 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Mon, 14 Dec 2015 15:16:46 +0100 Subject: Fix \label which was meants to be \ref in doc of CIC terms. --- doc/refman/RefMan-cic.tex | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'doc') diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex index e3e49e115d..1554ee04d3 100644 --- a/doc/refman/RefMan-cic.tex +++ b/doc/refman/RefMan-cic.tex @@ -24,7 +24,7 @@ written {\it ``x:T''}. Informally, {\it ``x:T''} can be thought as The types of types are {\em sorts}. Types and sorts are themselves terms so that terms, types and sorts are all components of a common syntactic language of terms which is described in -Section~\label{cic:terms} but, first, we describe sorts. +Section~\ref{cic:terms} but, first, we describe sorts. \subsection[Sorts]{Sorts\label{Sorts} \index{Sorts}} -- cgit v1.2.3