From 0a1cf07df2d2dab7475c7df645caede1adbbfc2a Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 1 Jul 2016 14:20:34 +0200
Subject: [PATCH] Make Program obligations Transparent by default.

This may save the need to seal off some stuff.
---
 theories/base.v | 1 +
 1 file changed, 1 insertion(+)

diff --git a/theories/base.v b/theories/base.v
index fc03e031..c4c2eb82 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -7,6 +7,7 @@ structures. *)
 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.
 Obligation Tactic := idtac.
 
-- 
GitLab