From 5caebcd8ff2bedae02a23d79251a2344c7aea4d6 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Sat, 9 Jun 2007 16:02:11 +0000
Subject: Various Program fixes, multiple pattern matches, aliases. Fix bug in
 coercion code for simultaneous coercion of different arguments of an
 inductive type. Add tactics for dealing with heterogeneous equality. Export
 more error reporting functions from Cases.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9886 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 Makefile | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'Makefile')

diff --git a/Makefile b/Makefile
index 88beb3d509..ea9960ec4b 100644
--- a/Makefile
+++ b/Makefile
@@ -1130,7 +1130,8 @@ CCVO=
 
 DPVO=contrib/dp/Dp.vo
 
-SUBTACVO=contrib/subtac/SubtacTactics.vo contrib/subtac/Utils.vo contrib/subtac/FixSub.vo contrib/subtac/Subtac.vo \
+SUBTACVO=contrib/subtac/SubtacTactics.vo contrib/subtac/Heq.vo \
+	contrib/subtac/Utils.vo contrib/subtac/FixSub.vo contrib/subtac/Subtac.vo \
 	contrib/subtac/FunctionalExtensionality.vo
 
 RTAUTOVO = \
-- 
cgit v1.2.3