From 15e2280fe975fa5a4376ee45557d3e532e208496 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Mon, 20 Feb 2017 22:22:48 +0100
Subject: Fix V7 syntax in refman.
---
doc/refman/RefMan-pro.tex | 6 +++---
1 file changed, 3 insertions(+), 3 deletions(-)
(limited to 'doc')
diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex
index c37367de5b..16c822b6a5 100644
--- a/doc/refman/RefMan-pro.tex
+++ b/doc/refman/RefMan-pro.tex
@@ -477,15 +477,15 @@ names.
\item{\tt Show Intro.}\comindex{Show Intro}\\
If the current goal begins by at least one product, this command
prints the name of the first product, as it would be generated by
-an anonymous {\tt Intro}. The aim of this command is to ease the
+an anonymous {\tt intro}. The aim of this command is to ease the
writing of more robust scripts. For example, with an appropriate
{\ProofGeneral} macro, it is possible to transform any anonymous {\tt
- Intro} into a qualified one such as {\tt Intro y13}.
+ intro} into a qualified one such as {\tt intro y13}.
In the case of a non-product goal, it prints nothing.
\item{\tt Show Intros.}\comindex{Show Intros}\\
This command is similar to the previous one, it simulates the naming
-process of an {\tt Intros}.
+process of an {\tt intros}.
\item{\tt Show Existentials.\label{ShowExistentials}}\comindex{Show Existentials}
\\ It displays
--
cgit v1.2.3
From 7497d4129775d15cdce862a0ac681c6400aabe54 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 6 Oct 2016 07:02:24 +0200
Subject: Logic library: Adding a characterization of excluded-middle in term
of choice of a representative in a partition of bool.
Also move a result about propositional extensionality from
ClassicalFacts.v to PropExtensionalityFacts.v, generalizing it by
symmetry.
Also spotting typos (thanks to Théo).
---
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 9216c81fcd..4a685a3b85 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -55,6 +55,7 @@ through the Require Import command.
theories/Logic/Description.v
theories/Logic/Epsilon.v
theories/Logic/IndefiniteDescription.v
+ theories/Logic/PropExtensionalityFacts.v
theories/Logic/FunctionalExtensionality.v
theories/Logic/ExtensionalityFacts.v
theories/Logic/WeakFan.v
--
cgit v1.2.3
From 9c21392c7957a0a1a66e5269022d5991649a38b5 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 2 Oct 2016 22:02:52 +0200
Subject: Adding a file providing extensional choice (i.e. choice over
setoids).
Also integrating suggestions from Théo.
---
doc/stdlib/index-list.html.template | 2 ++
1 file changed, 2 insertions(+)
(limited to 'doc')
diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index 4a685a3b85..4ffdbb1152 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -46,6 +46,7 @@ through the Require Import command.
theories/Logic/ClassicalDescription.v
theories/Logic/ClassicalEpsilon.v
theories/Logic/ClassicalUniqueChoice.v
+ theories/Logic/SetoidChoice.v
theories/Logic/Berardi.v
theories/Logic/Diaconescu.v
theories/Logic/Hurkens.v
@@ -57,6 +58,7 @@ through the Require Import command.
theories/Logic/IndefiniteDescription.v
theories/Logic/PropExtensionalityFacts.v
theories/Logic/FunctionalExtensionality.v
+ theories/Logic/ExtensionalFunctionRepresentative.v
theories/Logic/ExtensionalityFacts.v
theories/Logic/WeakFan.v
theories/Logic/WKL.v
--
cgit v1.2.3
From 4e85cc6e9792da116f1b20e484b2ce629c6f6865 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 2 Oct 2016 20:27:59 +0200
Subject: Adding explicitly a file to work in the context of propositional
extensionality.
---
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 4ffdbb1152..aeb0de48a3 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -56,6 +56,7 @@ through the Require Import command.
theories/Logic/Description.v
theories/Logic/Epsilon.v
theories/Logic/IndefiniteDescription.v
+ theories/Logic/PropExtensionality.v
theories/Logic/PropExtensionalityFacts.v
theories/Logic/FunctionalExtensionality.v
theories/Logic/ExtensionalFunctionRepresentative.v
--
cgit v1.2.3
From b7415c84269b1553470216b06871def933e2f3bd Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 9 Mar 2017 13:50:22 +0100
Subject: Clarifying doc about interpretation of scopes in notations (#5386).
---
doc/refman/RefMan-syn.tex | 28 ++++++++++++++++++++++++++++
1 file changed, 28 insertions(+)
(limited to 'doc')
diff --git a/doc/refman/RefMan-syn.tex b/doc/refman/RefMan-syn.tex
index 21c39de967..b7d36ecaa3 100644
--- a/doc/refman/RefMan-syn.tex
+++ b/doc/refman/RefMan-syn.tex
@@ -59,6 +59,12 @@ and pretty-printer of {\Coq} already know how to deal with the
syntactic expression (see \ref{ReservedNotation}), explicit precedences and
associativity rules have to be given.
+\Rem The right-hand side of a notation is interpreted at the time the
+notation is given. In particular, implicit arguments (see
+Section~\ref{Implicit Arguments}), coercions (see
+Section~\ref{Coercions}), etc. are resolved at the time of the
+declaration of the notation.
+
\subsection[Precedences and associativity]{Precedences and associativity\index{Precedences}
\index{Associativity}}
@@ -908,6 +914,28 @@ 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}.
+\Rem In notations, the subterms matching the identifiers of the
+notations are interpreted in the scope in which the identifiers
+occurred at the time of the declaration of the notation. Here is an
+example:
+
+\begin{coq_example}
+Parameter g : bool -> bool.
+Notation "@@" := true (only parsing) : bool_scope.
+Notation "@@" := false (only parsing): mybool_scope.
+
+(* Defining a notation while the argument of g is bound to bool_scope *)
+Bind Scope bool_scope with bool.
+Notation "# x #" := (g x) (at level 40).
+Check # @@ #.
+(* Rebinding the argument of g to mybool_scope has no effect on the notation *)
+Arguments g _%mybool_scope.
+Check # @@ #.
+(* But we can force the scope *)
+Delimit Scope mybool_scope with mybool.
+Check # @@%mybool #.
+\end{coq_example}
+
\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
--
cgit v1.2.3
From cae09e5af6cf31d96662b1b66a63c6a236a8e741 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 9 Mar 2017 15:36:42 +0100
Subject: Typo doc notations.
---
doc/refman/RefMan-syn.tex | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
(limited to 'doc')
diff --git a/doc/refman/RefMan-syn.tex b/doc/refman/RefMan-syn.tex
index b7d36ecaa3..61093709ec 100644
--- a/doc/refman/RefMan-syn.tex
+++ b/doc/refman/RefMan-syn.tex
@@ -303,7 +303,7 @@ the possible following elements delimited by single quotes:
of each newline
\end{itemize}
-Thus, for the previous example, we get
+%Thus, for the previous example, we get
%\footnote{The ``@'' is here to shunt
%the notation "'IF' A 'then' B 'else' C" which is defined in {\Coq}
%initial state}:
--
cgit v1.2.3
From b087d133f7d6d091cce72190c05a9a09d5b37791 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Tue, 14 Mar 2017 21:24:53 +0100
Subject: [toplevel] Remove unusable option -notop
Maxime points out that -notop cannot be used as the kernel requires
all constants to belong into a module. Indeed:
```
$ rlwrap ./bin/coqtop -notop
Coq < Definition foo := True.
Toplevel input, characters 0-23:
> Definition foo := True.
> ^^^^^^^^^^^^^^^^^^^^^^^
Error: No session module started (use -top dir)
Coq < Module M. Definition foo := True. End M.
Module M is defined
Coq < Locate foo.
Constant If you see this, it's a bug.M.foo
(shorter name to refer to it in current context is M.foo)
```
My rationale for the removal is that this kind of incomplete features
are often confusing to newcomers ─ it has happened to me many times ─
as it can be seen for example in #397 .
---
doc/refman/RefMan-com.tex | 6 ------
doc/refman/RefMan-ext.tex | 2 +-
2 files changed, 1 insertion(+), 7 deletions(-)
(limited to 'doc')
diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex
index bef0a1686f..45230fb6e5 100644
--- a/doc/refman/RefMan-com.tex
+++ b/doc/refman/RefMan-com.tex
@@ -123,12 +123,6 @@ The following command-line options are recognized by the commands {\tt
valid for {\tt coqc} as the toplevel module name is inferred from the
name of the output file.
-\item[{\tt -notop}]\ %
-
- Use the empty logical path for the toplevel module name instead of {\tt
- Top}. Not valid for {\tt coqc} as the toplevel module name is
- inferred from the name of the output file.
-
\item[{\tt -exclude-dir} {\em directory}]\ %
Exclude any subdirectory named {\em directory} while
diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex
index b475a5233c..1d423f8b16 100644
--- a/doc/refman/RefMan-ext.tex
+++ b/doc/refman/RefMan-ext.tex
@@ -991,7 +991,7 @@ but library file names based on other roots can be obtained by using
{\Coq} commands ({\tt coqc}, {\tt coqtop}, {\tt coqdep}, \dots) options
{\tt -Q} or {\tt -R} (see Section~\ref{coqoptions}). Also, when an
interactive {\Coq} session starts, a library of root {\tt Top} is
-started, unless option {\tt -top} or {\tt -notop} is set (see
+started, unless option {\tt -top} is set (see
Section~\ref{coqoptions}).
\subsection{Qualified names
--
cgit v1.2.3
From 347827ef4ea72048762c1677f37cb716109a5d9c Mon Sep 17 00:00:00 2001
From: Valentin Robert
Date: Thu, 16 Feb 2017 14:37:47 -0800
Subject: doc: fix a French-ism
---
doc/refman/RefMan-syn.tex | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
(limited to 'doc')
diff --git a/doc/refman/RefMan-syn.tex b/doc/refman/RefMan-syn.tex
index 21c39de967..ce662eb208 100644
--- a/doc/refman/RefMan-syn.tex
+++ b/doc/refman/RefMan-syn.tex
@@ -114,7 +114,7 @@ Notation "A \/ B" := (or A B) (at level 85, right associativity).
By default, a notation is considered non associative, but the
precedence level is mandatory (except for special cases whose level is
-canonical). The level is either a number or the mention {\tt next
+canonical). The level is either a number or the phrase {\tt next
level} whose meaning is obvious. The list of levels already assigned
is on Figure~\ref{init-notations}.
--
cgit v1.2.3
From 9e621625618e1a0f341b87d66c1ea6027369c2e5 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Tue, 20 Dec 2016 16:11:03 +0100
Subject: Fix some typos.
---
doc/refman/Polynom.tex | 8 ++++----
1 file changed, 4 insertions(+), 4 deletions(-)
(limited to 'doc')
diff --git a/doc/refman/Polynom.tex b/doc/refman/Polynom.tex
index 0664bf9095..77d5928345 100644
--- a/doc/refman/Polynom.tex
+++ b/doc/refman/Polynom.tex
@@ -342,16 +342,16 @@ describes their syntax and effects:
By default the tactic does not recognize power expressions as ring
expressions.
\item[sign {\term}] allows {\tt ring\_simplify} to use a minus operation
- when outputing its normal form, i.e writing $x - y$ instead of $x + (-y)$.
+ when outputting its normal form, i.e writing $x - y$ instead of $x + (-y)$.
The term {\term} is a proof that a given sign function indicates expressions
that are signed ({\term} has to be a
- proof of {\tt Ring\_theory.get\_sign}). See {\tt plugins/setoid\_ring/IntialRing.v} for examples of sign function.
-\item[div {\term}] allows {\tt ring} and {\tt ring\_simplify} to use moniomals
+ proof of {\tt Ring\_theory.get\_sign}). See {\tt plugins/setoid\_ring/InitialRing.v} for examples of sign function.
+\item[div {\term}] allows {\tt ring} and {\tt ring\_simplify} to use monomials
with coefficient other than 1 in the rewriting. The term {\term} is a proof that a given division function satisfies the specification of an euclidean
division function ({\term} has to be a
proof of {\tt Ring\_theory.div\_theory}). For example, this function is
called when trying to rewrite $7x$ by $2x = z$ to tell that $7 = 3 * 2 + 1$.
- See {\tt plugins/setoid\_ring/IntialRing.v} for examples of div function.
+ See {\tt plugins/setoid\_ring/InitialRing.v} for examples of div function.
\end{description}
--
cgit v1.2.3