From 4a1a55bb51ceb1439a77432d75f6a86c95aaaa14 Mon Sep 17 00:00:00 2001
From: Cyril Cohen
Date: Wed, 22 Jul 2015 17:03:20 +0200
Subject: blind fix

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

(limited to 'mathcomp')

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