From 3b2fd56a5645b3bd436085e514519c9f61200ae5 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Tue, 6 Feb 2018 13:52:29 +0100
Subject: add 3 tests to Make

---
 mathcomp/ssrtest/explain_match.v | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'mathcomp/ssrtest')

diff --git a/mathcomp/ssrtest/explain_match.v b/mathcomp/ssrtest/explain_match.v
index b79453b..2c7bc2f 100644
--- a/mathcomp/ssrtest/explain_match.v
+++ b/mathcomp/ssrtest/explain_match.v
@@ -1,3 +1,4 @@
+Require Import ssrmatching.
 Require Import ssreflect ssrbool ssrnat.
 
 Definition addnAC := (addnA, addnC).
@@ -9,4 +10,4 @@ ssrinstancesofruleL2R addnC.
 ssrinstancesofruleR2L addnA.
 ssrinstancesofruleR2L addnAC.
 Fail ssrinstancesoftpat (_ + _ in RHS). (* Not implemented *)
-Admitted.
\ No newline at end of file
+Admitted.
-- 
cgit v1.2.3