few bits for coq comparison of patterns

diff --git a/helm/papers/matita/matita2.tex b/helm/papers/matita/matita2.tex
index 8500cfa2c2b76f88e662dfd0c70b8929100360ac..5c56eccf3a83629361c4547efe1483feac55759e 100644 (file)
--- a/helm/papers/matita/matita2.tex
+++ b/helm/papers/matita/matita2.tex
@@ -1467,20 +1467,24 @@ would have resulted in this sequent:
 \end{grafite}
 
 where $H$ is $\beta$-expanded over the second $n$
-occurrence. This is a trick to make the unification algorithm ignore
-the head of the application (since the unification is essentially
-first-order) but normally operate on the arguments. 
-This works for some tactics, like rewrite and replace,
-but for example not for change and other tactics that do not relay on
-unification. 
+occurrence. 
+
+At this point, since Coq unification algorithm is essentially
+first-order, the application of an elimination principle (of the
+form $\forall P.\forall x.(H~x)\to (P~x)$) will unify 
+$x$ with \texttt{n} and $P$ with \texttt{(fun n0 : nat => m + n = n0)}.
+
+Since rewriting, replacing and several other tactics boils down to
+the application of the equality elimination principle, the previous
+trick deals the expected behaviour.
 
 The idea behind this way of identifying subterms in not really far
-from the idea behind patterns, but really fails in extending to
+from the idea behind patterns, but fails in extending to
 complex notation, since it relays on a mono-dimensional sequent representation.
 Real math notation places arguments upside-down (like in indexed sums or
 integrations) or even puts them inside a bidimensional matrix.  
 In these cases using the mouse to select the wanted term is probably the 
-only way to tell the system exactly what you want to do. 
+more effective way to tell the system what to do. 
 
 One of the goals of \MATITA{} is to use modern publishing techniques, and
 adopting a method for restricting tactics application domain that discourages