doc-src/Ref/undocumented.tex
 changeset 3485 f27a30a18a17 parent 327 7f3642193d85 child 4276 a770eae2cdb0
--- a/doc-src/Ref/undocumented.tex	Wed Jul 02 11:59:10 1997 +0200
+++ b/doc-src/Ref/undocumented.tex	Wed Jul 02 16:46:36 1997 +0200
@@ -162,7 +162,7 @@
$$(i, [], \phi_1;\ldots \phi_i\Imp \phi)$$
it returns another triple,
$$(\phi_i, [\phi_{i-1},\ldots, \phi_1], \phi)$$,
-where $\phi$ need not be atomic. Raises an exception if $i$ is out of
+where $\phi$ need not be atomic.  Raises an exception if $i$ is out of
range.

@@ -240,8 +240,8 @@
smash_unifiers: env * (term*term)list -> env seq
\endprog
This unification function maps an environment and a list of disagreement
-pairs to a sequence of updated environments. The function obliterates
-flex-flex pairs by choosing the obvious unifier. It may be used to tidy up
+pairs to a sequence of updated environments.  The function obliterates
+flex-flex pairs by choosing the obvious unifier.  It may be used to tidy up
any flex-flex pairs remaining at the end of a proof.