From 1fb7158584feed67769b64f4609504639ff6239c Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 22 Jan 2016 07:00:08 +0100
Subject: [PATCH] Fix scopes for if then else to also work with sumbool.

---
 modures/base.v | 1 +
 1 file changed, 1 insertion(+)

diff --git a/modures/base.v b/modures/base.v
index daca95399..28ba9cc27 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
-- 
GitLab