next blind fix

math-comp · Jul 22, 2015 · 5558b68 · 5558b68
1 parent 4a1a55b
commit 5558b68
Showing 1 changed file with 1 addition and 3 deletions.
diff --git 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).