From fa0b0bedf165812b170cedbce8a5b6cf94a5fadf Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 15 Dec 2015 04:31:01 +0100
Subject: Simplifying documentation of "assert form as pat".

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

diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 18bcd1af62..34b974381a 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -1249,18 +1249,9 @@ in the list of subgoals remaining to prove.
   introduction pattern (in particular, if {\intropattern} is {\ident},
   the tactic behaves like \texttt{assert ({\ident} :\ {\form})}).
 
-  If {\intropattern} is a disjunctive/conjunctive 
-  introduction pattern, the tactic behaves like \texttt{assert
-    {\form}} followed by a {\tt destruct} using this introduction pattern.
-
-  If {\intropattern} is a rewriting intropattern pattern, the tactic
-  behaves like \texttt{assert {\form}} followed by a call to {\tt
-    subst} on the resulting hypothesis, if applicable, or to {\tt
-    rewrite} otherwise.
-
-  If {\intropattern} is an injection intropattern pattern, the tactic
-  behaves like \texttt{assert {\form}} followed by {\tt injection}
-  using this introduction pattern.
+  If {\intropattern} is an action introduction pattern, the tactic
+  behaves like \texttt{assert {\form}} followed by the action done by
+  this introduction pattern.
 
 \item \texttt{assert {\form} as {\intropattern} by {\tac}}
 
-- 
cgit v1.2.3