diff --git a/algebra/base.v b/algebra/base.v index 413117f125b70d4bc1f640c181edf13882c52f4c..5235048e27407546fdfa3d668df21e503b052d9a 100644 --- a/algebra/base.v +++ b/algebra/base.v @@ -1,4 +1,4 @@ -From mathcomp.ssreflect Require Export ssreflect. +From mathcomp Require Export ssreflect. From prelude Require Export prelude. Global Set Bullet Behavior "Strict Subproofs". Global Open Scope general_if_scope.