← Back to branch summary

~ubuntu-branches/ubuntu/wily/coq-doc/wily

« back to all changes in this revision

Viewing changes to doc/refman/RefMan-tac.tex

  • Committer: Package Import Robot
  • Author(s): Stéphane Glondu
  • Date: 2012-01-03 23:42:48 UTC
  • mfrom: (1.2.4)
  • Revision ID: package-import@ubuntu.com-20120103234248-p9r8h1579n67v55a
Tags: 8.3pl3-1
New upstream release

Show diffs side-by-side

added added

removed removed

Lines of Context:
doc/refman/RefMan-tac.tex
478
478
  {\bindinglist$_1$}} {\tt ,} \ldots {\tt ,} {\term$_n$} \zeroone{{\tt with}
479
479
  {\bindinglist$_n$}}
480
480
 
481
 
  This summarizes the different syntaxes for {\tt apply}.
 
481
  This summarizes the different syntaxes for {\tt apply} and {\tt eapply}.
482
482
 
483
483
\item {\tt lapply {\term}} \tacindex{lapply} 
484
484
 
699
699
 
700
700
This applies each of {\term} in sequence in {\ident}.
701
701
 
702
 
\item {\tt apply \nelist{{\term} {\bindinglist}}{,} in {\ident}}
 
702
\item {\tt apply \nelist{{\term} with {\bindinglist}}{,} in {\ident}}
703
703
 
704
704
This does the same but uses the bindings in each {\bindinglist} to 
705
705
instantiate the parameters of the corresponding type of {\term}
706
706
(see syntax of bindings in Section~\ref{Binding-list}).
707
707
 
708
 
\item {\tt eapply \nelist{{\term} {\bindinglist}}{,} in {\ident}}
 
708
\item {\tt eapply \nelist{{\term} with {\bindinglist}}{,} in {\ident}}
709
709
\tacindex{eapply {\ldots} in}
710
710
 
711
 
This works as {\tt apply \nelist{{\term} {\bindinglist}}{,} in
 
711
This works as {\tt apply \nelist{{\term} with {\bindinglist}}{,} in
712
712
{\ident}} but turns unresolved bindings into existential variables, if
713
713
any, instead of failing.
714
714
 
715
 
\item {\tt apply \nelist{{\term}{,} {\bindinglist}}{,} in {\ident} as {\disjconjintropattern}}
 
715
\item {\tt apply \nelist{{\term}{,} with {\bindinglist}}{,} in {\ident} as {\disjconjintropattern}}
716
716
 
717
 
This works as {\tt apply \nelist{{\term}{,} {\bindinglist}}{,} in
 
717
This works as {\tt apply \nelist{{\term}{,} with {\bindinglist}}{,} in
718
718
{\ident}} then destructs the hypothesis {\ident} along
719
719
{\disjconjintropattern} as {\tt destruct {\ident} as
720
720
{\disjconjintropattern}} would.
721
721
 
722
 
\item {\tt eapply \nelist{{\term}{,} {\bindinglist}}{,} in {\ident} as {\disjconjintropattern}}
 
722
\item {\tt eapply \nelist{{\term}{,} with {\bindinglist}}{,} in {\ident} as {\disjconjintropattern}}
723
723
 
724
 
This works as {\tt apply \nelist{{\term}{,} {\bindinglist}}{,} in {\ident} as {\disjconjintropattern}} but using {\tt eapply}.
 
724
This works as {\tt apply \nelist{{\term}{,} with {\bindinglist}}{,} in {\ident} as {\disjconjintropattern}} but using {\tt eapply}.
725
725
 
726
726
\item {\tt simple apply {\term} in {\ident}}
727
727
\tacindex{simple apply {\ldots} in} 
736
736
instantiate.  Tactic {\tt simple apply {\term} in {\ident}} does not
737
737
either traverse tuples as {\tt apply {\term} in {\ident}} does.
738
738
 
739
 
\item {\tt simple apply \nelist{{\term}{,} {\bindinglist}}{,} in {\ident} as {\disjconjintropattern}}\\
740
 
{\tt simple eapply \nelist{{\term}{,} {\bindinglist}}{,} in {\ident} as {\disjconjintropattern}}
 
739
\item {\tt \zeroone{simple} apply \nelist{{\term} \zeroone{with {\bindinglist}}}{,} in {\ident} \zeroone{as {\disjconjintropattern}}}\\
 
740
{\tt \zeroone{simple} eapply \nelist{{\term} \zeroone{with {\bindinglist}}}{,} in {\ident} \zeroone{as {\disjconjintropattern}}}
741
741
 
742
 
This are the general forms of {\tt simple apply {\term} in {\ident}} and 
743
 
{\tt simple eapply {\term} in {\ident}}.
 
742
This summarizes the different syntactic variants of {\tt apply {\term}
 
743
  in {\ident}} and {\tt eapply {\term} in {\ident}}.
744
744
\end{Variants}
745
745
 
746
746
\subsection{\tt generalize \term
1019
1019
 
1020
1020
\ErrMsg \errindex{No evars}
1021
1021
 
 
1022
\subsection{\tt is\_var \term
 
1023
\tacindex{is\_var}
 
1024
\label{isvar}}
 
1025
 
 
1026
This tactic applies to any goal. It checks whether its argument is a
 
1027
variable or hypothesis in the current goal context or in the opened sections.
 
1028
 
 
1029
\ErrMsg \errindex{Not a variable or hypothesis}
 
1030
 
1022
1031
\subsection{Bindings list
1023
1032
\index{Binding list}
1024
1033
\label{Binding-list}}
1052
1061
  type are required.
1053
1062
 
1054
1063
  \ErrMsg \errindex{Not the right number of missing arguments}
1055
 
 
1056
1064
\end{itemize}
1057
1065
 
1058
1066
\subsection{Occurrences sets and occurrences clauses}
1586
1594
  disjunction $A\lor B$. Then, they are respectively equivalent to {\tt
1587
1595
    constructor 1} and {\tt constructor 2}.
1588
1596
  
1589
 
\item {\tt left \bindinglist}\\
1590
 
      {\tt right \bindinglist}\\
1591
 
      {\tt split \bindinglist}
 
1597
\item {\tt left with \bindinglist}\\
 
1598
      {\tt right with \bindinglist}\\
 
1599
      {\tt split with \bindinglist}
1592
1600
  
1593
1601
  As soon as the inductive type has the right number of constructors,
1594
 
    these expressions are equivalent to the corresponding {\tt
1595
 
    constructor $i$ with \bindinglist}.
 
1602
    these expressions are equivalent to calling {\tt
 
1603
    constructor $i$ with \bindinglist} for the appropriate $i$.
1596
1604
 
1597
1605
\item \texttt{econstructor}\tacindex{econstructor}\\
1598
1606
      \texttt{eexists}\tacindex{eexists}\\
4324
4332
user-defined tactics.
4325
4333
 
4326
4334
 
4327
 
% $Id: RefMan-tac.tex 13659 2010-11-29 11:09:07Z glondu $ 
 
4335
% $Id: RefMan-tac.tex 14762 2011-12-04 20:48:36Z herbelin $ 
4328
4336
 
4329
4337
%%% Local Variables: 
4330
4338
%%% mode: latex