diff --git a/theories/base.v b/theories/base.v
index fc03e031f598d2131524c7b9e6fad0a2314b1c85..c4c2eb8227a2d20700f5554db1a3a476ad273268 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.