From 0e37dc665cf7a6a9ed7d0d10199dd40134cf0148 Mon Sep 17 00:00:00 2001
From: Pierre Courtieu
Date: Fri, 12 May 2017 10:51:46 +0200
Subject: Documenting the new behaviour of specialize.

---
 doc/refman/RefMan-tac.tex | 10 +++++++---
 1 file changed, 7 insertions(+), 3 deletions(-)

diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index fc3fdd0025..15df2e601d 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -1337,12 +1337,16 @@ in the list of subgoals remaining to prove.
       quantifications or non-dependent implications) are instantiated
       by concrete terms coming either from arguments \term$_1$
       $\ldots$ \term$_n$ or from a bindings list (see
-      Section~\ref{Binding-list} for more about bindings lists). In the
-      second form, all instantiation elements must be given, whereas
-      in the first form the application to \term$_1$ {\ldots}
+      Section~\ref{Binding-list} for more about bindings lists). 
+      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$)}.
 
+      In the second form, instantiation elements can also be partial.
+      In this case the uninstantiated arguments are inferred by
+      unification if possible or left quantified in the hypothesis
+      otherwise.
+
       With the {\tt as} clause, the local hypothesis {\ident} is left
       unchanged and instead, the modified hypothesis is introduced as
       specified by the {\intropattern}.
-- 
cgit v1.2.3