From fb9ccea7f34b7fcd01a5f0f97b5c52b188154f5b Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 25 Feb 2016 15:20:35 +0100 Subject: ssrpattern: compose nicely with Tactic Notation --- mathcomp/Make | 1 + 1 file changed, 1 insertion(+) (limited to 'mathcomp/Make') diff --git a/mathcomp/Make b/mathcomp/Make index 9f41de1..a235149 100644 --- a/mathcomp/Make +++ b/mathcomp/Make @@ -172,6 +172,7 @@ ssrtest/view_case.v ssrtest/wlogletin.v ssrtest/wlog_suff.v ssrtest/wlong_intro.v +ssrtest/tacnotationpattern.v ssreflect.ml4 ssreflect.mllib ssrmatching.ml4 -- cgit v1.2.3