Updated PR by removing whitespaces. Bug 17450.

1 files changed, 101 insertions, 101 deletions

diff --git a/common/Subtyping.v b/common/Subtyping.v
index e1bf61af..c09226e0 100644
--- a/common/Subtyping.v
+++ b/common/Subtyping.v
@@ -207,7 +207,7 @@ Definition type_move (e: typenv) (r1 r2: positive) : res (bool * typenv) :=
 (** Solve the remaining subtyping constraints by iteration. *)
 
 Fixpoint solve_rec (e: typenv) (changed: bool) (q: list constraint) : res (typenv * bool) :=
-  match q with 
+  match q with
   | nil =>
       OK (e, changed)
   | (r1, r2) :: q' =>
@@ -222,7 +222,7 @@ Definition weight_bounds (ob: option bounds) : nat :=
 Lemma weight_bounds_1:
   forall lo hi s, weight_bounds (Some (B lo hi s)) < weight_bounds None.
 Proof.
-  intros; simpl. generalize (T.weight_range hi); omega. 
+  intros; simpl. generalize (T.weight_range hi); omega.
 Qed.
 
 Lemma weight_bounds_2:
@@ -230,7 +230,7 @@ Lemma weight_bounds_2:
   T.sub lo2 lo1 -> T.sub hi1 hi2 -> lo1 <> lo2 \/ hi1 <> hi2 ->
   weight_bounds (Some (B lo1 hi1 s1)) < weight_bounds (Some (B lo2 hi2 s2)).
 Proof.
-  intros; simpl. 
+  intros; simpl.
   generalize (T.weight_sub _ _ s1) (T.weight_sub _ _ s2) (T.weight_sub _ _ H) (T.weight_sub _ _ H0); intros.
   destruct H1.
   assert (T.weight lo2 < T.weight lo1) by (apply T.weight_sub_strict; auto). omega.
