From 5558b68a828897fadbedaf544e786948c3865f35 Mon Sep 17 00:00:00 2001
From: Cyril Cohen
Date: Wed, 22 Jul 2015 17:16:53 +0200
Subject: next blind fix

---
 mathcomp/ssrtest/ssrsyntax2.v | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

(limited to 'mathcomp')

diff --git a/mathcomp/ssrtest/ssrsyntax2.v b/mathcomp/ssrtest/ssrsyntax2.v
index 21088c8..b0f8f98 100644
--- a/mathcomp/ssrtest/ssrsyntax2.v
+++ b/mathcomp/ssrtest/ssrsyntax2.v
@@ -1,7 +1,5 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
-Require Import mathcomp.ssreflect.ssreflect.
-From mathcomp
-Require Import ssrsyntax1.
+Require Import mathcomp.ssrtest.ssrsyntax1.
 Require Import Arith.
 
 Goal (forall a b, a + b = b + a).
-- 
cgit v1.2.3