diff --git a/theories/base.v b/theories/base.v
index 370621e1054bd56d509a833e22f8de34345a81b3..1d35448e8c2d753375a6e5891afe7f009a2b0178 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -8,7 +8,9 @@ Global Generalizable All Variables.
 Global Set Automatic Coercions Import.
 Global Set Asymmetric Patterns.
 Global Unset Transparent Obligations.
-From Coq Require Export Morphisms RelationClasses List Bool Utf8 Program Setoid.
+From Coq Require Export Morphisms RelationClasses List Bool Utf8 Setoid.
+Export ListNotations.
+From Coq.Program Require Export Basics Syntax.
 Obligation Tactic := idtac.
 
 (** Throughout this development we use [C_scope] for all general purpose
diff --git a/theories/pretty.v b/theories/pretty.v
index 05636db16f603c2ba7a476a4a334e7c636b4a304..58fd38347cb830e869560976e93956b39a6fa73f 100644
--- a/theories/pretty.v
+++ b/theories/pretty.v
@@ -37,8 +37,7 @@ Proof.
   by destruct (decide (0 < x)%N); auto using pretty_N_go_help_irrel.
 Qed.
 Instance pretty_N : Pretty N := λ x, pretty_N_go x ""%string.
-Lemma pretty_N_unfold x :
-  pretty x = pretty_N_go x "".
+Lemma pretty_N_unfold x : pretty x = pretty_N_go x "".
 Proof. done. Qed.
 Instance pretty_N_inj : Inj (@eq N) (=) pretty.
 Proof.
@@ -48,8 +47,7 @@ Proof.
   cut (∀ x y s s', pretty_N_go x s = pretty_N_go y s' →
     String.length s = String.length s' → x = y ∧ s = s').
   { intros help x y Hp.
-    eapply (help x y "" ""); [by rewrite <-!pretty_N_unfold|].
-    eauto. }
+    eapply (help x y "" ""); [by rewrite <-!pretty_N_unfold|done]. }
   assert (∀ x s, ¬String.length (pretty_N_go x s) < String.length s) as help.
   { setoid_rewrite <-Nat.le_ngt.
     intros x; induction (N.lt_wf_0 x) as [x _ IH]; intros s.
diff --git a/theories/tactics.v b/theories/tactics.v
index ce5a3b957234411f9308f555e0543bb7c90ac976..b1b9224e71bc1f288c761c698e9ec67005525af5 100644
--- a/theories/tactics.v
+++ b/theories/tactics.v
@@ -407,6 +407,13 @@ Tactic Notation "feed" "destruct" constr(H) :=
 Tactic Notation "feed" "destruct" constr(H) "as" simple_intropattern(IP) :=
   feed (fun p => let H':=fresh in pose proof p as H'; destruct H' as IP) H.
 
+(** The block definitions are taken from [Coq.Program.Equality] and can be used
+by tactics to separate their goal from hypotheses they generalize over. *)
+Definition block {A : Type} (a : A) := a.
+
+Ltac block_goal := match goal with [ |- ?T ] => change (block T) end.
+Ltac unblock_goal := unfold block in *.
+
 
 (** The following tactic can be used to add support for patterns to tactic notation:
 It will search for the first subterm of the goal matching [pat], and then call [tac]