@@ -245,7 +245,7 @@ Lemma weight_type_move:
   (e'.(te_sub) = e.(te_sub) \/ e'.(te_sub) = (r1, r2) :: e.(te_sub))
   /\ (forall r, weight_bounds e'.(te_typ)!r <= weight_bounds e.(te_typ)!r)
   /\ (changed = true ->
-        weight_bounds e'.(te_typ)!r1 + weight_bounds e'.(te_typ)!r2 
+        weight_bounds e'.(te_typ)!r1 + weight_bounds e'.(te_typ)!r2
         < weight_bounds e.(te_typ)!r1 + weight_bounds e.(te_typ)!r2).
 Proof.
   unfold type_move; intros.
@@ -267,22 +267,22 @@ Local Opaque weight_bounds.
 + split; auto. split; intros. omega. discriminate.
 + assert (weight_bounds (Some b1) < weight_bounds (Some (B lo1 hi1 s1)))
   by (apply weight_bounds_2; auto with ty).
-  split; auto. split; intros. 
+  split; auto. split; intros.
   rewrite PTree.gsspec. destruct (peq r r1). subst r. rewrite E1. omega. omega.
-  rewrite PTree.gss. rewrite PTree.gso by auto. rewrite E2. omega. 
+  rewrite PTree.gss. rewrite PTree.gso by auto. rewrite E2. omega.
 + assert (weight_bounds (Some b2) < weight_bounds (Some (B lo2 hi2 s2)))
   by (apply weight_bounds_2; auto with ty).
-  split; auto. split; intros. 
+  split; auto. split; intros.
   rewrite PTree.gsspec. destruct (peq r r2). subst r. rewrite E2. omega. omega.
   rewrite PTree.gss. rewrite PTree.gso by auto. rewrite E1. omega.
 + assert (weight_bounds (Some b1) < weight_bounds (Some (B lo1 hi1 s1)))
   by (apply weight_bounds_2; auto with ty).
   assert (weight_bounds (Some b2) < weight_bounds (Some (B lo2 hi2 s2)))
   by (apply weight_bounds_2; auto with ty).
-  split; auto. split; intros. 
+  split; auto. split; intros.
   rewrite ! PTree.gsspec.
   destruct (peq r r2). subst r. rewrite E2. omega.
-  destruct (peq r r1). subst r. rewrite E1. omega. 
+  destruct (peq r r1). subst r. rewrite E1. omega.
   omega.
   rewrite PTree.gss. rewrite PTree.gso by auto. rewrite PTree.gss. omega.
 
@@ -290,15 +290,15 @@ Local Opaque weight_bounds.
   assert (weight_bounds (Some b2) < weight_bounds None) by (apply weight_bounds_1).
   inv H; simpl.
   split. destruct (T.sub_dec hi1 lo1); auto.
-  split; intros. 
+  split; intros.
   rewrite PTree.gsspec. destruct (peq r r2). subst r; rewrite E2; omega. omega.
-  rewrite PTree.gss. rewrite PTree.gso by auto. rewrite E1. omega. 
+  rewrite PTree.gss. rewrite PTree.gso by auto. rewrite E1. omega.
 
 - set (b1 := B (T.low_bound hi2) hi2 (T.low_bound_sub hi2)) in *.
   assert (weight_bounds (Some b1) < weight_bounds None) by (apply weight_bounds_1).
   inv H; simpl.
   split. destruct (T.sub_dec hi2 lo2); auto.
-  split; intros. 
+  split; intros.
   rewrite PTree.gsspec. destruct (peq r r1). subst r; rewrite E1; omega. omega.
   rewrite PTree.gss. rewrite PTree.gso by auto. rewrite E2. omega.
 
@@ -323,7 +323,7 @@ Lemma weight_solve_rec:
      <= weight_constraints e.(te_typ) e.(te_sub) + weight_constraints e.(te_typ) q.
 Proof.
   induction q; simpl; intros.
-- inv H. split. intros; omega. replace (changed' && negb changed') with false. 
+- inv H. split. intros; omega. replace (changed' && negb changed') with false.
   omega. destruct changed'; auto.
 - destruct a as [r1 r2]; monadInv H; simpl.
   rename x into changed1. rename x0 into e1.
@@ -334,7 +334,7 @@ Proof.
              weight_constraints (te_typ e) (te_sub e))
   by (apply weight_constraints_tighter; auto).
   assert (Q: weight_constraints (te_typ e1) (te_sub e1) <=
-             weight_constraints (te_typ e1) (te_sub e) + 
+             weight_constraints (te_typ e1) (te_sub e) +
              weight_bounds (te_typ e1)!r1 + weight_bounds (te_typ e1)!r2).
   { destruct A as [Q|Q]; rewrite Q. omega. simpl. omega. }
   assert (R: weight_constraints (te_typ e1) q <= weight_constraints (te_typ e) q)
