From be707cec756ec7b23555adedd71e8a9c683441a5 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 9 Mar 2017 10:39:10 +0100
Subject: [PATCH] Blacklist `_obligation_` for Search.

---
 theories/base.v | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/theories/base.v b/theories/base.v
index 78af51fb..1f2cc470 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.
-- 
GitLab