From 7ea0db435910c2db2a9ae4cadfd54f49f3640b62 Mon Sep 17 00:00:00 2001
From: Jim Fehrle
Date: Mon, 18 Jan 2021 21:22:52 -0800
Subject: Remove the Hide Obligations flag

---
 theories/Program/Tactics.v | 4 ----
 1 file changed, 4 deletions(-)

(limited to 'theories/Program')

diff --git a/theories/Program/Tactics.v b/theories/Program/Tactics.v
index fce69437d7..d852ad24fe 100644
--- a/theories/Program/Tactics.v
+++ b/theories/Program/Tactics.v
@@ -319,7 +319,3 @@ Create HintDb program discriminated.
 Ltac program_simpl := program_simplify ; try typeclasses eauto 10 with program ; try program_solve_wf.
 
 Obligation Tactic := program_simpl.
-
-Definition obligation (A : Type) {a : A} := a.
-
-Register obligation as program.tactics.obligation.
-- 
cgit v1.2.3