diff --git a/modures/base.v b/modures/base.v
index daca953991be97e2d08d06ae875329258e789c7a..28ba9cc272f4d46bfecc870d7333bea6757ff535 100644
--- a/modures/base.v
+++ b/modures/base.v
@@ -1,3 +1,4 @@
 Require Export mathcomp.ssreflect.ssreflect.
 Require Export prelude.prelude.
 Global Set Bullet Behavior "Strict Subproofs".
+Global Open Scope general_if_scope.
\ No newline at end of file