diff options
author | Arnaud Spiwack <arnaud@spiwack.net> | 2014-08-05 14:47:07 +0200 |
---|---|---|
committer | Arnaud Spiwack <arnaud@spiwack.net> | 2014-08-05 16:52:14 +0200 |
commit | e8b01bbabc0550c289617c867ea8ce2e19579417 (patch) | |
tree | b48daab88e5926798f270bfcce89a3b9bb596089 /doc/refman/RefMan-ltac.tex | |
parent | 2569645c3bf0944b24bac50cb61887097f50224a (diff) |
Documentation: refine accept uconstr arguments.
Diffstat (limited to 'doc/refman/RefMan-ltac.tex')
-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 |