diff options
| author | msozeau | 2007-06-09 16:02:11 +0000 |
|---|---|---|
| committer | msozeau | 2007-06-09 16:02:11 +0000 |
| commit | 5caebcd8ff2bedae02a23d79251a2344c7aea4d6 (patch) | |
| tree | f10f3e2fb94e16fb5fc6df04e03d79ff428b4bb1 /Makefile | |
| parent | 481b6a29a87d04cfe54607702c83c9d35f371d75 (diff) | |
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
Diffstat (limited to 'Makefile')
| -rw-r--r-- | Makefile | 3 |
1 files changed, 2 insertions, 1 deletions
@@ -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 = \ |