diff --git a/.gitattributes b/.gitattributes
new file mode 100644
index 0000000000000000000000000000000000000000..c925e3166ee66e64206fc6ef05efd4bda052ded0
--- /dev/null
+++ b/.gitattributes
@@ -0,0 +1 @@
+*.v gitlab-language=coq
diff --git a/README.md b/README.md
index ff5fba87fe72889aa00617fbeefb3c1ca0623103..1cfec97a868839746efe746d895bd84c7bba8160 100644
--- a/README.md
+++ b/README.md
@@ -7,7 +7,7 @@ This is the Coq development of the [Iris Project](http://iris-project.org).
 This version is known to compile with:
 
  - Coq 8.6.1 / 8.7.0
- - Ssreflect 1.6.2
+ - Ssreflect 1.6.4
  - A development version of [std++](https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp)
 
 If you need to work with Coq 8.5, please check out the
diff --git a/theories/heap_lang/tactics.v b/theories/heap_lang/tactics.v
index 6d7e58eaeb58dc8545d7db837a8a1bad4c5171bc..1198fb520ac2490fd90ca8390bb499a2dd0f47c2 100644
--- a/theories/heap_lang/tactics.v
+++ b/theories/heap_lang/tactics.v
@@ -195,7 +195,7 @@ Proof.
     destruct e=> //=; repeat (simplify_eq/=; case_match=>//);
       inversion 1; simplify_eq/=; rewrite ?to_of_val; eauto.
     unfold subst'; repeat (simplify_eq/=; case_match=>//); eauto.
-  - apply ectxi_language_sub_values=> /= Ki e' Hfill.
+  - apply ectxi_language_sub_redexes_are_values=> /= Ki e' Hfill.
     destruct e=> //; destruct Ki; repeat (simplify_eq/=; case_match=>//);
       naive_solver eauto using to_val_is_Some.
 Qed.
diff --git a/theories/program_logic/ectx_language.v b/theories/program_logic/ectx_language.v
index e9e92ab5ded233a35c1e720db1ae74327256c4a2..d8330354d3150be4dd10d200a839b13f77e2584c 100644
--- a/theories/program_logic/ectx_language.v
+++ b/theories/program_logic/ectx_language.v
@@ -62,7 +62,9 @@ Section ectx_language.
   Definition head_irreducible (e : expr) (σ : state) :=
     ∀ e' σ' efs, ¬head_step e σ e' σ' efs.
 
-  Definition sub_values (e : expr) :=
+  (* All non-value redexes are at the root.  In other words, all sub-redexes are
+     values. *)
+  Definition sub_redexes_are_values (e : expr) :=
     ∀ K e', e = fill K e' → to_val e' = None → K = empty_ectx.
 
   Inductive prim_step (e1 : expr) (σ1 : state)
@@ -103,21 +105,21 @@ Section ectx_language.
   Qed.
 
   Lemma prim_head_reducible e σ :
-    reducible e σ → sub_values e → head_reducible e σ.
+    reducible e σ → sub_redexes_are_values e → head_reducible e σ.
   Proof.
     intros (e'&σ'&efs&[K e1' e2' -> -> Hstep]) ?.
     assert (K = empty_ectx) as -> by eauto 10 using val_stuck.
     rewrite fill_empty /head_reducible; eauto.
   Qed.
   Lemma prim_head_irreducible e σ :
-    head_irreducible e σ → sub_values e → irreducible e σ.
+    head_irreducible e σ → sub_redexes_are_values e → irreducible e σ.
   Proof.
     rewrite -not_reducible -not_head_reducible. eauto using prim_head_reducible.
   Qed.
 
   Lemma ectx_language_atomic e :
     (∀ σ e' σ' efs, head_step e σ e' σ' efs → irreducible e' σ') →
-    sub_values e →
+    sub_redexes_are_values e →
     Atomic e.
   Proof.
     intros Hatomic_step Hatomic_fill σ e' σ' efs [K e1' e2' -> -> Hstep].
diff --git a/theories/program_logic/ectxi_language.v b/theories/program_logic/ectxi_language.v
index 71cb016b4c3a9f891fd55722c8ed149a8c784dd6..6475a921d966e2d7b9360ab1946049505c02c056 100644
--- a/theories/program_logic/ectxi_language.v
+++ b/theories/program_logic/ectxi_language.v
@@ -90,8 +90,9 @@ Section ectxi_language.
     fill_not_val, fill_app, step_by_val, foldl_app.
   Next Obligation. intros K1 K2 ?%app_eq_nil; tauto. Qed.
 
-  Lemma ectxi_language_sub_values e :
-    (∀ Ki e', e = fill_item Ki e' → is_Some (to_val e')) → sub_values e.
+  Lemma ectxi_language_sub_redexes_are_values e :
+    (∀ Ki e', e = fill_item Ki e' → is_Some (to_val e')) →
+    sub_redexes_are_values e.
   Proof.
     intros Hsub K e' ->. destruct K as [|Ki K _] using @rev_ind=> //=.
     intros []%eq_None_not_Some. eapply fill_val, Hsub. by rewrite /= fill_app.
diff --git a/theories/tests/tree_sum.v b/theories/tests/tree_sum.v
index d4609d5bbef731404e2dfd227bd87c39e3a22fdc..28f75f6c8a26e77a3c6ceea613114910dac6c48e 100644
--- a/theories/tests/tree_sum.v
+++ b/theories/tests/tree_sum.v
@@ -40,8 +40,7 @@ Lemma sum_loop_wp `{!heapG Σ} v t l (n : Z) :
   {{{ RET #(); l ↦ #(sum t + n) ∗ is_tree v t }}}.
 Proof.
   iIntros (Φ) "[Hl Ht] HΦ".
-  iLöb as "IH" forall (v t l n Φ). wp_rec. wp_let.
-  destruct t as [n'|tl tr]; simpl in *.
+  iInduction t as [n'|tl ? tr] "IH" forall (v l n Φ); wp_rec; wp_let.
   - iDestruct "Ht" as "%"; subst.
     wp_match. wp_load. wp_op. wp_store.
     by iApply ("HΦ" with "[$Hl]").
@@ -49,7 +48,7 @@ Proof.
     wp_match. wp_proj. wp_load.
     wp_apply ("IH" with "Hl Htl"). iIntros "[Hl Htl]".
     wp_seq. wp_proj. wp_load.
-    wp_apply ("IH" with "Hl Htr"). iIntros "[Hl Htr]".
+    wp_apply ("IH1" with "Hl Htr"). iIntros "[Hl Htr]".
     iApply "HΦ". iSplitL "Hl".
     { by replace (sum tl + sum tr + n) with (sum tr + (sum tl + n)) by omega. }
     iExists ll, lr, vl, vr. by iFrame.