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/Make                    | 3 +++
 mathcomp/ssrtest/explain_match.v | 3 ++-
 2 files changed, 5 insertions(+), 1 deletion(-)

(limited to 'mathcomp')

diff --git a/mathcomp/Make b/mathcomp/Make
index e259330..d3c7642 100644
--- a/mathcomp/Make
+++ b/mathcomp/Make
@@ -132,15 +132,18 @@ ssreflect/ssrnat.v
 ssreflect/ssrnotations.v
 ssreflect/tuple.v
 ssrtest/absevarprop.v
+ssrtest/abstract_var2.v
 ssrtest/binders_of.v
 ssrtest/binders.v
 ssrtest/caseview.v
 ssrtest/congr.v
 ssrtest/deferclear.v
+ssrtest/derive_inversion.v
 ssrtest/dependent_type_err.v
 ssrtest/elim2.v
 ssrtest/elim_pattern.v
 ssrtest/elim.v
+ssrtest/explain_match.v
 ssrtest/first_n.v
 ssrtest/gen_have.v
 ssrtest/gen_pattern.v
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