diff --git a/lib/coq/CFApp.v b/lib/coq/CFApp.v
index 3f7e67402aa16d791021de8ea6e4963622771ea6..5f85c87a7eceacc4668af5318a721fe05d18cc74 100644
--- a/lib/coq/CFApp.v
+++ b/lib/coq/CFApp.v
@@ -210,7 +210,7 @@ Qed.
 Lemma app_wgframe : forall B f xs H H1 H2 (Q1 Q:B->hprop),
   app f xs H1 Q1 ->
   H ==> (H1 \* H2) ->
-  (Q1 \*+ H2) ===> (Q \*+ (Hexists H', H')) ->
+  (Q1 \*+ H2) ===> (Q \*+ \GC) ->
   app f xs H Q.
 Proof using.
   intros B f xs. gen f. induction xs as [|[A x] xs]; introv M WH WQ. false.
@@ -223,10 +223,11 @@ Qed.
 
 Lemma app_weaken : forall B f xs H (Q Q':B->hprop),
   app f xs H Q ->
-  Q ===> Q' -> 
-  app f xs H Q'.  
-Proof using.   
-  introv M W. applys* app_wgframe. hsimpl. intros r. hsimpl~ \[].
+  Q ===> Q' ->
+  app f xs H Q'.
+Proof using.
+  introv M W. applys* app_wgframe. hsimpl. intros r.
+  hchange W. hsimpl.
 Qed.
 
 (* DEPRECATED
diff --git a/lib/coq/CFHeaps.v b/lib/coq/CFHeaps.v
index e98a9e11e1eca110fe2e763f527ae4bd0e212cb7..dbcbb4dcf32ee856d810d4ede69718e82320e783 100644
--- a/lib/coq/CFHeaps.v
+++ b/lib/coq/CFHeaps.v
@@ -275,17 +275,25 @@ Tactic Notation "rew_disjoint" "*" :=
 
 (** Representation of credits *)
 
-Definition credits_type : Type := nat.
+Definition credits_type : Type := int.
 
 (** Zero and one credits *)
 
-Definition credits_zero : credits_type := 0%nat.
-Definition credits_one : credits_type := 1%nat.
+Definition credits_zero : credits_type := 0.
+Definition credits_one : credits_type := 1.
 
 (** Representation of heaps *)
 
 Definition heap : Type := (state * credits_type)%type.
 
+(** Projections *)
+
+Definition heap_state (h:heap) : state :=
+  match h with (m,_) => m end.
+
+Definition heap_credits (h:heap) : credits_type :=
+  match h with (_,c) => c end.
+
 (** Predicate over pairs *)
 
 Definition prod_st A B (v:A*B) (P:A->Prop) (Q:B->Prop) := (* todo move to TLC *)
@@ -312,7 +320,7 @@ Notation "\# h1 h2" := (heap_disjoint h1 h2)
 (** Union of heaps *)
 
 Definition heap_union (h1 h2 : heap) : heap :=
-  prod_func state_union (fun a b => (a + b)%nat) h1 h2.
+  prod_func state_union (fun a b => (a + b)) h1 h2.
 
 Notation "h1 \+ h2" := (heap_union h1 h2)
    (at level 51, right associativity).
@@ -320,8 +328,12 @@ Notation "h1 \+ h2" := (heap_union h1 h2)
 (** Empty heap *)
 
 Definition heap_empty : heap :=
-  (state_empty, 0%nat).
+  (state_empty, 0).
 
+(** Affine heaps *)
+
+Definition heap_affine (h: heap) : Prop :=
+  0 <= heap_credits h.
 
 (*------------------------------------------------------------------*)
 (* ** Properties on heaps *)
@@ -411,6 +423,31 @@ Proof using.
   fequals. applys state_union_assoc. math.
 Qed.
 
+(** Affine *)
+
+Lemma heap_affine_empty :
+  heap_affine heap_empty.
+Proof.
+  unfold heap_affine, heap_empty. simpl.
+  math.
+Qed.
+
+Lemma heap_affine_union : forall h1 h2,
+  heap_affine h1 ->
+  heap_affine h2 ->
+  heap_affine (h1 \+ h2).
+Proof.
+  intros (m1 & c1) (m2 & c2) HA1 HA2.
+  unfold heap_affine, heap_union, prod_func in *. simpl in *.
+  math.
+Qed.
+
+Lemma heap_affine_credits : forall c,
+  0 <= c ->
+  heap_affine (state_empty, c).
+Proof. auto. Qed.
+
+
 (** Hints and tactics *)
 
 Hint Resolve heap_union_neutral_l heap_union_neutral_r.
@@ -455,6 +492,11 @@ Definition heap_is_star (H1 H2 : hprop) : hprop :=
                       /\ heap_disjoint h1 h2
                       /\ h = heap_union h1 h2.
 
+(** Affine heap predicates *)
+
+Definition affine (H : hprop) : Prop :=
+  forall h, H h -> heap_affine h.
+
 (** Lifting of existentials *)
 
 Definition heap_is_pack A (Hof : A -> hprop) : hprop :=
@@ -465,21 +507,18 @@ Definition heap_is_pack A (Hof : A -> hprop) : hprop :=
 Definition heap_is_empty_st (H:Prop) : hprop :=
   fun h => h = heap_empty /\ H.
 
-(** Garbage collection predicate: [Hexists H, H]. *)
+(** Garbage collection predicate: equivalent to [Hexists H, H \* \[affine H]]. *)
 
 Definition heap_is_gc : hprop :=
-  heap_is_pack (fun H => H).
+  fun h => heap_affine h /\ exists H, H h.
 
 (** Credits *)
 
-Definition heap_is_credits_nat (n:nat) : hprop :=
-  fun h => let (m,n') := h in m = state_empty /\ n' = n.
-
-Definition heap_is_credits_int (x:int) : hprop :=
-  heap_is_star (heap_is_credits_nat (abs x)) (heap_is_empty_st (x >= 0)%I).
+Definition heap_is_credits (x:int) : hprop :=
+  fun h => let (m,x') := h in m = state_empty /\ x' = x.
 
 Opaque heap_union state_single heap_is_star heap_is_pack
-  heap_is_credits_nat heap_is_credits_int.
+  heap_is_gc heap_is_credits heap_affine affine.
 
 (** Hprop is inhabited *)
 
@@ -505,10 +544,7 @@ Notation "H1 '\*' H2" := (heap_is_star H1 H2)
 
 Notation "\GC" := (heap_is_gc) : heap_scope.
 
-Notation "'\$_nat' n" := (heap_is_credits_nat n)
-  (at level 40, format "\$_nat  n") : heap_scope.
-
-Notation "'\$' x" := (heap_is_credits_int x)
+Notation "'\$' x" := (heap_is_credits x)
   (at level 40, format "\$ x") : heap_scope.
 
 Notation "'Hexists' x1 , H" := (heap_is_pack (fun x1 => H))
@@ -781,24 +817,24 @@ Tactic Notation "rew_heap" "*" "in" hyp(H) :=
 (* ** Properties of heap credits *)
 
 Section Credits.
-Transparent heap_is_credits_nat heap_is_credits_int
+Transparent heap_is_credits
   heap_is_empty heap_is_empty_st heap_is_star heap_union heap_disjoint.
 
 Definition pay_one H H' :=
-  H ==> \$ 1%I \* H'.
+  H ==> \$ 1 \* H'.
 
-Lemma credits_nat_zero_eq : \$_nat 0 = \[].
+Lemma credits_zero_eq : \$ 0 = \[].
 Proof using.
-  unfold heap_is_credits_nat, heap_is_empty, heap_empty.
+  unfold heap_is_credits, heap_is_empty, heap_empty.
   applys pred_ext_1. intros [m n]. iff [M1 M2] M.  (* todo: extens should work *)
     subst*.
     inverts* M.
 Qed.
 
-Lemma credits_nat_split_eq : forall (n m : nat),
-  \$_nat (n+m) = \$_nat n \* \$_nat m.
+Lemma credits_split_eq : forall (n m : int),
+  \$ (n+m) = \$ n \* \$ m.
 Proof using.
-  intros c1 c2. unfold heap_is_credits_nat, heap_is_star, heap_union, heap_disjoint.
+  intros c1 c2. unfold heap_is_credits, heap_is_star, heap_union, heap_disjoint.
   applys pred_ext_1. intros [m n]. (* todo: extens should work *)
   iff [M1 M2] ([m1 n1]&[m2 n2]&(M1&E1)&(M2&E2)&M3&M4).
     exists (state_empty,c1) (state_empty,c2). simpl. splits*.
@@ -807,60 +843,39 @@ Proof using.
     inverts M4. subst*.
 Qed.
 
-Lemma credits_nat_le : forall (n m : nat),
-  (n >= m)%nat -> \$_nat n ==> \$_nat m \* \$_nat (n-m).
-Proof using.
-  introv M. rewrite <- credits_nat_split_eq.
-  math_rewrite (m + (n-m) = n)%nat. auto.
-Qed.
-
-Lemma credits_nat_le_rest : forall (n m : nat), (* todo: move later, inverse hyp *)
-  (n <= m)%nat -> exists H', \$_nat m ==> \$_nat n \* H'.
-Proof using.
-  introv M. exists (\$_nat (m - n)). rewrite <- credits_nat_split_eq.
-  math_rewrite (n + (m-n) = m)%nat. auto.
-Qed.
-
-Lemma credits_int_zero_eq : \$ 0%I = \[].
+Lemma credits_le_rest : forall (n m : int), (* todo: move later, inverse hyp *)
+  n <= m -> exists H', affine H' /\ \$ m ==> \$ n \* H'.
 Proof using.
-  unfold heap_is_credits_int. change (abs 0) with (0%nat).
-  rewrite credits_nat_zero_eq. (* hsimpl would prove the goal here *)
-  unfold heap_is_star, heap_is_empty, heap_is_empty_st.
-  applys pred_ext_1. iff (h1&h2&H1&(H2&E)&D&U) E.
-    subst. autos* state_disjoint_empty_l.
-    subst. exists heap_empty heap_empty. splits~. splits~. math.
+  introv M. exists (\$ (m - n)). rewrite <- credits_split_eq.
+  math_rewrite (n + (m-n) = m).
+  splits~.
+  Local Transparent affine. unfold affine, heap_is_credits.
+  intros (? & ?) (? & ?); subst. apply heap_affine_credits.
+  math.
 Qed.
 
-Lemma credits_int_split_eq : forall (x y : int),
-  (x >= 0) -> (y >= 0) ->
-  \$(x+y) = \$ x \* \$ y.
+Lemma credits_join_eq : forall x y,
+  \$ x \* \$ y = \$(x+y).
 Proof using.
-  introv Px Py. unfold heap_is_credits_int. rew_heap.
-  rewrite (star_comm \[x >= 0]). rew_heap.
-  rewrite star_assoc. rewrite <- credits_nat_split_eq.
-  rewrite~ abs_plus. (* hsimpl would prove the goal here *)
-  unfold heap_is_star, heap_is_empty_st.
-  applys pred_ext_1. iff (h1&h2&H1&(H2&E)&D&U).
-    subst. exists h1 heap_empty. splits~. exists heap_empty heap_empty. splits~.
-    subst. destruct E as (h3&(E3&P3)&(E4&P4)&D'&U').
-      subst. exists h1 heap_empty. splits~. splits~. math. fequal.
-      autos* state_disjoint_empty_r.
-Qed.
+  introv. unfold heap_is_credits.
+  applys pred_ext_1. intros h. splits.
+  { intros ([m1 c1] & [m2 c2] & ([? ?] & [? ?] & [[? ?] ?])).
+    subst. unfold heap_union. simpl.
+    rewrite state_union_neutral_r. splits~. }
+  { destruct h as [m c]. intros (? & ?). subst.
+    unfold heap_is_star.
+    exists (state_empty, x) (state_empty, y).
+    splits~.
+    { unfold heap_disjoint. simpl.
+      splits~. apply state_disjoint_empty_l. }
+    { unfold heap_union. simpl.
+      rewrite~ state_union_neutral_r. } }
+ Qed.
 
-Lemma credits_int_le : forall (x y : int),
-  (x >= y)%I -> (y >= 0)%I -> \$ x ==> \$ y \* \$ (x-y).
+Lemma credits_join_eq_rest : forall x y (H:hprop),
+  \$ x \* \$ y \* H = \$(x+y) \* H.
 Proof using.
-  introv M N. unfold heap_is_credits_int. rew_heap.
-  unfold heap_is_star, heap_is_empty_st.
-  intros h (h1&h2&H1&(H2&E)&D&U). destruct h1 as [c1 n1].
-  destruct H1 as [C1 N1]. subst.
-  exists (state_empty,abs y). exists (state_empty,abs (x-y)).
-  splits~. constructors~. exists heap_empty.
-  exists (state_empty,abs (x-y)). splits~.
-  esplit. esplit. splits~. constructors~. splits~. math.
-  simpl. fequals. rewrite~ <- abs_plus. rewrite LibNat.plus_zero_r.
-  fequals. math.
-  math.
+  introv. rewrite star_assoc. rewrite~ credits_join_eq.
 Qed.
 
 End Credits.
@@ -871,7 +886,7 @@ End Credits.
 
 (** Tactic [credits_split] converts [\$(x+y) \* ...] into [\$x \* \$y \* ...] *)
 
-Hint Rewrite credits_int_split_eq credits_nat_split_eq : credits_split_rew.
+Hint Rewrite credits_split_eq : credits_split_rew.
 
 Ltac credits_split :=
   autorewrite with credits_split_rew.
@@ -882,38 +897,11 @@ Lemma credits_swap : forall x (H:hprop),
   H \* (\$ x) = (\$ x) \* H.
 Proof using. intros. rewrite~ star_comm. Qed.
 
-(* need additional nonnegativity hypotheses
-
-Lemma credits_join_eq : forall x y,
-  \$ x \* \$ y = \$(x+y).
-Proof using. .... Qed.
-
-Lemma credits_join_eq_rest : forall x y (H:hprop),
-  \$ x \* \$ y \* H = \$(x+y) \* H.
-Proof using. ..... Qed.
-
-*)
-
-(* TODO: above should be rewritten with pre-condition x>=0 and y>=0
-   which can be extracted from left-hand-side *)
-
-Lemma credits_nat_join_eq : forall x y,
-  \$_nat x \* \$_nat y = \$_nat(x+y).
-Proof using. intros. rewrite~ credits_nat_split_eq. Qed.
-
-Lemma credits_nat_join_eq_rest : forall x y (H:hprop),
-  \$_nat x \* \$_nat y \* H = \$_nat(x+y) \* H.
-Proof using. intros. rewrite~ credits_nat_split_eq. rewrite~ star_assoc. Qed.
-
 
 Ltac credits_join_in H :=
   match H with
-  | \$_nat ?x \* \$_nat ?y => rewrite (@credits_nat_join_eq x y)
-  | \$_nat ?x \* \$_nat ?y \* ?H' => rewrite (@credits_nat_join_eq_rest x y H')
-(* TODO: activate these once lemmas are proved
   | \$ ?x \* \$ ?y => rewrite (@credits_join_eq x y)
   | \$ ?x \* \$ ?y \* ?H' => rewrite (@credits_join_eq_rest x y H')
-*)
   | _ \* ?H' => credits_join_in H'
   end.
 
@@ -1037,6 +1025,70 @@ Definition Group a A (G:htype A a) (M:map a A) :=
   \* \[LibMap.finite M].
 
 
+(*------------------------------------------------------------------*)
+(* ** Properties of [affine] *)
+
+Section Affine.
+Transparent affine.
+
+Lemma affine_empty :
+  affine \[].
+Proof.
+  unfold affine, heap_is_empty. intros; subst.
+  apply heap_affine_empty.
+Qed.
+
+Lemma affine_star : forall H1 H2,
+  affine H1 ->
+  affine H2 ->
+  affine (H1 \* H2).
+Proof.
+  Transparent heap_is_star.
+  introv HA1 HA2. unfold affine, heap_is_star in *.
+  intros h (? & ? & ? & ? & ? & ?). subst.
+  apply~ heap_affine_union.
+Qed.
+
+Lemma affine_credits : forall c,
+  0 <= c ->
+  affine (\$ c).
+Proof.
+  Transparent heap_is_credits.
+  introv N. unfold affine, heap_is_credits.
+  intros (m & c'). intros (? & ?). subst.
+  apply~ heap_affine_credits.
+Qed.
+
+Lemma affine_empty_st : forall P,
+  affine \[P].
+Proof.
+  Transparent heap_is_empty_st.
+  introv. unfold affine, heap_is_empty_st.
+  introv (? & ?); subst.
+  apply heap_affine_empty.
+Qed.
+
+Lemma affine_gc :
+  affine \GC.
+Proof.
+  Transparent heap_is_gc.
+  unfold affine, heap_is_gc.
+  tauto.
+Qed.
+
+(* affine_hdata? *)
+
+End Affine.
+
+Hint Resolve
+     affine_empty affine_star affine_credits affine_empty_st
+     affine_gc
+: affine.
+
+Ltac affine :=
+  match goal with |- affine _ => eauto with affine zarith end.
+
+
 (********************************************************************)
 (* ** [xunfold] tactics *)
 
@@ -1551,8 +1603,14 @@ Proof using.
 Qed.
 
 Lemma hsimpl_gc : forall H,
+  affine H ->
   H ==> \GC.
-Proof using. intros. unfold heap_is_gc. introv M. exists~ H. Qed.
+Proof using.
+  Local Transparent affine heap_is_gc.
+  introv HA. unfold heap_is_gc, pred_incl.
+  intros h Hh. unfold affine in HA.
+  splits~. eauto.
+Qed.
 
 Lemma hsimpl_cancel_1 : forall H HA HR HT,
   HT ==> HA \* HR -> H \* HT ==> HA \* (H \* HR).
@@ -1603,128 +1661,61 @@ Lemma hsimpl_cancel_10 : forall H HA HR H1 H2 H3 H4 H5 H6 H7 H8 H9 HT,
 Proof using. intros. rewrite (star_comm_assoc H9). apply~ hsimpl_cancel_9. Qed.
 
 
-Lemma hsimpl_cancel_credits_nat_1 : forall (n m : nat) HA HR HT,
-  (n >= m)%nat ->
-  \$_nat (n - m) \* HT ==> HA \* HR ->
-  \$_nat n \* HT ==> HA \* (\$_nat m \* HR).
+Lemma hsimpl_cancel_credits_1 : forall (n m : int) HA HR HT,
+  \$ (n - m) \* HT ==> HA \* HR ->
+  \$ n \* HT ==> HA \* (\$ m \* HR).
 Proof using.
-  introv L E. math_rewrite (n = (n - m) + m)%nat.
-  rewrite credits_nat_split_eq. rewrite <- star_assoc.
+  introv E. math_rewrite (n = (n - m) + m).
+  rewrite credits_split_eq. rewrite <- star_assoc.
   applys~ hsimpl_cancel_2.
 Qed.
 
-Lemma hsimpl_cancel_credits_nat_2 : forall (n m : nat) HA HR H1 HT,
-  (n >= m)%nat -> \$_nat (n - m) \* H1 \* HT ==> HA \* HR ->
-  H1 \* \$_nat n \* HT ==> HA \* (\$_nat m \* HR).
-Proof using.
-  intros. rewrite (star_comm_assoc H1). apply~ hsimpl_cancel_credits_nat_1.
-Qed.
-
-Lemma hsimpl_cancel_credits_nat_3 : forall (n m : nat) HA HR H1 H2 HT,
-  (n >= m)%nat -> \$_nat (n - m) \* H1 \* H2 \* HT ==> HA \* HR ->
-  H1 \* H2 \* \$_nat n \* HT ==> HA \* (\$_nat m \* HR).
-Proof using. intros. rewrite (star_comm_assoc H2). apply~ hsimpl_cancel_credits_nat_2. Qed.
-
-Lemma hsimpl_cancel_credits_nat_4 : forall (n m : nat) HA HR H1 H2 H3 HT,
-  (n >= m)%nat -> \$_nat (n - m) \* H1 \* H2 \* H3 \* HT ==> HA \* HR ->
-  H1 \* H2 \* H3 \* \$_nat n \* HT ==> HA \* (\$_nat m \* HR).
-Proof using. intros. rewrite (star_comm_assoc H3). apply~ hsimpl_cancel_credits_nat_3. Qed.
-
-Lemma hsimpl_cancel_credits_nat_5 : forall (n m : nat) HA HR H1 H2 H3 H4 HT,
-  (n >= m)%nat -> \$_nat (n - m) \* H1 \* H2 \* H3 \* H4 \* HT ==> HA \* HR ->
-  H1 \* H2 \* H3 \* H4 \* \$_nat n \* HT ==> HA \* (\$_nat m \* HR).
-Proof using. intros. rewrite (star_comm_assoc H4). apply~ hsimpl_cancel_credits_nat_4. Qed.
-
-Lemma hsimpl_cancel_credits_nat_6 : forall (n m : nat) HA HR H1 H2 H3 H4 H5 HT,
-  (n >= m)%nat -> \$_nat (n - m) \* H1 \* H2 \* H3 \* H4 \* H5 \* HT ==> HA \* HR ->
-  H1 \* H2 \* H3 \* H4 \* H5 \* \$_nat n \* HT ==> HA \* (\$_nat m \* HR).
-Proof using. intros. rewrite (star_comm_assoc H5). apply~ hsimpl_cancel_credits_nat_5. Qed.
-
-Lemma hsimpl_cancel_credits_nat_7 : forall (n m : nat) HA HR H1 H2 H3 H4 H5 H6 HT,
-  (n >= m)%nat -> \$_nat (n - m) \* H1 \* H2 \* H3 \* H4 \* H5 \* H6 \* HT ==> HA \* HR ->
-  H1 \* H2 \* H3 \* H4 \* H5 \* H6 \* \$_nat n \* HT ==> HA \* (\$_nat m \* HR).
-Proof using. intros. rewrite (star_comm_assoc H6). apply~ hsimpl_cancel_credits_nat_6. Qed.
-
-Lemma hsimpl_cancel_credits_nat_8 : forall (n m : nat) HA HR H1 H2 H3 H4 H5 H6 H7 HT,
-  (n >= m)%nat -> \$_nat (n - m) \* H1 \* H2 \* H3 \* H4 \* H5 \* H6 \* H7 \* HT ==> HA \* HR ->
-  H1 \* H2 \* H3 \* H4 \* H5 \* H6 \* H7 \* \$_nat n \* HT ==> HA \* (\$_nat m \* HR).
-Proof using. intros. rewrite (star_comm_assoc H7). apply~ hsimpl_cancel_credits_nat_7. Qed.
-
-Lemma hsimpl_cancel_credits_nat_9 : forall (n m : nat) HA HR H1 H2 H3 H4 H5 H6 H7 H8 HT,
-  (n >= m)%nat -> \$_nat (n - m) \* H1 \* H2 \* H3 \* H4 \* H5 \* H6 \* H7 \* H8 \* HT ==> HA \* HR ->
-  H1 \* H2 \* H3 \* H4 \* H5 \* H6 \* H7 \* H8 \* \$_nat n \* HT ==> HA \* (\$_nat m \* HR).
-Proof using. intros. rewrite (star_comm_assoc H8). apply~ hsimpl_cancel_credits_nat_8. Qed.
-
-Lemma hsimpl_cancel_credits_nat_10 : forall (n m : nat) HA HR H1 H2 H3 H4 H5 H6 H7 H8 H9 HT,
-  (n >= m)%nat -> \$_nat (n - m) \* H1 \* H2 \* H3 \* H4 \* H5 \* H6 \* H7 \* H8 \* H9 \* HT ==> HA \* HR ->
-  H1 \* H2 \* H3 \* H4 \* H5 \* H6 \* H7 \* H8 \* H9 \* \$_nat n \* HT ==> HA \* (\$_nat m \* HR).
-Proof using. intros. rewrite (star_comm_assoc H9). apply~ hsimpl_cancel_credits_nat_9. Qed.
-
-
-Lemma hsimpl_cancel_credits_int_1 : forall n m HA HR HT,
-  n >= m -> m >= 0 ->
-  \$ (n - m) \* HT ==> HA \* HR -> \$ n \* HT ==> HA \* (\$ m \* HR).
-Proof using.
-  introv L R E. math_rewrite (n = (n - m) + m).
-  rewrite credits_int_split_eq. rewrite <- star_assoc.
-  applys~ hsimpl_cancel_2. math. math.
-Qed.
-
-Lemma hsimpl_cancel_credits_int_2 : forall n m HA HR H1 HT,
-  n >= m -> m >= 0 ->
+Lemma hsimpl_cancel_credits_2 : forall (n m : int) HA HR H1 HT,
   \$ (n - m) \* H1 \* HT ==> HA \* HR ->
   H1 \* \$ n \* HT ==> HA \* (\$ m \* HR).
 Proof using.
-  intros. rewrite (star_comm_assoc H1). apply~ hsimpl_cancel_credits_int_1.
+  intros. rewrite (star_comm_assoc H1). apply~ hsimpl_cancel_credits_1.
 Qed.
 
-Lemma hsimpl_cancel_credits_int_3 : forall n m HA HR H1 H2 HT,
-  n >= m -> m >= 0 ->
+Lemma hsimpl_cancel_credits_3 : forall (n m : int) HA HR H1 H2 HT,
   \$ (n - m) \* H1 \* H2 \* HT ==> HA \* HR ->
   H1 \* H2 \* \$ n \* HT ==> HA \* (\$ m \* HR).
-Proof using. intros. rewrite (star_comm_assoc H2). apply~ hsimpl_cancel_credits_int_2. Qed.
+Proof using. intros. rewrite (star_comm_assoc H2). apply~ hsimpl_cancel_credits_2. Qed.
 
-Lemma hsimpl_cancel_credits_int_4 : forall n m HA HR H1 H2 H3 HT,
-  n >= m -> m >= 0 ->
+Lemma hsimpl_cancel_credits_4 : forall (n m : int) HA HR H1 H2 H3 HT,
   \$ (n - m) \* H1 \* H2 \* H3 \* HT ==> HA \* HR ->
   H1 \* H2 \* H3 \* \$ n \* HT ==> HA \* (\$ m \* HR).
-Proof using. intros. rewrite (star_comm_assoc H3). apply~ hsimpl_cancel_credits_int_3. Qed.
+Proof using. intros. rewrite (star_comm_assoc H3). apply~ hsimpl_cancel_credits_3. Qed.
 
-Lemma hsimpl_cancel_credits_int_5 : forall n m HA HR H1 H2 H3 H4 HT,
-  n >= m -> m >= 0 ->
+Lemma hsimpl_cancel_credits_5 : forall (n m : int) HA HR H1 H2 H3 H4 HT,
   \$ (n - m) \* H1 \* H2 \* H3 \* H4 \* HT ==> HA \* HR ->
   H1 \* H2 \* H3 \* H4 \* \$ n \* HT ==> HA \* (\$ m \* HR).
-Proof using. intros. rewrite (star_comm_assoc H4). apply~ hsimpl_cancel_credits_int_4. Qed.
+Proof using. intros. rewrite (star_comm_assoc H4). apply~ hsimpl_cancel_credits_4. Qed.
 
-Lemma hsimpl_cancel_credits_int_6 : forall n m HA HR H1 H2 H3 H4 H5 HT,
-  n >= m -> m >= 0 ->
+Lemma hsimpl_cancel_credits_6 : forall (n m : int) HA HR H1 H2 H3 H4 H5 HT,
   \$ (n - m) \* H1 \* H2 \* H3 \* H4 \* H5 \* HT ==> HA \* HR ->
   H1 \* H2 \* H3 \* H4 \* H5 \* \$ n \* HT ==> HA \* (\$ m \* HR).
-Proof using. intros. rewrite (star_comm_assoc H5). apply~ hsimpl_cancel_credits_int_5. Qed.
+Proof using. intros. rewrite (star_comm_assoc H5). apply~ hsimpl_cancel_credits_5. Qed.
 
-Lemma hsimpl_cancel_credits_int_7 : forall n m HA HR H1 H2 H3 H4 H5 H6 HT,
-  n >= m -> m >= 0 ->
+Lemma hsimpl_cancel_credits_7 : forall (n m : int) HA HR H1 H2 H3 H4 H5 H6 HT,
   \$ (n - m) \* H1 \* H2 \* H3 \* H4 \* H5 \* H6 \* HT ==> HA \* HR ->
   H1 \* H2 \* H3 \* H4 \* H5 \* H6 \* \$ n \* HT ==> HA \* (\$ m \* HR).
-Proof using. intros. rewrite (star_comm_assoc H6). apply~ hsimpl_cancel_credits_int_6. Qed.
+Proof using. intros. rewrite (star_comm_assoc H6). apply~ hsimpl_cancel_credits_6. Qed.
 
-Lemma hsimpl_cancel_credits_int_8 : forall n m HA HR H1 H2 H3 H4 H5 H6 H7 HT,
-  n >= m -> m >= 0 ->
+Lemma hsimpl_cancel_credits_8 : forall (n m : int) HA HR H1 H2 H3 H4 H5 H6 H7 HT,
   \$ (n - m) \* H1 \* H2 \* H3 \* H4 \* H5 \* H6 \* H7 \* HT ==> HA \* HR ->
   H1 \* H2 \* H3 \* H4 \* H5 \* H6 \* H7 \* \$ n \* HT ==> HA \* (\$ m \* HR).
-Proof using. intros. rewrite (star_comm_assoc H7). apply~ hsimpl_cancel_credits_int_7. Qed.
+Proof using. intros. rewrite (star_comm_assoc H7). apply~ hsimpl_cancel_credits_7. Qed.
 
-Lemma hsimpl_cancel_credits_int_9 : forall n m HA HR H1 H2 H3 H4 H5 H6 H7 H8 HT,
-  n >= m -> m >= 0 ->
+Lemma hsimpl_cancel_credits_9 : forall (n m : int) HA HR H1 H2 H3 H4 H5 H6 H7 H8 HT,
   \$ (n - m) \* H1 \* H2 \* H3 \* H4 \* H5 \* H6 \* H7 \* H8 \* HT ==> HA \* HR ->
   H1 \* H2 \* H3 \* H4 \* H5 \* H6 \* H7 \* H8 \* \$ n \* HT ==> HA \* (\$ m \* HR).
-Proof using. intros. rewrite (star_comm_assoc H8). apply~ hsimpl_cancel_credits_int_8. Qed.
+Proof using. intros. rewrite (star_comm_assoc H8). apply~ hsimpl_cancel_credits_8. Qed.
 
-Lemma hsimpl_cancel_credits_int_10 : forall n m HA HR H1 H2 H3 H4 H5 H6 H7 H8 H9 HT,
-  n >= m -> m >= 0 ->
+Lemma hsimpl_cancel_credits_10 : forall (n m : int) HA HR H1 H2 H3 H4 H5 H6 H7 H8 H9 HT,
   \$ (n - m) \* H1 \* H2 \* H3 \* H4 \* H5 \* H6 \* H7 \* H8 \* H9 \* HT ==> HA \* HR ->
   H1 \* H2 \* H3 \* H4 \* H5 \* H6 \* H7 \* H8 \* H9 \* \$ n \* HT ==> HA \* (\$ m \* HR).
-Proof using. intros. rewrite (star_comm_assoc H9). apply~ hsimpl_cancel_credits_int_9. Qed.
+Proof using. intros. rewrite (star_comm_assoc H9). apply~ hsimpl_cancel_credits_9. Qed.
 
 
 Lemma hsimpl_cancel_eq_1 : forall H H' HA HR HT,
@@ -1874,7 +1865,8 @@ Ltac hsimpl_cleanup tt :=
   try hsimpl_hint_remove tt;
   try remove_empty_heaps_right tt;
   try remove_empty_heaps_left tt;
-  try apply hsimpl_gc.
+  try apply hsimpl_gc;
+  try affine.
 
 Ltac hsimpl_try_same tt :=
   first
@@ -1918,32 +1910,18 @@ Ltac hsimpl_find_data l HL cont :=
   | _ \* _ \* _ \* _ \* _ \* _ \* _ \* _ \* _ \* hdata _ l \* _ => apply hsimpl_cancel_eq_10
   end; [ cont tt | ].
 
-Ltac hsimpl_find_credits_nat HL :=
-  match HL with
-  | \$_nat _ \* _ => apply hsimpl_cancel_credits_nat_1
-  | _ \* \$_nat _ \* _ => apply hsimpl_cancel_credits_nat_2
-  | _ \* _ \* \$_nat _ \* _ => apply hsimpl_cancel_credits_nat_3
-  | _ \* _ \* _ \* \$_nat _ \* _ => apply hsimpl_cancel_credits_nat_4
-  | _ \* _ \* _ \* _ \* \$_nat _ \* _ => apply hsimpl_cancel_credits_nat_5
-  | _ \* _ \* _ \* _ \* _ \* \$_nat _ \* _ => apply hsimpl_cancel_credits_nat_6
-  | _ \* _ \* _ \* _ \* _ \* _ \* \$_nat _ \* _ => apply hsimpl_cancel_credits_nat_7
-  | _ \* _ \* _ \* _ \* _ \* _ \* _ \* \$_nat _ \* _ => apply hsimpl_cancel_credits_nat_8
-  | _ \* _ \* _ \* _ \* _ \* _ \* _ \* _ \* \$_nat _ \* _ => apply hsimpl_cancel_credits_nat_9
-  | _ \* _ \* _ \* _ \* _ \* _ \* _ \* _ \* _ \* \$_nat _ \* _ => apply hsimpl_cancel_credits_nat_10
-  end.
-
-Ltac hsimpl_find_credits_int HL :=
+Ltac hsimpl_find_credits HL :=
   match HL with
-  | \$ _ \* _ => apply hsimpl_cancel_credits_int_1
-  | _ \* \$ _ \* _ => apply hsimpl_cancel_credits_int_2
-  | _ \* _ \* \$ _ \* _ => apply hsimpl_cancel_credits_int_3
-  | _ \* _ \* _ \* \$ _ \* _ => apply hsimpl_cancel_credits_int_4
-  | _ \* _ \* _ \* _ \* \$ _ \* _ => apply hsimpl_cancel_credits_int_5
-  | _ \* _ \* _ \* _ \* _ \* \$ _ \* _ => apply hsimpl_cancel_credits_int_6
-  | _ \* _ \* _ \* _ \* _ \* _ \* \$ _ \* _ => apply hsimpl_cancel_credits_int_7
-  | _ \* _ \* _ \* _ \* _ \* _ \* _ \* \$ _ \* _ => apply hsimpl_cancel_credits_int_8
-  | _ \* _ \* _ \* _ \* _ \* _ \* _ \* _ \* \$ _ \* _ => apply hsimpl_cancel_credits_int_9
-  | _ \* _ \* _ \* _ \* _ \* _ \* _ \* _ \* _ \* \$ _ \* _ => apply hsimpl_cancel_credits_int_10
+  | \$ _ \* _ => apply hsimpl_cancel_credits_1
+  | _ \* \$ _ \* _ => apply hsimpl_cancel_credits_2
+  | _ \* _ \* \$ _ \* _ => apply hsimpl_cancel_credits_3
+  | _ \* _ \* _ \* \$ _ \* _ => apply hsimpl_cancel_credits_4
+  | _ \* _ \* _ \* _ \* \$ _ \* _ => apply hsimpl_cancel_credits_5
+  | _ \* _ \* _ \* _ \* _ \* \$ _ \* _ => apply hsimpl_cancel_credits_6
+  | _ \* _ \* _ \* _ \* _ \* _ \* \$ _ \* _ => apply hsimpl_cancel_credits_7
+  | _ \* _ \* _ \* _ \* _ \* _ \* _ \* \$ _ \* _ => apply hsimpl_cancel_credits_8
+  | _ \* _ \* _ \* _ \* _ \* _ \* _ \* _ \* \$ _ \* _ => apply hsimpl_cancel_credits_9
+  | _ \* _ \* _ \* _ \* _ \* _ \* _ \* _ \* _ \* \$ _ \* _ => apply hsimpl_cancel_credits_10
   end.
 
 Ltac hsimpl_extract_exists tt :=
@@ -2031,8 +2009,7 @@ Ltac hsimpl_step process_credits :=
     | ?H => (* should be check_noevar3 on the next line TODO *)
        first [ is_evar H; fail 1 | idtac ];
        hsimpl_find_same H HL (* may fail *)
-    | \$_nat _ => check_arg_true process_credits; hsimpl_find_credits_nat HL
-    | \$ _ => check_arg_true process_credits; hsimpl_find_credits_int HL
+    | \$ _ => check_arg_true process_credits; hsimpl_find_credits HL
     | hdata _ ?l => hsimpl_find_data l HL ltac:(hsimpl_find_data_post) (* may fail *)
     | ?x ~> Id _ => check_noevar2 x; apply hsimpl_id (* may fail *)
     | ?x ~> ?T _ => check_noevar2 x;
@@ -2062,8 +2039,7 @@ idtac HN;
     | ?H => idtac "find";
         first [ has_evar H; idtac "has evar"; fail 1 | idtac "has no evar" ];
          hsimpl_find_same H HL (* may fail *)
-    | \$_nat _ => check_arg_true process_credits; idtac "credits_nat"; hsimpl_find_credits_nat HL
-    | \$ _ => check_arg_true process_credits; idtac "credits_int"; hsimpl_find_credits_int HL
+    | \$ _ => check_arg_true process_credits; idtac "credits"; hsimpl_find_credits HL
     | hdata _ ?l => idtac "hdata"; hsimpl_find_data l HL ltac:(hsimpl_find_data_post) (* may fail *)
     | ?x ~> Id _ => idtac "id";  check_noevar x; apply hsimpl_id (* todo: why is this requiring a fail 2 ? *)
     | ?x ~> _ _ => idtac "some";  check_noevar2 x; apply hsimpl_id_unify
@@ -2173,24 +2149,6 @@ Tactic Notation "chsimpl" "~" := chsimpl; auto_tilde.
 Tactic Notation "chsimpl" "*" := chsimpl; auto_star.
 
 
-(********************************************************************)
-(* ** Derived lemmas using hsimpl *)
-
-Section Facts.
-Transparent heap_is_credits_int.
-
-Lemma pay_one_nat : forall H H',
-  pay_one H H' = (H ==> \$_nat 1%nat \* H').
-Proof using.
-  intros. unfolds. fequals.
-  unfold heap_is_credits_int.
-  asserts_rewrite ((Z.abs_nat 1%Z) = 1%nat).
-    forwards~: succ_abs_eq_abs_one_plus 0. math.
-  apply pred_incl_antisym. hsimpl. hsimpl. math.
-Qed.
-
-End Facts.
-
 (********************************************************************)
 (* ** Other stuff *)
 
@@ -2669,11 +2627,12 @@ Qed.
 
 Lemma local_gc_pre_on : forall HG H' B (F:~~B) H Q,
   is_local F ->
+  affine HG ->
   H ==> HG \* H' ->
   F H' Q ->
   F H Q.
 Proof using.
-  introv L M W. rewrite L. introv Ph.
+  introv L HA M W. rewrite L. introv Ph.
   exists H' HG Q. splits.
   rewrite star_comm. apply~ M.
   auto.
@@ -2699,7 +2658,7 @@ Lemma local_weaken_gc_pre : forall B H' Q' (F:~~B) (H:hprop) Q,
   Q' ===> Q ->
   F H Q.
 Proof using.
-  intros. apply* (@local_gc_pre_on (\GC) H'). hchange H2. hsimpl.
+  intros. apply* (@local_gc_pre_on (\GC) H'). affine. hchange H2. hsimpl.
   applys* local_weaken.
 Qed.
 
diff --git a/lib/coq/CFLibCredits.v b/lib/coq/CFLibCredits.v
index 530638b968a001c0ad839808b10d375bf62d88e8..27648983e35c2eebf4bff357d98ae4518f82b694 100644
--- a/lib/coq/CFLibCredits.v
+++ b/lib/coq/CFLibCredits.v
@@ -28,17 +28,14 @@ Implicit Types x y z : int.
 (********************************************************************)
 (** Additional lemmas on credits *)
 
-Definition credits_nat_eq := 
-  args_eq_1 heap_is_credits_nat. 
-  (* todo: state as a lemma instead *)
-
-Lemma credits_nat_zero_eq_prove : forall (n:nat),
-  n = 0%nat -> \$_nat n = \[].
-Proof. intros. subst. apply credits_nat_zero_eq. Qed.
+Lemma credits_eq : forall x y,
+  x = y ->
+  \$ x = \$ y.
+Proof. apply (args_eq_1 heap_is_credits). Qed.
 
 Lemma credits_int_zero_eq_prove : forall (x:int),
   x = 0 -> \$ x = \[].
-Proof. intros. subst. apply credits_int_zero_eq. Qed.
+Proof. intros. subst. apply credits_zero_eq. Qed.
 
 
 
diff --git a/lib/coq/CFTactics.v b/lib/coq/CFTactics.v
index 7bd5022f14b0710c640fdd0dd614c106062b7c59..1bf8e5bdaad7a0b61240ff1c5ae0c1ef2af276c6 100644
--- a/lib/coq/CFTactics.v
+++ b/lib/coq/CFTactics.v
@@ -505,6 +505,7 @@ Tactic Notation "xpull" "as" simple_intropattern(I1) simple_intropattern(I2)
 Ltac xgc_remove_hprop H :=
   eapply (@local_gc_pre_on H);
     [ try xlocal
+    | try affine
     | hsimpl
     | xtag_pre_post ].
 
@@ -557,6 +558,7 @@ Ltac xgc_post_if_not_evar_then cont :=
 
 Lemma local_gc_pre_all : forall B Q (F:~~B) H,
   is_local F ->
+  affine H ->
   F \[] Q ->
   F H Q.
 Proof using. intros. apply* (@local_gc_pre_on H). hsimpl. Qed.
@@ -1618,7 +1620,7 @@ Lemma xret_lemma : forall B (v:B) H (Q:B->hprop),
   local (fun H' Q' => H' ==> Q' v) H Q.
 Proof using.
   introv W. eapply (@local_gc_pre_on (\GC)).
-  auto. hchanges W. apply~ local_erase. hsimpl.
+  auto. affine. hchanges W. apply~ local_erase. hsimpl.
 Qed.
 
 (* Lemma used by [xret] and [xret_no_gc]
@@ -3832,15 +3834,11 @@ Tactic Notation "xname_post" ident(X) :=
     used before a credit split operation, e.g. to replace
     [$n] with [$a \* $b], when [n = a + b].
 
-    LATER: add demos for this tactic. 
+    LATER: add demos for this tactic.
   *)
 
 Ltac xcredit goal :=
   match goal with
-  | |- context[\$_nat goal] =>
-      idtac (* no need to rewrite *)
-  | |- context[\$_nat ?n] =>
-      math_rewrite (n = goal :> nat)
   | |- context[\$ goal] =>
       idtac (* no need to rewrite *)
   | |- context[\$ ?n] =>
@@ -3867,15 +3865,11 @@ Ltac xpay_start tt :=
 Ltac xpay_core tt :=
   xpay_start tt; [ unfold pay_one; hsimpl | ].
 
-Ltac xpay_nat_core tt :=
-  xpay_start tt; [ rewrite pay_one_nat; hsimpl | ].
-
 Tactic Notation "xpay" := xpay_core tt.
 
 Ltac xpay_on_impl goal :=
   xcredit goal;
-  first [ rewrite credits_int_split_eq 
-        | rewrite credits_nat_split_eq ];
+  first [ rewrite credits_split_eq ];
   xpay.
 
 Tactic Notation "xpay" constr(goal) :=
@@ -3913,12 +3907,22 @@ Tactic Notation "xpay_skip" := xpay_fake tt.
 Ltac xgc_credit_core HP :=
   let H := fresh in
   let E := fresh in
-  destruct (credits_nat_le_rest HP) as (H&E);
-  xchange E; [ chsimpl | xgc H; clear H E ].
+  destruct (credits_le_rest HP) as (H&HA&E);
+  xchange E; [ xgc H; clear H HA E; hclean ].
 
 Tactic Notation "xgc_credit" constr(HP) :=
   xgc_credit_core HP.
 
+Goal forall m n B (F : ~~B) Q,
+  m <= n ->
+  is_local F ->
+  F (\$m) Q ->
+  F (\$n) Q.
+Proof.
+  introv H L HH.
+  xgc_credit_core H.
+  assumption.
+Qed.
 
 (*--------------------------------------------------------*)
 (* ** [xskip_credits] *)
diff --git a/lib/stdlib/Array_proof.v b/lib/stdlib/Array_proof.v
index a373b3e502a2ec7270e66589ac512f7eeb5ea395..5a463da5d5e4735f15ad2bafd422f0d2d1192f29 100644
--- a/lib/stdlib/Array_proof.v
+++ b/lib/stdlib/Array_proof.v
@@ -32,6 +32,10 @@ Parameter Array : forall A, list A -> loc -> hprop.
      the ownership of single cells, each of which being
      described using heap_is_single. *)
 
+Parameter Array_affine : forall A t (L: list A), affine (t ~> Array L).
+  (* TODO: prove this *)
+Hint Resolve Array_affine : affine.
+
 (* -------------------------------------------------------------------------- *)
 
 (* The length of an array is at most [Sys.max_array_length]. This could be
diff --git a/lib/stdlib/Pervasives_proof.v b/lib/stdlib/Pervasives_proof.v
index 2ef585b3cd8635470de5ccb0ddd356aa739c8965..8f0bd6c9c4d67b9e78d9e4ac469e9fdc8ce3db1e 100644
--- a/lib/stdlib/Pervasives_proof.v
+++ b/lib/stdlib/Pervasives_proof.v
@@ -260,6 +260,10 @@ Qed.
 Notation "r '~~>' v" := (hdata (Ref v) r)
   (at level 32, no associativity) : heap_scope.
 
+(* TODO: prove it and/or generalize wrt Heapdata *)
+Parameter Ref_affine : forall A r (v: A), affine (r ~~> v).
+Hint Resolve Ref_affine : affine.
+
 Lemma ref_spec : forall A (v:A),
   app ref [v]
     PRE \[]