diff options
Diffstat (limited to 'doc/refman')
| -rw-r--r-- | doc/refman/RefMan-cic.tex | 12 | ||||
| -rw-r--r-- | doc/refman/RefMan-pre.tex | 2 | ||||
| -rw-r--r-- | doc/refman/RefMan-tac.tex | 28 | ||||
| -rw-r--r-- | doc/refman/RefMan-tus.tex | 18 |
4 files changed, 36 insertions, 24 deletions
diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex index b9c17d8148..fdd2725810 100644 --- a/doc/refman/RefMan-cic.tex +++ b/doc/refman/RefMan-cic.tex @@ -79,8 +79,8 @@ An algebraic universe $u$ is either a variable (a qualified identifier with a number) or a successor of an algebraic universe (an expression $u+1$), or an upper bound of algebraic universes (an expression $max(u_1,...,u_n)$), or the base universe (the expression -$0$) which corresponds, in the arity of sort-polymorphic inductive -types (see Section \ref{Sort-polymorphism-inductive}), +$0$) which corresponds, in the arity of template polymorphic inductive +types (see Section \ref{Template-polymorphism}), to the predicative sort {\Set}. A graph of constraints between the universe variables is maintained globally. To ensure the existence of a mapping of the universes to the positive integers, the graph of @@ -977,8 +977,8 @@ Inductive exType (P:Type->Prop) : Type := %is recursive or not. We shall write the type $(x:_R T)C$ if it is %a recursive argument and $(x:_P T)C$ if the argument is not recursive. -\paragraph[Sort-polymorphism of inductive types.]{Sort-polymorphism of inductive types.\index{Sort-polymorphism of inductive types}} -\label{Sort-polymorphism-inductive} +\paragraph[Template polymorphism.]{Template polymorphism.\index{Template polymorphism}} +\label{Template-polymorphism} Inductive types declared in {\Type} are polymorphic over their arguments in {\Type}. @@ -1120,6 +1120,10 @@ Check (fun (A:Prop) (B:Set) => prod A B). Check (fun (A:Type) (B:Prop) => prod A B). \end{coq_example} +\Rem Template polymorphism used to be called ``sort-polymorphism of +inductive types'' before universe polymorphism (see +Chapter~\ref{Universes-full}) was introduced. + \subsection{Destructors} The specification of inductive definitions with arities and constructors is quite natural. But we still have to say how to use an diff --git a/doc/refman/RefMan-pre.tex b/doc/refman/RefMan-pre.tex index f36969e821..0441f952df 100644 --- a/doc/refman/RefMan-pre.tex +++ b/doc/refman/RefMan-pre.tex @@ -529,7 +529,7 @@ intensive computations. Christine Paulin implemented an extension of inductive types allowing recursively non uniform parameters. Hugo Herbelin implemented -sort-polymorphism for inductive types. +sort-polymorphism for inductive types (now called template polymorphism). Claudio Sacerdoti Coen improved the tactics for rewriting on arbitrary compatible equivalence relations. He also generalized rewriting to diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index 0edc66f839..87b9e4914f 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -1275,15 +1275,18 @@ in the list of subgoals remaining to prove. \item{\tt assert ( {\ident} := {\term} )} - This behaves as {\tt assert ({\ident} :\ {\type});[exact - {\term}|idtac]} where {\type} is the type of {\term}. This is - deprecated in favor of {\tt pose proof}. + This behaves as {\tt assert ({\ident} :\ {\type}) by exact {\term}} + where {\type} is the type of {\term}. This is deprecated in favor of + {\tt pose proof}. + + If the head of {\term} is {\ident}, the tactic behaves as + {\tt specialize \term}. \ErrMsg \errindex{Variable {\ident} is already declared} -\item \texttt{pose proof {\term} as {\intropattern}\tacindex{pose proof}} +\item \texttt{pose proof {\term} \zeroone{as {\intropattern}}\tacindex{pose proof}} - This tactic behaves like \texttt{assert T as {\intropattern} by + This tactic behaves like \texttt{assert T \zeroone{as {\intropattern}} by exact {\term}} where \texttt{T} is the type of {\term}. In particular, \texttt{pose proof {\term} as {\ident}} behaves as @@ -1326,8 +1329,8 @@ in the list of subgoals remaining to prove. following subgoals: {\tt U -> T} and \texttt{U}. The subgoal {\tt U -> T} comes first in the list of remaining subgoal to prove. -\item {\tt specialize ({\ident} \term$_1$ \dots\ \term$_n$)\tacindex{specialize}} \\ - {\tt specialize {\ident} with \bindinglist} +\item {\tt specialize ({\ident} \term$_1$ \dots\ \term$_n$)\tacindex{specialize} \zeroone{as \intropattern}}\\ + {\tt specialize {\ident} with {\bindinglist} \zeroone{as \intropattern}} The tactic {\tt specialize} works on local hypothesis \ident. The premises of this hypothesis (either universal @@ -1338,14 +1341,19 @@ in the list of subgoals remaining to prove. second form, all instantiation elements must be given, whereas in the first form the application to \term$_1$ {\ldots} \term$_n$ can be partial. The first form is equivalent to - {\tt assert (\ident' := {\ident} {\term$_1$} \dots\ \term$_n$); - clear \ident; rename \ident' into \ident}. + {\tt assert ({\ident} := {\ident} {\term$_1$} \dots\ \term$_n$)}. + + With the {\tt as} clause, the local hypothesis {\ident} is left + unchanged and instead, the modified hypothesis is introduced as + specified by the {\intropattern}. The name {\ident} can also refer to a global lemma or hypothesis. In this case, for compatibility reasons, the behavior of {\tt specialize} is close to that of {\tt generalize}: the instantiated statement becomes an additional - premise of the goal. + premise of the goal. The {\tt as} clause is especially useful + in this case to immediately introduce the instantiated statement + as a local hypothesis. \begin{ErrMsgs} \item \errindexbis{{\ident} is used in hypothesis \ident'}{is used in hypothesis} diff --git a/doc/refman/RefMan-tus.tex b/doc/refman/RefMan-tus.tex index 797b0adedd..017de6d484 100644 --- a/doc/refman/RefMan-tus.tex +++ b/doc/refman/RefMan-tus.tex @@ -288,8 +288,8 @@ constructors: \item $(\texttt{VAR}\;id)$, a reference to a global identifier called $id$; \item $(\texttt{Rel}\;n)$, a bound variable, whose binder is the $nth$ binder up in the term; -\item $\texttt{DLAM}\;(x,t)$, a deBruijn's binder on the term $t$; -\item $\texttt{DLAMV}\;(x,vt)$, a deBruijn's binder on all the terms of +\item $\texttt{DLAM}\;(x,t)$, a de Bruijn's binder on the term $t$; +\item $\texttt{DLAMV}\;(x,vt)$, a de Bruijn's binder on all the terms of the vector $vt$; \item $(\texttt{DOP0}\;op)$, a unary operator $op$; \item $\texttt{DOP2}\;(op,t_1,t_2)$, the application of a binary @@ -299,7 +299,7 @@ vector of terms $vt$. \end{itemize} In this meta-language, bound variables are represented using the -so-called deBrujin's indexes. In this representation, an occurrence of +so-called de Bruijn's indexes. In this representation, an occurrence of a bound variable is denoted by an integer, meaning the number of binders that must be traversed to reach its own binder\footnote{Actually, $(\texttt{Rel}\;n)$ means that $(n-1)$ binders @@ -339,7 +339,7 @@ on the terms of the meta-language: \fun{val Generic.dependent : 'op term -> 'op term -> bool} {Returns true if the first term is a sub-term of the second.} %\fun{val Generic.subst\_var : identifier -> 'op term -> 'op term} -% { $(\texttt{subst\_var}\;id\;t)$ substitutes the deBruijn's index +% { $(\texttt{subst\_var}\;id\;t)$ substitutes the de Bruijn's index % associated to $id$ to every occurrence of the term % $(\texttt{VAR}\;id)$ in $t$.} \end{description} @@ -482,7 +482,7 @@ following constructor functions: \begin{description} \fun{val Term.mkRel : int -> constr} - {$(\texttt{mkRel}\;n)$ represents deBrujin's index $n$.} + {$(\texttt{mkRel}\;n)$ represents de Bruijn's index $n$.} \fun{val Term.mkVar : identifier -> constr} {$(\texttt{mkVar}\;id)$ @@ -545,7 +545,7 @@ following constructor functions: \fun{val Term.mkProd : name ->constr ->constr -> constr} {$(\texttt{mkProd}\;x\;A\;B)$ represents the product $(x:A)B$. - The free ocurrences of $x$ in $B$ are represented by deBrujin's + The free ocurrences of $x$ in $B$ are represented by de Bruijn's indexes.} \fun{val Term.mkNamedProd : identifier -> constr -> constr -> constr} @@ -553,14 +553,14 @@ following constructor functions: but the bound occurrences of $x$ in $B$ are denoted by the identifier $(\texttt{mkVar}\;x)$. The function automatically changes each occurrences of this identifier into the corresponding - deBrujin's index.} + de Bruijn's index.} \fun{val Term.mkArrow : constr -> constr -> constr} {$(\texttt{arrow}\;A\;B)$ represents the type $(A\rightarrow B)$.} \fun{val Term.mkLambda : name -> constr -> constr -> constr} {$(\texttt{mkLambda}\;x\;A\;b)$ represents the lambda abstraction - $[x:A]b$. The free ocurrences of $x$ in $B$ are represented by deBrujin's + $[x:A]b$. The free ocurrences of $x$ in $B$ are represented by de Bruijn's indexes.} \fun{val Term.mkNamedLambda : identifier -> constr -> constr -> constr} @@ -666,7 +666,7 @@ use the primitive \textsl{Case} described in Chapter \ref{Cic} \item Restoring type coercions and synthesizing the implicit arguments (the one denoted by question marks in {\Coq} syntax: see Section~\ref{Coercions}). -\item Transforming the named bound variables into deBrujin's indexes. +\item Transforming the named bound variables into de Bruijn's indexes. \item Classifying the global names into the different classes of constants (defined constants, constructors, inductive types, etc). \end{enumerate} |