From d54b8dff818f0b1218df14cfb2b813da93154fa9 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Thu, 12 Apr 2018 09:54:36 +0200
Subject: remove ssrtest: it now belongs to Coq

---
 mathcomp/Make | 46 ----------------------------------------------
 1 file changed, 46 deletions(-)

(limited to 'mathcomp/Make')

diff --git a/mathcomp/Make b/mathcomp/Make
index 1db29ba..ee016ce 100644
--- a/mathcomp/Make
+++ b/mathcomp/Make
@@ -132,52 +132,6 @@ ssreflect/ssrnat.v
 ssreflect/ssrnotations.v
 ssreflect/ssrmatching.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
-ssrtest/havesuff.v
-ssrtest/have_TC.v
-ssrtest/have_transp.v
-ssrtest/have_view_idiom.v
-ssrtest/if_isnt.v
-ssrtest/indetLHS.v
-ssrtest/intro_beta.v
-ssrtest/intro_noop.v
-ssrtest/ipatalternation.v
-ssrtest/ltac_have.v
-ssrtest/ltac_in.v
-ssrtest/move_after.v
-ssrtest/multiview.v
-ssrtest/occarrow.v
-ssrtest/patnoX.v
-ssrtest/primproj.v
-ssrtest/rewpatterns.v
-ssrtest/set_lamda.v
-ssrtest/set_pattern.v
-ssrtest/ssrsyntax1.v
-ssrtest/ssrsyntax2.v
-ssrtest/tc.v
-ssrtest/testmx.v
-ssrtest/typeof.v
-ssrtest/unfold_Opaque.v
-ssrtest/unkeyed.v
-ssrtest/view_case.v
-ssrtest/wlogletin.v
-ssrtest/wlog_suff.v
-ssrtest/wlong_intro.v
 
 -I .
 -R . mathcomp
-- 
cgit v1.2.3