From 9227d6e9412ae4ebe70fb9b6bd5d2f6ecc354864 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 1 Oct 2015 09:29:10 +0200
Subject: Improving reference manual in that auto uses simple apply rather than
apply.
Still, there are small differences, e.g. on
"use_metas_eagerly_in_conv_on_closed_terms", but also maybe in some
amount of use of delta that Matthieu would know better than me if it
matters or not in practice.
---
doc/refman/RefMan-tac.tex | 51 ++++++++++++++++++++++++++---------------------
1 file changed, 28 insertions(+), 23 deletions(-)
(limited to 'doc')
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index fa6f783934..06431055ad 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -3394,7 +3394,7 @@ local definition. Example: {\tt unfold not in (Type of H1) (Type of H3).}
This tactic implements a Prolog-like resolution procedure to solve the
current goal. It first tries to solve the goal using the {\tt
assumption} tactic, then it reduces the goal to an atomic one using
-{\tt intros} and introducing the newly generated hypotheses as hints.
+{\tt intros} and introduces the newly generated hypotheses as hints.
Then it looks at the list of tactics associated to the head symbol of
the goal and tries to apply one of them (starting from the tactics
with lower cost). This process is recursively applied to the generated
@@ -3454,11 +3454,10 @@ intact. \texttt{auto} and \texttt{trivial} never fail.
\tacindex{eauto}
\label{eauto}
-This tactic generalizes {\tt auto}. In contrast with
-the latter, {\tt eauto} uses unification of the goal
-against the hints rather than pattern-matching
-(in other words, it uses {\tt eapply} instead of
-{\tt apply}).
+This tactic generalizes {\tt auto}. While {\tt auto} does not try
+resolution hints which would leave existential variables in the goal,
+{\tt eauto} does try them (informally speaking, it uses {\tt eapply}
+where {\tt auto} uses {\tt apply}).
As a consequence, {\tt eauto} can solve such a goal:
\begin{coq_eval}
@@ -3623,21 +3622,27 @@ The {\hintdef} is one of the following expressions:
\item {\tt Resolve \term}
\comindex{Hint Resolve}
- This command adds {\tt apply {\term}} to the hint list
+ This command adds {\tt simple apply {\term}} to the hint list
with the head symbol of the type of \term. The cost of that hint is
- the number of subgoals generated by {\tt apply {\term}}.
-
- In case the inferred type of \term\ does not start with a product the
- tactic added in the hint list is {\tt exact {\term}}. In case this
- type can be reduced to a type starting with a product, the tactic {\tt
- apply {\term}} is also stored in the hints list.
-
- If the inferred type of \term\ contains a dependent
- quantification on a predicate, it is added to the hint list of {\tt
- eapply} instead of the hint list of {\tt apply}. In this case, a
- warning is printed since the hint is only used by the tactic {\tt
- eauto} (see \ref{eauto}). A typical example of a hint that is used
- only by \texttt{eauto} is a transitivity lemma.
+ the number of subgoals generated by {\tt simple apply {\term}}.
+%{\tt auto} actually uses a slightly modified variant of {\tt simple apply} with use_metas_eagerly_in_conv_on_closed_terms set to false
+
+ The cost of that hint is the number of subgoals generated by that
+ tactic.
+
+ % Is it really needed?
+ %% In case the inferred type of \term\ does not start with a product
+ %% the tactic added in the hint list is {\tt exact {\term}}. In case
+ %% this type can however be reduced to a type starting with a product,
+ %% the tactic {\tt apply {\term}} is also stored in the hints list.
+
+ If the inferred type of \term\ contains a dependent quantification
+ on a variable which occurs only in the premisses of the type and not
+ in its conclusion, no instance could be inferred for the variable by
+ unification with the goal. In this case, the hint is added to the
+ hint list of {\tt eauto} (see \ref{eauto}) instead of the hint list
+ of {\tt auto} and a warning is printed. A typical example of a hint
+ that is used only by \texttt{eauto} is a transitivity lemma.
\begin{ErrMsgs}
\item \errindex{Bound head variable}
@@ -3649,7 +3654,7 @@ The {\hintdef} is one of the following expressions:
The type of {\term} contains products over variables that do not
appear in the conclusion. A typical example is a transitivity axiom.
- In that case the {\tt apply} tactic fails, and thus is useless.
+ In that case the {\tt simple apply} tactic fails, and thus is useless.
\end{ErrMsgs}
@@ -3664,10 +3669,10 @@ The {\hintdef} is one of the following expressions:
\item \texttt{Immediate {\term}}
\comindex{Hint Immediate}
- This command adds {\tt apply {\term}; trivial} to the hint list
+ This command adds {\tt simple apply {\term}; trivial} to the hint list
associated with the head symbol of the type of {\ident} in the given
database. This tactic will fail if all the subgoals generated by
- {\tt apply {\term}} are not solved immediately by the {\tt trivial}
+ {\tt simple apply {\term}} are not solved immediately by the {\tt trivial}
tactic (which only tries tactics with cost $0$).
This command is useful for theorems such as the symmetry of equality
--
cgit v1.2.3
From 5e62675419fb6a5a8f8a86fbf3f6df4427e70d21 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 2 Oct 2015 16:50:26 +0200
Subject: Fixing error messages about Hint.
---
doc/refman/RefMan-tac.tex | 18 ++++++++++--------
1 file changed, 10 insertions(+), 8 deletions(-)
(limited to 'doc')
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 06431055ad..a21e5631fc 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -3645,16 +3645,16 @@ The {\hintdef} is one of the following expressions:
that is used only by \texttt{eauto} is a transitivity lemma.
\begin{ErrMsgs}
- \item \errindex{Bound head variable}
+%% \item \errindex{Bound head variable}
+
+ \item \term\ \errindex{cannot be used as a hint}
The head symbol of the type of {\term} is a bound variable such
that this tactic cannot be associated to a constant.
- \item \term\ \errindex{cannot be used as a hint}
-
- The type of {\term} contains products over variables that do not
- appear in the conclusion. A typical example is a transitivity axiom.
- In that case the {\tt simple apply} tactic fails, and thus is useless.
+ %% The type of {\term} contains products over variables that do not
+ %% appear in the conclusion. A typical example is a transitivity axiom.
+ %% In that case the {\tt simple apply} tactic fails, and thus is useless.
\end{ErrMsgs}
@@ -3684,7 +3684,7 @@ The {\hintdef} is one of the following expressions:
\begin{ErrMsgs}
- \item \errindex{Bound head variable}
+%% \item \errindex{Bound head variable}
\item \term\ \errindex{cannot be used as a hint}
@@ -3710,7 +3710,9 @@ The {\hintdef} is one of the following expressions:
\item {\ident} \errindex{is not an inductive type}
- \item {\ident} \errindex{not declared}
+% No need to have this message here, is is generic to all commands
+% referring to globals
+%% \item {\ident} \errindex{not declared}
\end{ErrMsgs}
--
cgit v1.2.3
From f41de34bcd48f008cf7d3fae4c7fce925048e606 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Fri, 2 Oct 2015 21:32:25 +0200
Subject: Mark the Coq.Compat files for documentation. (Fix bug #4353)
---
doc/stdlib/index-list.html.template | 10 +++++++++-
1 file changed, 9 insertions(+), 1 deletion(-)
(limited to 'doc')
diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index 024e13413a..866193ffb4 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -591,7 +591,7 @@ through the Require Import command.
Program:
- Support for dependently-typed programming.
+ Support for dependently-typed programming
theories/Program/Basics.v
@@ -612,4 +612,12 @@ through the Require Import command.
theories/Unicode/Utf8_core.v
theories/Unicode/Utf8.v
+
+ Compat:
+ Compatibility wrappers for previous versions of Coq
+
+
+ theories/Compat/Coq84.v
+ theories/Compat/Coq85.v
+
--
cgit v1.2.3
From 2b033589d1b7900fdb86dfad145f1c284657ae8c Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Sun, 4 Oct 2015 09:22:16 +0200
Subject: Fix typo. (Fix bug #4355)
---
doc/refman/RefMan-oth.tex | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
(limited to 'doc')
diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex
index 739a89af4c..4b2b8660c2 100644
--- a/doc/refman/RefMan-oth.tex
+++ b/doc/refman/RefMan-oth.tex
@@ -967,8 +967,8 @@ the constants {\qualid$_1$} {\ldots} {\qualid$_n$} in tactics using
$\delta$-conversion (unfolding a constant is replacing it by its
definition).
-{\tt Opaque} has also on effect on the conversion algorithm of {\Coq},
-telling it to delay the unfolding of a constant as mush as possible when
+{\tt Opaque} has also an effect on the conversion algorithm of {\Coq},
+telling it to delay the unfolding of a constant as much as possible when
{\Coq} has to check the conversion (see Section~\ref{conv-rules})
of two distinct applied constants.
--
cgit v1.2.3