@@ -342,16 +342,16 @@ Proof.
   set (ch1 := if changed' && negb (changed || changed1) then 1 else 0) in *.
   set (ch2 := if changed' && negb changed then 1 else 0) in *.
   destruct changed1.
-  assert (ch2 <= ch1 + 1). 
-  { unfold ch2, ch1. rewrite orb_true_r. simpl. rewrite andb_false_r. 
+  assert (ch2 <= ch1 + 1).
+  { unfold ch2, ch1. rewrite orb_true_r. simpl. rewrite andb_false_r.
     destruct (changed' && negb changed); omega. }
   exploit C; eauto. omega.
   assert (ch2 <= ch1).
   { unfold ch2, ch1. rewrite orb_false_r. omega. }
-  generalize (B r1) (B r2); omega.  
+  generalize (B r1) (B r2); omega.
 Qed.
 
-Definition weight_typenv (e: typenv) : nat := 
+Definition weight_typenv (e: typenv) : nat :=
   weight_constraints e.(te_typ) e.(te_sub).
 
 (** Iterative solving of the remaining constraints *)
@@ -364,7 +364,7 @@ Function solve_constraints (e: typenv) {measure weight_typenv e}: res typenv :=
   end.
 Proof.
   intros. exploit weight_solve_rec; eauto. simpl. intros [A B].
-  unfold weight_typenv. omega. 
+  unfold weight_typenv. omega.
 Qed.
 
 Definition typassign := positive -> T.t.
@@ -383,7 +383,7 @@ Definition satisf (te: typassign) (e: typenv) : Prop :=
 
 Lemma satisf_initial: forall te, satisf te initial.
 Proof.
-  unfold initial; intros; split; simpl; intros. 
+  unfold initial; intros; split; simpl; intros.
   rewrite PTree.gempty in H; discriminate.
   contradiction.
 Qed.
@@ -398,11 +398,11 @@ Proof.
   destruct (T.eq lo (T.lub lo ty)); monadInv H.
   subst e'; auto.
   destruct H0 as [P Q]; split; auto; intros.
-  destruct (peq x x0). 
+  destruct (peq x x0).
   + subst x0. rewrite E in H; inv H.
-    exploit (P x); simpl. rewrite PTree.gss; eauto. intuition. 
-    apply T.sub_trans with (T.lub lo0 ty); auto. eapply T.lub_left; eauto. 
-  + eapply P; simpl. rewrite PTree.gso; eauto. 
+    exploit (P x); simpl. rewrite PTree.gss; eauto. intuition.
+    apply T.sub_trans with (T.lub lo0 ty); auto. eapply T.lub_left; eauto.
+  + eapply P; simpl. rewrite PTree.gso; eauto.
 - inv H. destruct H0 as [P Q]; split; auto; intros.
   eapply P; simpl. rewrite PTree.gso; eauto. congruence.
 Qed.
@@ -416,12 +416,12 @@ Proof.
   destruct (te_typ e)!x as [[lo hi s1]|] eqn:E.
 - destruct (T.sub_dec ty hi); try discriminate.
   destruct (T.eq lo (T.lub lo ty)); monadInv H.
-  + subst e'. apply T.sub_trans with lo. 
+  + subst e'. apply T.sub_trans with lo.
     rewrite e0. eapply T.lub_right; eauto. eapply P; eauto.
-  + apply T.sub_trans with (T.lub lo ty). 
-    eapply T.lub_right; eauto. 
-    eapply (P x). simpl. rewrite PTree.gss; eauto. 
-- inv H. eapply (P x); simpl. rewrite PTree.gss; eauto. 
+  + apply T.sub_trans with (T.lub lo ty).
+    eapply T.lub_right; eauto.
+    eapply (P x). simpl. rewrite PTree.gss; eauto.
+- inv H. eapply (P x); simpl. rewrite PTree.gss; eauto.
 Qed.
 
 Lemma type_defs_incr:
@@ -448,11 +448,11 @@ Proof.
   destruct (T.eq hi (T.glb hi ty)); monadInv H.
   subst e'; auto.
   destruct H0 as [P Q]; split; auto; intros.
-  destruct (peq x x0). 
+  destruct (peq x x0).
   + subst x0. rewrite E in H; inv H.
-    exploit (P x); simpl. rewrite PTree.gss; eauto. intuition. 
-    apply T.sub_trans with (T.glb hi0 ty); auto. eapply T.glb_left; eauto. 
-  + eapply P; simpl. rewrite PTree.gso; eauto. 
+    exploit (P x); simpl. rewrite PTree.gss; eauto. intuition.
+    apply T.sub_trans with (T.glb hi0 ty); auto. eapply T.glb_left; eauto.
+  + eapply P; simpl. rewrite PTree.gso; eauto.
 - inv H. destruct H0 as [P Q]; split; auto; intros.
   eapply P; simpl. rewrite PTree.gso; eauto. congruence.
 Qed.
@@ -466,12 +466,12 @@ Proof.
   destruct (te_typ e)!x as [[lo hi s1]|] eqn:E.
 - destruct (T.sub_dec lo ty); try discriminate.
   destruct (T.eq hi (T.glb hi ty)); monadInv H.
-  + subst e'. apply T.sub_trans with hi. 
-    eapply P; eauto. rewrite e0. eapply T.glb_right; eauto. 
-  + apply T.sub_trans with (T.glb hi ty). 
-    eapply (P x). simpl. rewrite PTree.gss; eauto. 
-    eapply T.glb_right; eauto. 
-- inv H. eapply (P x); simpl. rewrite PTree.gss; eauto. 
+  + subst e'. apply T.sub_trans with hi.
+    eapply P; eauto. rewrite e0. eapply T.glb_right; eauto.
+  + apply T.sub_trans with (T.glb hi ty).
+    eapply (P x). simpl. rewrite PTree.gss; eauto.
+    eapply T.glb_right; eauto.
+- inv H. eapply (P x); simpl. rewrite PTree.gss; eauto.
 Qed.
 
 Lemma type_uses_incr:
@@ -502,27 +502,27 @@ Proof.
   destruct (T.sub_dec lo1 hi2); try discriminate.
   set (lo := T.lub lo1 lo2) in *. set (hi := T.glb hi1 hi2) in *.
   destruct (T.eq lo2 lo); destruct (T.eq hi1 hi); monadInv H; simpl in *.
-  + subst e'; simpl in *. split; auto. 
+  + subst e'; simpl in *. split; auto.
   + subst e'; simpl in *. split; auto. intros. destruct (peq x r1).
-    subst x. 
-    rewrite E1 in H. injection H; intros; subst lo0 hi0. 
-    exploit (P r1). rewrite PTree.gss; eauto. intuition. 
+    subst x.
+    rewrite E1 in H. injection H; intros; subst lo0 hi0.
+    exploit (P r1). rewrite PTree.gss; eauto. intuition.
     apply T.sub_trans with (T.glb hi1 hi2); auto. eapply T.glb_left; eauto.
     eapply P. rewrite PTree.gso; eauto.
   + subst e'; simpl in *. split; auto. intros. destruct (peq x r2).
-    subst x. 
-    rewrite E2 in H. injection H; intros; subst lo0 hi0. 
-    exploit (P r2). rewrite PTree.gss; eauto. intuition. 
+    subst x.
+    rewrite E2 in H. injection H; intros; subst lo0 hi0.
+    exploit (P r2). rewrite PTree.gss; eauto. intuition.
     apply T.sub_trans with (T.lub lo1 lo2); auto. eapply T.lub_right; eauto.
     eapply P. rewrite PTree.gso; eauto.
-  + split; auto. intros. 
-    destruct (peq x r1). subst x. 
-    rewrite E1 in H. injection H; intros; subst lo0 hi0. 
-    exploit (P r1). rewrite PTree.gso; eauto. rewrite PTree.gss; eauto. intuition. 
+  + split; auto. intros.
+    destruct (peq x r1). subst x.
+    rewrite E1 in H. injection H; intros; subst lo0 hi0.
+    exploit (P r1). rewrite PTree.gso; eauto. rewrite PTree.gss; eauto. intuition.
     apply T.sub_trans with (T.glb hi1 hi2); auto. eapply T.glb_left; eauto.
-    destruct (peq x r2). subst x. 
-    rewrite E2 in H. injection H; intros; subst lo0 hi0. 
-    exploit (P r2). rewrite PTree.gss; eauto. intuition. 
+    destruct (peq x r2). subst x.
+    rewrite E2 in H. injection H; intros; subst lo0 hi0.
+    exploit (P r2). rewrite PTree.gss; eauto. intuition.
     apply T.sub_trans with (T.lub lo1 lo2); auto. eapply T.lub_right; eauto.
     eapply P. rewrite ! PTree.gso; eauto.
 - inv H; simpl in *. split; intros.
@@ -531,7 +531,7 @@ Proof.
 - inv H; simpl in *. split; intros.
   eapply P. rewrite PTree.gso; eauto. congruence.
   apply Q.   destruct (T.sub_dec hi2 lo2); auto with coqlib.
-- inv H; simpl in *. split; auto. 
+- inv H; simpl in *. split; auto.
 Qed.
 
 Hint Resolve type_move_incr: ty.
@@ -544,24 +544,24 @@ Proof.
   destruct (peq r1 r2). subst r2. apply T.sub_refl.
   destruct (te_typ e)!r1 as [[lo1 hi1 s1]|] eqn:E1;
   destruct (te_typ e)!r2 as [[lo2 hi2 s2]|] eqn:E2.
-- destruct (T.sub_dec hi1 lo2). 
+- destruct (T.sub_dec hi1 lo2).
   inv H. apply T.sub_trans with hi1. eapply P; eauto. apply T.sub_trans with lo2; auto. eapply P; eauto.
   destruct (T.sub_dec lo1 hi2); try discriminate.
   set (lo := T.lub lo1 lo2) in *. set (hi := T.glb hi1 hi2) in *.
   destruct (T.eq lo2 lo); destruct (T.eq hi1 hi); monadInv H; simpl in *.
   + subst e'; simpl in *. apply Q; auto.
-  + subst e'; simpl in *. apply Q; auto. 
-  + subst e'; simpl in *. apply Q; auto. 
+  + subst e'; simpl in *. apply Q; auto.
+  + subst e'; simpl in *. apply Q; auto.
   + apply Q; auto.
 - inv H; simpl in *. destruct (T.sub_dec hi1 lo1).
-  + apply T.sub_trans with hi1. eapply P; eauto. rewrite PTree.gso; eauto. 
-    apply T.sub_trans with lo1; auto. eapply P. rewrite PTree.gss; eauto. 
+  + apply T.sub_trans with hi1. eapply P; eauto. rewrite PTree.gso; eauto.
+    apply T.sub_trans with lo1; auto. eapply P. rewrite PTree.gss; eauto.
   + auto with coqlib.
 - inv H; simpl in *. destruct (T.sub_dec hi2 lo2).
-  + apply T.sub_trans with hi2. eapply P. rewrite PTree.gss; eauto. 
-    apply T.sub_trans with lo2; auto. eapply P. rewrite PTree.gso; eauto. 
+  + apply T.sub_trans with hi2. eapply P. rewrite PTree.gss; eauto.
+    apply T.sub_trans with lo2; auto. eapply P. rewrite PTree.gso; eauto.
   + auto with coqlib.
-- inv H. simpl in Q; auto. 
+- inv H. simpl in Q; auto.
 Qed.
 
 Lemma solve_rec_incr:
@@ -575,12 +575,12 @@ Qed.
 
 Lemma solve_rec_sound:
   forall te r1 r2 q e changed e' changed',
-  solve_rec e changed q = OK(e', changed') -> In (r1, r2) q -> satisf te e' -> 
+  solve_rec e changed q = OK(e', changed') -> In (r1, r2) q -> satisf te e' ->
   T.sub (te r1) (te r2).
 Proof.
   induction q; simpl; intros.
 - contradiction.
-- destruct a as [r3 r4]; monadInv H. destruct H0. 
+- destruct a as [r3 r4]; monadInv H. destruct H0.
   + inv H. eapply type_move_sound; eauto. eapply solve_rec_incr; eauto.
   + eapply IHq; eauto with ty.
 Qed.
@@ -590,12 +590,12 @@ Lemma type_move_false:
   type_move e r1 r2 = OK(false, e') ->
   te_typ e' = te_typ e /\ T.sub (makeassign e r1) (makeassign e r2).
 Proof.
-  unfold type_move; intros. 
+  unfold type_move; intros.
   destruct (peq r1 r2). inv H. split; auto. apply T.sub_refl.
   unfold makeassign;
   destruct (te_typ e)!r1 as [[lo1 hi1 s1]|] eqn:E1;
   destruct (te_typ e)!r2 as [[lo2 hi2 s2]|] eqn:E2.
-- destruct (T.sub_dec hi1 lo2). 
+- destruct (T.sub_dec hi1 lo2).
   inv H. split; auto. eapply T.sub_trans; eauto.
   destruct (T.sub_dec lo1 hi2); try discriminate.
   set (lo := T.lub lo1 lo2) in *. set (hi := T.glb hi1 hi2) in *.
@@ -609,17 +609,17 @@ Qed.
 Lemma solve_rec_false:
   forall r1 r2 q e changed e',
   solve_rec e changed q = OK(e', false) ->
-  changed = false /\ 
+  changed = false /\
   (In (r1, r2) q -> T.sub (makeassign e r1) (makeassign e r2)).
 Proof.
   induction q; simpl; intros.
-- inv H. tauto. 
+- inv H. tauto.
 - destruct a as [r3 r4]; monadInv H.
   exploit IHq; eauto. intros [P Q].
   destruct changed; try discriminate. destruct x; try discriminate.
   exploit type_move_false; eauto. intros [U V].
-  split. auto. intros [A|A]. inv A. auto. exploit Q; auto. 
-  unfold makeassign; rewrite U; auto.    
+  split. auto. intros [A|A]. inv A. auto. exploit Q; auto.
+  unfold makeassign; rewrite U; auto.
 Qed.
 
 Lemma solve_constraints_incr:
@@ -638,7 +638,7 @@ Proof.
   intros e0; functional induction (solve_constraints e0); intros.
 - inv H. split; intros.
   unfold makeassign; rewrite H. split; auto with ty.
-  exploit solve_rec_false. eauto. intros [A B]. eapply B; eauto. 
+  exploit solve_rec_false. eauto. intros [A B]. eapply B; eauto.
 - eauto.
 - discriminate.
 Qed.
@@ -646,7 +646,7 @@ Qed.
 Theorem solve_sound:
   forall e te, solve e = OK te -> satisf te e.
 Proof.
-  unfold solve; intros. monadInv H. 
+  unfold solve; intros. monadInv H.
   eapply solve_constraints_incr. eauto. eapply solve_constraints_sound; eauto.
 Qed.
 
@@ -657,17 +657,17 @@ Lemma type_def_complete:
   satisf te e -> T.sub ty (te x) -> exists e', type_def e x ty = OK e' /\ satisf te e'.
 Proof.
   unfold type_def; intros. destruct H as [P Q].
-  destruct (te_typ e)!x as [[lo hi s1]|] eqn:E. 
-- destruct (T.sub_dec ty hi). 
+  destruct (te_typ e)!x as [[lo hi s1]|] eqn:E.
+- destruct (T.sub_dec ty hi).
   destruct (T.eq lo (T.lub lo ty)).
   exists e; split; auto. split; auto.
-  econstructor; split; eauto. split; simpl; auto; intros. 
-  rewrite PTree.gsspec in H. destruct (peq x0 x). 
-  inv H. exploit P; eauto. intuition. eapply T.lub_min; eauto. 
+  econstructor; split; eauto. split; simpl; auto; intros.
+  rewrite PTree.gsspec in H. destruct (peq x0 x).
+  inv H. exploit P; eauto. intuition. eapply T.lub_min; eauto.
   eapply P; eauto.
   elim n. apply T.sub_trans with (te x); auto. eapply P; eauto.
 - econstructor; split; eauto. split; simpl; auto; intros.
-  rewrite PTree.gsspec in H. destruct (peq x0 x). 
+  rewrite PTree.gsspec in H. destruct (peq x0 x).
   inv H. split; auto. apply T.high_bound_majorant; auto.
   eapply P; eauto.
 Qed.
@@ -689,17 +689,17 @@ Lemma type_use_complete:
   satisf te e -> T.sub (te x) ty -> exists e', type_use e x ty = OK e' /\ satisf te e'.
 Proof.
   unfold type_use; intros. destruct H as [P Q].
-  destruct (te_typ e)!x as [[lo hi s1]|] eqn:E. 
-- destruct (T.sub_dec lo ty). 
+  destruct (te_typ e)!x as [[lo hi s1]|] eqn:E.
+- destruct (T.sub_dec lo ty).
   destruct (T.eq hi (T.glb hi ty)).
   exists e; split; auto. split; auto.
-  econstructor; split; eauto. split; simpl; auto; intros. 
-  rewrite PTree.gsspec in H. destruct (peq x0 x). 
-  inv H. exploit P; eauto. intuition. eapply T.glb_max; eauto. 
+  econstructor; split; eauto. split; simpl; auto; intros.
+  rewrite PTree.gsspec in H. destruct (peq x0 x).
+  inv H. exploit P; eauto. intuition. eapply T.glb_max; eauto.
   eapply P; eauto.
   elim n. apply T.sub_trans with (te x); auto. eapply P; eauto.
 - econstructor; split; eauto. split; simpl; auto; intros.
-  rewrite PTree.gsspec in H. destruct (peq x0 x). 
+  rewrite PTree.gsspec in H. destruct (peq x0 x).
   inv H. split; auto. apply T.low_bound_minorant; auto.
   eapply P; eauto.
 Qed.
@@ -730,15 +730,15 @@ Proof.
 - exploit (P r1); eauto. intros [L1 U1].
   exploit (P r2); eauto. intros [L2 U2].
   destruct (T.sub_dec hi1 lo2). econstructor; econstructor; eauto.
-  destruct (T.sub_dec lo1 hi2). 
+  destruct (T.sub_dec lo1 hi2).
   destruct (T.eq lo2 (T.lub lo1 lo2)); destruct (T.eq hi1 (T.glb hi1 hi2));
   econstructor; econstructor; split; eauto; split; auto; simpl; intros.
-  + rewrite PTree.gsspec in H1. destruct (peq x r1). 
-    clear e0. inv H1. split; auto.  
+  + rewrite PTree.gsspec in H1. destruct (peq x r1).
+    clear e0. inv H1. split; auto.
     apply T.glb_max. auto. apply T.sub_trans with (te r2); auto.
     eapply P; eauto.
-  + rewrite PTree.gsspec in H1. destruct (peq x r2). 
-    clear e0. inv H1. split; auto.  
+  + rewrite PTree.gsspec in H1. destruct (peq x r2).
+    clear e0. inv H1. split; auto.
     apply T.lub_min. apply T.sub_trans with (te r1); auto. auto.
     eapply P; eauto.
   + rewrite ! PTree.gsspec in H1. destruct (peq x r2).
@@ -746,18 +746,18 @@ Proof.
     destruct (peq x r1).
     inv H1. split; auto. apply T.glb_max; auto. apply T.sub_trans with (te r2); auto.
     eapply P; eauto.
-  + elim n1. apply T.sub_trans with (te r1); auto. 
-    apply T.sub_trans with (te r2); auto. 
+  + elim n1. apply T.sub_trans with (te r1); auto.
+    apply T.sub_trans with (te r2); auto.
 - econstructor; econstructor; split; eauto; split.
   + simpl; intros. rewrite PTree.gsspec in H1. destruct (peq x r2).
-    inv H1. exploit P; eauto. intuition. 
+    inv H1. exploit P; eauto. intuition.
     apply T.sub_trans with (te r1); auto.
     apply T.high_bound_majorant. apply T.sub_trans with (te r1); auto.
     eapply P; eauto.
   + destruct (T.sub_dec hi1 lo1); auto.
 - econstructor; econstructor; split; eauto; split.
   + simpl; intros. rewrite PTree.gsspec in H1. destruct (peq x r1).
-    inv H1. exploit P; eauto. intuition. 
+    inv H1. exploit P; eauto. intuition.
     apply T.low_bound_minorant. apply T.sub_trans with (te r2); auto.
     apply T.sub_trans with (te r2); auto.
     eapply P; eauto.
@@ -773,7 +773,7 @@ Lemma solve_rec_complete:
 Proof.
   induction q; simpl; intros.
 - econstructor; econstructor; eauto.
-- destruct a as [r1 r2]. 
+- destruct a as [r1 r2].
   exploit (type_move_complete te e r1 r2); auto. intros (changed1 & e1 & A & B).
   exploit (IHq e1 (changed || changed1)); auto. intros (e' & changed' & C & D).
   exists e'; exists changed'. rewrite A; simpl; rewrite C; auto.
@@ -782,26 +782,26 @@ Qed.
 Lemma solve_constraints_complete:
   forall te e, satisf te e -> exists e', solve_constraints e = OK e' /\ satisf te e'.
 Proof.
-  intros te e. functional induction (solve_constraints e); intros. 
+  intros te e. functional induction (solve_constraints e); intros.
 - exists e; auto.
 - exploit (solve_rec_complete te (te_sub e) {| te_typ := te_typ e; te_sub := nil |} false).
   destruct H; split; auto. simpl; tauto.
   destruct H; auto.
-  intros (e1 & changed1 & P & Q). 
-  apply IHr. congruence. 
+  intros (e1 & changed1 & P & Q).
+  apply IHr. congruence.
 - exploit (solve_rec_complete te (te_sub e) {| te_typ := te_typ e; te_sub := nil |} false).
   destruct H; split; auto. simpl; tauto.
   destruct H; auto.
-  intros (e1 & changed1 & P & Q). 
+  intros (e1 & changed1 & P & Q).
   congruence.
 Qed.
 
 Lemma solve_complete:
   forall te e, satisf te e -> exists te', solve e = OK te'.
 Proof.
-  intros. unfold solve. 
-  destruct (solve_constraints_complete te e H) as (e' & P & Q). 
-  econstructor. rewrite P. simpl. eauto. 
+  intros. unfold solve.
+  destruct (solve_constraints_complete te e H) as (e' & P & Q).
+  econstructor. rewrite P. simpl. eauto.
 Qed.
 
 End SubSolver.