diff --git a/theories/base.v b/theories/base.v
index 78af51fb72d6f289b49a381d41c0d6def62da1cb..1f2cc470d3a0003c9df3d81e1c513140e575b73a 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -12,7 +12,11 @@ From Coq Require Export Morphisms RelationClasses List Bool Utf8 Setoid.
 Set Default Proof Using "Type".
 Export ListNotations.
 From Coq.Program Require Export Basics Syntax.
+
+(* Tweak program: don't let it automatically simplify obligations and hide
+them from the results of the [Search] commands. *)
 Obligation Tactic := idtac.
+Add Search Blacklist "_obligation_".
 
 (** Sealing off definitions *)
 Set Primitive Projections.