From ab2b5816cea1c309d33e31f89bfa112c9b1966cc Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 18 Feb 2016 14:09:24 +0100
Subject: [PATCH] turns out we can import with shorter names (and we actually
 already do that frequently in "From Coq Import")

---
 algebra/base.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/algebra/base.v b/algebra/base.v
index 413117f12..5235048e2 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.
-- 
GitLab