[commit: ghc] master: Comments only (43a5970)

[git at git.haskell.org]

Repository : ssh://git@git.haskell.org/ghc

On branch  : master
Link       : http://ghc.haskell.org/trac/ghc/changeset/43a5970a4f721138145f55e90bd910f3723abc3c/ghc

>---------------------------------------------------------------

commit 43a5970a4f721138145f55e90bd910f3723abc3c
Author: Simon Peyton Jones <simonpj at microsoft.com>
Date:   Fri Dec 4 12:24:49 2015 +0000

    Comments only


>---------------------------------------------------------------

43a5970a4f721138145f55e90bd910f3723abc3c
 compiler/typecheck/TcSMonad.hs | 13 +++++--------
 1 file changed, 5 insertions(+), 8 deletions(-)

diff --git a/compiler/typecheck/TcSMonad.hs b/compiler/typecheck/TcSMonad.hs
index 8ddb488..0c5564b 100644
--- a/compiler/typecheck/TcSMonad.hs
+++ b/compiler/typecheck/TcSMonad.hs
@@ -662,8 +662,8 @@ Definition [Can-rewrite relation]
 A "can-rewrite" relation between flavours, written f1 >= f2, is a
 binary relation with the following properties
 
-  R1.  >= is transitive
-  R2.  If f1 >= f, and f2 >= f,
+  (R1) >= is transitive
+  (R2) If f1 >= f, and f2 >= f,
        then either f1 >= f2 or f2 >= f1
 
 Lemma.  If f1 >= f then f1 >= f1
@@ -690,7 +690,7 @@ See Note [Flavours with roles].
 Theorem: S(f,a) is well defined as a function.
 Proof: Suppose (a -f1-> t1) and (a -f2-> t2) are both in S,
                and  f1 >= f and f2 >= f
-       Then by (R2) f1 >= f2 or f2 >= f1, which contradicts (WF)
+       Then by (R2) f1 >= f2 or f2 >= f1, which contradicts (WF1)
 
 Notation: repeated application.
   S^0(f,t)     = t
@@ -702,9 +702,6 @@ A generalised substitution S is "inert" iff
   (IG1) there is an n such that
         for every f,t, S^n(f,t) = S^(n+1)(f,t)
 
-  (IG2) if (b -f-> t) in S, and f >= f, then S(f,t) = t
-        that is, each individual binding is "self-stable"
-
 By (IG1) we define S*(f,t) to be the result of exahaustively
 applying S(f,_) to t.
 
@@ -719,8 +716,8 @@ guarantee that this recursive use will terminate.
 
 Note [Extending the inert equalities]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-This is the main theorem!
-
+Theorem [Stability under extension]
+   This is the main theorem!
    Suppose we have a "work item"
        a -fw-> t
    and an inert generalised substitution S,