From cd440dbd43a632cf8f445a80d034f36e4235c63e Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Sat, 10 Oct 2015 13:02:56 +0200
Subject: Fix a few latex errors in documentation of Proof Using (e.g. \tt*).

---
 doc/refman/RefMan-pro.tex | 13 ++++++++-----
 1 file changed, 8 insertions(+), 5 deletions(-)

(limited to 'doc')

diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex
index 5dbf315535..481afa8f87 100644
--- a/doc/refman/RefMan-pro.tex
+++ b/doc/refman/RefMan-pro.tex
@@ -165,14 +165,17 @@ in Section~\ref{ProofWith}.
   {\tt Type* } is the forward transitive closure of the entire set of
   section variables occurring in the statement.
 
-\variant {\tt Proof using -(} {\ident$_1$} {\ldots} {\ident$_n$} {\tt ).}
+\variant {\tt Proof using -( \ident$_1$} {\ldots} {\tt \ident$_n$  ).}
   
   Use all section variables except {\ident$_1$} {\ldots} {\ident$_n$}.
 
-\variant {\tt Proof using }  {\emph collection$_1$} {\tt + } {\emph collection$_2$} {\tt .}
-\variant {\tt Proof using }  {\emph collection$_1$} {\tt - } {\emph collection$_2$} {\tt .}
-\variant {\tt Proof using }  {\emph collection$_1$} {\tt - (} {\ident$_1$} {\ldots} {\ident$_n$} {\tt ).}
-\variant {\tt Proof using }  {\emph collection$_1$}{\tt* .}
+\variant {\tt Proof using \nterm{collection}$_1$ + \nterm{collection}$_2$ .}
+
+\variant {\tt Proof using \nterm{collection}$_1$ - \nterm{collection}$_2$ .}
+
+\variant {\tt Proof using \nterm{collection} - ( \ident$_1$} {\ldots} {\tt \ident$_n$ ).}
+
+\variant {\tt Proof using \nterm{collection} * .}
 
   Use section variables being, respectively, in the set union, set difference,
   set complement, set forward transitive closure.
-- 
cgit v1.2.3


From bf39345125d66d3efd9f934be91200013f57841c Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 11 Oct 2015 16:29:54 +0200
Subject: Documenting matching under binders.

---
 doc/refman/RefMan-ltac.tex | 7 +++++++
 1 file changed, 7 insertions(+)

(limited to 'doc')

diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex
index d388840df5..04c356e44f 100644
--- a/doc/refman/RefMan-ltac.tex
+++ b/doc/refman/RefMan-ltac.tex
@@ -691,6 +691,13 @@ variables of the form {\tt @?id} that occur in head position of an
 application. For these variables, the matching is second-order and
 returns a functional term.
 
+Alternatively, when a metavariable of the form {\tt ?id} occurs under
+binders, say $x_1$, \ldots, $x_n$ and the expression matches, the
+metavariable is instantiated by a term which can then be used in any
+context which also binds the variables $x_1$, \ldots, $x_n$ with
+same types. This provides with a primitive form of matching
+under context which does not require manipulating a functional term.
+
 If the matching with {\cpattern}$_1$ succeeds, then {\tacexpr}$_1$ is
 evaluated into some value by substituting the pattern matching
 instantiations to the metavariables. If {\tacexpr}$_1$ evaluates to a
-- 
cgit v1.2.3