From 9af65178a18a9db0cd6039e13d5f5bfe2b2baccc 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.
---
 algebra/agree.v | 4 ++--
 prelude/base.v  | 1 +
 2 files changed, 3 insertions(+), 2 deletions(-)

diff --git a/algebra/agree.v b/algebra/agree.v
index 6479419c0..a62b288f2 100644
--- a/algebra/agree.v
+++ b/algebra/agree.v
@@ -148,8 +148,8 @@ Arguments agreeC : clear implicits.
 Arguments agreeR : clear implicits.
 
 Program Definition agree_map {A B} (f : A → B) (x : agree A) : agree B :=
-  {| agree_car n := f (x n); agree_is_valid := agree_is_valid x |}.
-Solve Obligations with auto using agree_valid_S.
+  {| agree_car n := f (x n); agree_is_valid := agree_is_valid x;
+     agree_valid_S := agree_valid_S _ x |}.
 Lemma agree_map_id {A} (x : agree A) : agree_map id x = x.
 Proof. by destruct x. Qed.
 Lemma agree_map_compose {A B C} (f : A → B) (g : B → C) (x : agree A) :
diff --git a/prelude/base.v b/prelude/base.v
index fc03e031f..c4c2eb822 100644
--- a/prelude/base.v
+++ b/prelude/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