Make Program obligations Transparent by default.

This may save the need to seal off some stuff.

Make Program obligations Transparent by default.
This may save the need to seal off some stuff.
0a1cf07d · Robbert Krebbers · d11b32df · 0a1cf07d
Commit 0a1cf07d authored Jul 01, 2016 by Robbert Krebbers
Hide whitespace changes
Inline Side-by-side

Showing with 1 addition and 0 deletions

theories/base.v theories/base.v +1 -0

No files found.
--- 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.