diff options
-rw-r--r-- | doc/refman/RefMan-ltac.tex | 9 |
1 files changed, 8 insertions, 1 deletions
diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex index cf2e70814..8c5eee7f4 100644 --- a/doc/refman/RefMan-ltac.tex +++ b/doc/refman/RefMan-ltac.tex @@ -885,7 +885,8 @@ The following returns the type of {\term}: The terms built in Ltac are well-typed by default. It may not be appropriate for building large terms using a recursive Ltac function: the term has to be entirely type checked at each step, resulting in -potentially very slow behavior. It is possible to build untyped terms using Ltac with the syntax +potentially very slow behavior. It is possible to build untyped terms +using Ltac with the syntax \begin{quote} {\tt uconstr :} {\term} @@ -902,6 +903,12 @@ term which can be used in tactics. {\tt type\_term} {\term} \end{quote} +Untyped terms built using {\tt uconstr :} can also be used as +arguments to the {\tt refine} tactic~\ref{refine}. In that case the +untyped term is type checked against the conclusion of the goal, and +the holes which are not solved by the typing procedure are turned into +new subgoals. + \subsubsection[Counting the goals]{Counting the goals\index{Ltac!numgoals}\index{numgoals!in Ltac}} The number of goals under focus can be recovered using the {\tt |