diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-10-24 23:15:16 +0200 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-10-24 23:15:16 +0200 |
commit | 8232f27773f3463600fbaac0f70966bd4893ea20 (patch) | |
tree | 3a341815e0f49b3903f96c230cdd99303f62dd24 | |
parent | 810077167cd6f5077abe7b79b12ae9b51eae1b62 (diff) | |
parent | 014e02e0a7d469d46bf5d8314efe039bea3c0dbe (diff) |
Merge branch 'v8.5' into v8.6
-rw-r--r-- | doc/refman/RefMan-tac.tex | 61 | ||||
-rw-r--r-- | test-suite/success/Notations.v | 6 |
2 files changed, 55 insertions, 12 deletions
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index 2da12c8d6..dd45feebc 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -3489,7 +3489,7 @@ hints of the database named {\tt core}. Uses the hint databases $\ident_1$ \dots\ $\ident_n$ in addition to the database {\tt core}. See Section~\ref{Hints-databases} for the list of pre-defined databases and the way to create or extend a - database. This option can be combined with the previous one. + database. \item {\tt auto with *} @@ -3503,9 +3503,17 @@ hints of the database named {\tt core}. $lemma_i$ is an inductive type, it is the collection of its constructors which is added as hints. -\item \texttt{auto using} \nterm{lemma}$_1$ {\tt ,} {\ldots} {\tt ,} \nterm{lemma}$_n$ with \ident$_1$ {\ldots} \ident$_n$ +\item {\tt info\_auto} - This combines the effects of the {\tt using} and {\tt with} options. + Behaves like {\tt auto} but shows the tactics it uses to solve the goal. + This variant is very useful for getting a better understanding of automation, + or to know what lemmas/assumptions were used. + +\item {\tt \zeroone{info\_}auto \zeroone{\num}} \zeroone{{\tt using} \nterm{lemma}$_1$ + {\tt ,} {\ldots} {\tt ,} \nterm{lemma}$_n$} \zeroone{{\tt with} + \ident$_1$ {\ldots} \ident$_n$} + + This is the most general form, combining the various options. \item {\tt trivial}\tacindex{trivial} @@ -3517,6 +3525,14 @@ hints of the database named {\tt core}. \item \texttt{trivial with *} +\item \texttt{trivial using} \nterm{lemma}$_1$ {\tt ,} {\ldots} {\tt ,} \nterm{lemma}$_n$ + +\item {\tt info\_trivial} + +\item {\tt \zeroone{info\_}trivial} \zeroone{{\tt using} \nterm{lemma}$_1$ + {\tt ,} {\ldots} {\tt ,} \nterm{lemma}$_n$} \zeroone{{\tt with} + \ident$_1$ {\ldots} \ident$_n$} + \end{Variants} \Rem {\tt auto} either solves completely the goal or else leaves it @@ -3530,8 +3546,8 @@ intact. \texttt{auto} and \texttt{trivial} never fail. 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}). +{\tt eauto} does try them (informally speaking, it uses +{\tt simple eapply} where {\tt auto} uses {\tt simple apply}). As a consequence, {\tt eauto} can solve such a goal: \begin{coq_eval} @@ -3546,8 +3562,17 @@ eauto. Abort. \end{coq_eval} -Note that {\tt ex\_intro} should be declared as an -hint. +Note that {\tt ex\_intro} should be declared as a hint. + +\begin{Variants} + +\item {\tt \zeroone{info\_}eauto \zeroone{\num}} \zeroone{{\tt using} \nterm{lemma}$_1$ + {\tt ,} {\ldots} {\tt ,} \nterm{lemma}$_n$} \zeroone{{\tt with} + \ident$_1$ {\ldots} \ident$_n$} + + The various options for eauto are the same as for auto. + +\end{Variants} \SeeAlso Section~\ref{Hints-databases} @@ -3701,11 +3726,12 @@ The {\hintdef} is one of the following expressions: 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 - % 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. + In case the inferred type of \term\ does not start with a product + the tactic added in the hint list is {\tt exact {\term}}. +% Actually, a slightly restricted version is used (no conversion on the head symbol) + In case + this type can however be reduced to a type starting with a product, + the tactic {\tt simple 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 @@ -3735,6 +3761,17 @@ The {\hintdef} is one of the following expressions: Adds each \texttt{Resolve} {\term$_i$}. + \item {\tt Resolve -> \term} + + Adds the left-to-right implication of an equivalence as a hint + (informally the hint will be used as {\tt apply <- \term}, + although as mentionned before, the tactic actually used is + a restricted version of apply). + + \item {\tt Resolve <- \term} + + Adds the right-to-left implication of an equivalence as a hint. + \end{Variants} \item \texttt{Immediate {\term}} diff --git a/test-suite/success/Notations.v b/test-suite/success/Notations.v index 666c91257..07bbb60c4 100644 --- a/test-suite/success/Notations.v +++ b/test-suite/success/Notations.v @@ -122,3 +122,9 @@ Goal True. {{ exact I. }} Qed. Check |- {{ 0 }} 0. + +(* Check parsing of { and } is not affected by notations #3479 *) +Notation " |- {{ a }} b" := (a=b) (no associativity, at level 10). +Goal True. +{{ exact I. }} +Qed. |